The Coq mailing list

[Emilio Jesús Gallego Arias <e AT x80.org>]

Dear all,

We are happy to announce the first preview release of coq-lsp [1], a
lightweight language server protocol [7] server for Coq.

coq-lsp is based on work we have been doing for the last few years, in
particular with jsCoq [2] and lambdapi's [3] language server protocol.

coq-lsp is not yet ready for production, as there are known issues.  On
the other hand, we have tested coq-lsp with popular Coq developments
such as Software Foundations and we find it usable. See below for the
main known issues you should expect when using this release. So please
try it and give us feedback if you are feeling a bit adventurous.

The easiest way to install coq-lsp is using its opam package, which
should appear in the opam repository any minute now. That will install
coq-lsp for Coq 8.16.

The `main` branch which targets 8.17 will benefit from quite a few
bugfixes and improvements in latency that we did upstream.

A vscode client is provided in the vscode marketplace [5]; the server
has been also tested on Emacs using eglot [6]

coq-lsp departs from the traditional interaction paradigm in Coq, and
instead tries to implement continuous document checking, which is a
better fit for current UI models.

We hope to develop coq-lsp in an open manner, with (almost) weekly
developer meetings upcoming.

Some features in this 0.1.0 release are:

- Incremental compilation and continuous document checking
- Smart, cache-aware error recovery
- Whole-document goal display (Press Ctrl-Enter to display goals at point)
- Markdown support
- Document outline
- Timing and memory stats
- Client-side configuration options
- Standards-based, modular implementation

Release 0.1.1 should happen for Coq 8.17 beta.

In addition to the authors of the original lambdapi implementation
(Frédéric Blanqui, Rodolphe Lepigre, and myself, among others),
contributors to this release are:

- Ali Caglayan
- Shachar Itzhaky
- Ramkumar Ramachandra

Let us know what you think in our Zulip channel [4]

[1] https://github.com/ejgallego/coq-lsp
[2] https://github.com/jscoq/jscoq
[3] https://github.com/Deducteam/lambdapi
[4] https://coq.zulipchat.com/#narrow/stream/329642-coq-lsp
[5] 
https://marketplace.visualstudio.com/manage/publishers/ejgallego/extensions/coq-lsp
[6] https://github.com/joaotavora/eglot
[7] https://microsoft.github.io/language-server-protocol/

Kind regards,
Emilio J. Gallego Arias

coq-lsp 0.1.0 known issues:
---------------------------

- Opening two files will incompatible parsing rules will break parsing
  for both. This is Coq issue #12575, (and affects all IDEs).

- coq-lsp can't resume parsing reliably: this means that for each edit
  or request, coq-lsp must re-parse the document. This makes coq-lsp
  quite inconvenient to use in large documents, and precludes many
  interesting features like on-demand document checking.

  The problem seems to come from Coq's parser needing some more work in
  order to reliable support restarting from every possible source
  location; we hope to fix it for Coq 8.17.

- Overall, Coq upstream still needs many changes in order to implement
  reasonable features, help is much welcome if you wanna contribute!