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 ejgallego/coq-serapi#143