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)
coq-lsp F.A.Q.  for some often asked questions.
Don’t hesitate to stop by our Zulip  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.
coq-lsp developers and user online meeting will take place Monday January 9th, at 5pm Paris time, see  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:
- 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 of
(@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
- Coq “Notice” messages, such as the ones generated by
Searchare not shown anymore as diagnostics. Instead, they will
be shown on the side panel when clicking on the corresponding
show_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)
- Don’t crash if the log file can’t be created (@ejgallego, #87)
- Use LSP functions for client-side logging (@ejgallego, #87)
_CoqProjectdetection settings to client window (@ejgallego, #88)
- Use plugin include paths from
- 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)
$/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,
- 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)
The coq-lsp team
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!