The Coq mailing list

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

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.txt` has been removed in favor of `coq-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 `About` or
   `Search` are not shown anymore as diagnostics. Instead, they will
   be shown on the side panel when clicking on the corresponding
   command. The `show_notices_as_diagnostics` option allows to restore
   old behavior (@ejgallego, #128, fixes #125)
 - Print some more info about Coq workspace configuration (@ejgallego, #151)
 - Admit failed `Qed` by 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 `_CoqProject` detection 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/fileProgress` progress 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] https://github.com/ejgallego/coq-lsp/blob/main/etc/FAQ.md
[2] https://coq.zulipchat.com/#narrow/stream/329642-coq-lsp
[3] https://github.com/ejgallego/coq-lsp/wiki/Coq-Lsp-Calls

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!