BreakOut 2020 12 01 Karl
Two topics discussed:
attending: Emilio Gallego, Gaëtan Gilbert, Karl Palmskog
-
how to support load: files have to be marked as not to produce
.vofiles; no special difficulty,coqdepseems to work ok already -
work on inter-project composition: work in progress, once it is finished and tested, we expect Coq's dune language to be stable.
[Enrico joined mid-discussion]
Karl shows their work on having naming suggestions / linting information, and questions how to integrate with document managers.
Document managers should offer a plugin API for such linters, composed of 2 callbacks:
-
callback for document update, providing API to query document / changes similar to what SerAPI has
Key problem: frequency / smoothness of interactive updates w.r.t. the callback.
-
callback to ask for linting information for a particular point, main challenge to avoid the linter maintain their own document model
Some more links:
To the extent possible under law, the contributors of the Rocq wiki have waived all copyright and related or neighboring rights to their contributions.
By contributing to the Rocq wiki, you agree that you hold the copyright and you agree to license your contribution under the CC0 license or you agree that you have permission to distribute your contribution under the CC0 license.