Dear all,
we are happy to announce the release of coq-lsp 0.1.2, a new language Server and VSCode extension for the Coq interactive proof assistant.
coq-lsp aims to provide a modern and streamlined proof-editing experience, supporting incremental checking, markdown documents, and an error recovery strategy friendly to step wise development of proof documents.
The 0.1.2 release has been significantly improved since the 0.1.0 preview release, we encourage Visual Studio Code users to try it!
(make sure that the client and server version coincide, and see below for known issues)
See the coq-lsp F.A.Q. [1] for some often asked questions.
Don’t hesitate to stop by our Zulip [2] channel to chat, provide feedback, or report bugs.
coq-lsp is developed in an open, collaborative way, if you are interested in helping, we are really looking forward to it. There are many interesting projects that can be done with coq-lsp as a base.
The first coq-lsp developers and user online meeting will take place Monday January 9th, at 5pm Paris time, see [3] for details.
The main known issue is that coq-lsp won’t properly handle yet proving with multiple buffers, this is due to problems in Coq upstream, Coq developers and in particular Gaëtan Gilbert are working in a fix.
If you find this issue, simply close all other .v files and restart the server.
The full changelog for this release is:
coq-lsp 0.1.2: Message
- Send an error to the client if the client and server versions don’t
match (@ejgallego, #126) - Parse options -noinit, -indices-matter, and -impredicative-set from
_CoqProject(@artagnon, @ejgallego, #140, #150) - Log file
log-lsp.txthas been removed in favor ofcoq-lsp.trace.server
(@artagnon, @ejgallego, #130, #148) - Added --bt flag to print a backtrace on error (@Alizter, #147)
- A detailed view of Coq errors is now displayed in the info panel
(@ejgallego, #128) - Coq “Notice” messages, such as the ones generated by
Aboutor
Searchare not shown anymore as diagnostics. Instead, they will
be shown on the side panel when clicking on the corresponding
command. Theshow_notices_as_diagnosticsoption allows to restore
old behavior (@ejgallego, #128, fixes #125) - Print some more info about Coq workspace configuration (@ejgallego, #151)
- Admit failed
Qedby default; allow users to configure it
(@ejgallego, #118, fixes #90)
coq-lsp 0.1.1: Location
- Don’t crash if the log file can’t be created (@ejgallego, #87)
- Use LSP functions for client-side logging (@ejgallego, #87)
- Log
_CoqProjectdetection settings to client window (@ejgallego, #88) - Use plugin include paths from
_CoqProject(@ejgallego, #88) - Support OCaml >= 4.12 (@ejgallego, #93)
- Optimize the number of diagnostics sent in eager mode (@ejgallego, #104)
- Improved syntax highlighting on VSCode client (@artagnon, #105)
- Resume document checking from the point it was interrupted
(@ejgallego, #95, #99) - Don’t convert Coq “Info” messages such as “Foo is defined” to
feedback by default; users willing to see them can set the
corresponding option (@ejgallego, #113) - Send
$/coq/fileProgressprogress notifications from server,
similarly to what Lean does; display them in Code’s right gutter
(@ejgallego, #106, fixes #54) - Show goals on click by default, allow users to configure the
behavior to follow cursor in different ways (@ejgallego, #116,
fixes #89) - Show file position in goal buffer, use collapsible elements for
goal list (@ejgallego, #115, fixes #109) - Resume checking from common prefix on document update (@ejgallego,
#111, fixes #110) - Only serve goals, hover, and symbols requests when the document
has been sufficiently processed (@ejgallego, #120, fixes #100)
Kind regards,
The coq-lsp team
[1] coq-lsp/FAQ.md at main · ejgallego/coq-lsp · GitHub
[2] https://coq.zulipchat.com/#narrow/stream/329642-coq-lsp
[3] Coq Lsp Calls · ejgallego/coq-lsp Wiki · GitHub
Errata for the 0.1.0 release mail: we forgot Vincent Laporte in the list of contributors, who contributed the first version of the VSCode client. Thanks Vincent and sorry!