BreakOut 2020 12 01 Karl - coq/coq GitHub Wiki

Two topics discussed:

attending: Emilio Gallego, Gaëtan Gilbert, Karl Palmskog

Dune for Coq Projects

  • how to support load: files have to be marked as not to produce .vo files; no special difficulty, coqdep seems 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.

Linter API

[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:

https://microsoft.github.io/language-server-protocol/specifications/specification-current/#textDocument_codeAction