Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

[roadmap] coq-layout-engine general issue #72

Open
ejgallego opened this issue Nov 17, 2022 · 0 comments
Open

[roadmap] coq-layout-engine general issue #72

ejgallego opened this issue Nov 17, 2022 · 0 comments
Labels
kind: meta

Comments

@ejgallego
Copy link
Owner

ejgallego commented Nov 17, 2022 •
edited
Loading

This issue is for tracking the integration of coq-layout-engine into coq-lsp.

What is coq-layout-engine ?

coq-layout-engine is a new printer for Coq documents that targets a box model similar to the one of LaTeX or the DOM, with a focus on this last media. The idea of printing Coq terms in a different format appeared early in the jsCoq development, but only until recently we figured out the right way we'd like to proceed.

History and development

The early wishes for a different goal rendering system arose early in the development of jsCoq as to do some "point and click" proving. Moreover, there are many common use cases, for example, linking identifiers to their location, unfolding notations on the go, displaying implicit arguments, outputting to TeX, etc...

While many of these issues can be solved by other means, including this information in a rich printer setting seems to work pretty well. Isabelle realized about this quite some time ago, and they use what is called, "Semantic Printing". Unfortunately Coq current printer doesn't preserve the required structure.

An overview of the issues and first implementation effort was given in a talk at IRIF in Oct 2021, see the slides , the corresponding code is at jscoq/jscoq#28

Thus, coq-layout-engine is very similar in spirit to Isabelle's printer, but using a different tech stack, in particular, we output to something very close to HTML / Web Components.

Goals

  • standards based
  • cover most use cases in regular and educational Coq development
  • non-goal: compatibility with old printer
  • provide users with advanced notations support (for example relation refinement style)

Roadmap

For the last year, the development of coq-layout-engine has been waiting for coq-lsp and jsCoq to modernize other parts of their stack, but we are reaching a point where we can experiment a bit more. The current TODO list is:

  • Move the directory to her,e, for now we host monorepos style to make the development more agile
  • Complete the printing for all structures to html
  • Render for notations (either web components or React ?)
  • Extend Coq to hint the printer properly
  • Challenge: can CSS alone provide a reasonable layout?
  • Challenge: Coq elaboration API is pretty challenging to use from UIs, for many reasons. There is tricky work to do here. The first problem is lack of a proper functional interface to it.
  • Implement CEP PR 10 / 11 / 19
  • Test-suite

Notes and related work

  • There was a meeting with Clément Pit-Claudel, Shachar Itzhacky, and Emilio J. Gallego Arias to discuss the jsCoq prototype
  • See the slides for more links to important CEPs
  • Shachar's Pp.t printer and test-suite in jsCoq (and port to vsCode ongoing in Problems building v8.10 branch rocq-archive/coq-serapi#143
@ejgallego ejgallego changed the title Integrate coq-layout-engine coq-layout-engine general issue Jan 24, 2023
@ejgallego ejgallego changed the title coq-layout-engine general issue [roadmap] coq-layout-engine general issue Jan 25, 2023
@ejgallego ejgallego mentioned this issue Jan 25, 2023
Open
@Alizter Alizter moved this to Todo in coq-lsp roadmap Jan 29, 2023
@Alizter Alizter moved this from Todo to Meta in coq-lsp roadmap Jan 29, 2023
This was referenced Feb 15, 2023
Open
Closed
ejgallego added a commit that referenced this issue Apr 4, 2024
@ejgallego
[layout engine] Move Coq Layout engine tree to coq-lsp repos.
a6a0f71 
For now we just host the code here, and compile it. We will add the
selection method later on.

CC: #72

Replaces: jscoq/jscoq#282
@ejgallego ejgallego mentioned this issue Apr 4, 2024
Draft
ejgallego added a commit that referenced this issue Apr 4, 2024
@ejgallego
[layout engine] Move Coq Layout engine tree to coq-lsp repos.
42de2c6 
For now we just host the code here, and compile it. We will add the
selection method later on.

CC: #72

Replaces: jscoq/jscoq#282
ejgallego added a commit that referenced this issue Apr 4, 2024
@ejgallego
[layout engine] Move Coq Layout engine tree to coq-lsp repos.
8455ada 
For now we just host the code here, and compile it. We will add the
selection method later on.

CC: #72

Replaces: jscoq/jscoq#282
ejgallego added a commit that referenced this issue Apr 4, 2024
@ejgallego
[layout engine] Move Coq Layout engine tree to coq-lsp repos.
7e2f013 
For now we just host the code here, and compile it. We will add the
selection method later on.

CC: #72

Replaces: jscoq/jscoq#282
ejgallego added a commit that referenced this issue Apr 10, 2024
@ejgallego
[layout engine] Move Coq Layout engine tree to coq-lsp repos.
da50223 
For now we just host the code here, and compile it. We will add the
selection method later on.

CC: #72

Replaces: jscoq/jscoq#282
ejgallego added a commit that referenced this issue Jun 4, 2024
@ejgallego
[layout engine] Move Coq Layout engine tree to coq-lsp repos.
0b694b2 
For now we just host the code here, and compile it. We will add the
selection method later on.

CC: #72

Replaces: jscoq/jscoq#282
ejgallego added a commit that referenced this issue Jun 5, 2024
@ejgallego
[layout engine] Move Coq Layout engine tree to coq-lsp repos.
09389cc 
For now we just host the code here, and compile it. We will add the
selection method later on.

CC: #72

Replaces: jscoq/jscoq#282
ejgallego added a commit that referenced this issue Sep 26, 2024
@ejgallego
[layout engine] Move Coq Layout engine tree to coq-lsp repos.
9e891bb 
For now we just host the code here, and compile it. We will add the
selection method later on.

CC: #72

Replaces: jscoq/jscoq#282
ejgallego added a commit that referenced this issue Sep 26, 2024
@ejgallego
[layout engine] Move Coq Layout engine tree to coq-lsp repos.
1ed3416 
For now we just host the code here, and compile it. We will add the
selection method later on.

CC: #72

Replaces: jscoq/jscoq#282
ejgallego added a commit that referenced this issue Sep 28, 2024
@ejgallego
[layout engine] Move Coq Layout engine tree to coq-lsp repos.
2b94731 
For now we just host the code here, and compile it. We will add the
selection method later on.

CC: #72

Replaces: jscoq/jscoq#282
ejgallego added a commit that referenced this issue Sep 29, 2024
@ejgallego
[layout engine] Move Coq Layout engine tree to coq-lsp repos.
8f4b21a 
For now we just host the code here, and compile it. We will add the
selection method later on.

CC: #72

Replaces: jscoq/jscoq#282
patrick-nicodemus pushed a commit to patrick-nicodemus/coq-lsp that referenced this issue Dec 2, 2024
@ejgallego @patrick-nicodemus
[layout engine] Move Coq Layout engine tree to coq-lsp repos.
9303145 
For now we just host the code here, and compile it. We will add the
selection method later on.

CC: ejgallego#72

Replaces: jscoq/jscoq#282
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
kind: meta
Projects
coq-lsp roadmap
Status: Meta
Milestone
No milestone
Development

No branches or pull requests
1 participant
@ejgallego