The Coq mailing list

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

Dear all,

we are happy to announce the availability of coq-lsp 0.1.5, a Language
Server and Visual Studio Code extension for the Coq Proof Assistant.

See the install instructions at https://github.com/ejgallego/coq-lsp

This release provides many bug fixes and quality of life improvements,
in particular the goal panel has been much improved, and will now
display information about bullets, shelved, and admitted
goals. Additionally, error recovery interacts better with bullets now,
providing an improved case-analysis workflow.

In terms of protocol support, we have greatly improved the document
outline, added a preliminary jump to definition feature, and coq-lsp
will now show type information of identifiers and inductives when
hovering on them.

The Coq markdown mode has been improved as to properly highlight Coq
code, and some problems with windows and Unicode paths should be fixed
now.

We'd like to profusely thank all the early testers and contributors
for their feedback.

coq-lsp is developed collaboratively, you can find information about
our development process in the project's webpage; don't hesitate to
communicate any feedback or suggestion as to make contributing
experience more accessible to everyone.

Please find the detailed changelog below.

Ali Caglayan did a large effort in terms of documentation, testing,
and project management for this release. Also, a preliminary Neovim
mode has been made available by Jaehwang Jung.

Roadmap for 0.2.x:
------------------

This release marks a milestone for the 0.1.x series, as we consider
coq-lsp fit for our own Coq use.

We have been using coq-lsp daily for our Coq projects, and so far the
experience has been quite positive; we thus feel confident as to
recommend coq-lsp more broadly.

We expect a few more 0.1.x releases, targeting fixes and minor
improvements, but we will start work on 0.2.x soon.

Key points for 0.2.x are workspace support, integration with jsCoq and
github.dev, and support for external tools, replacing the coq-serapi
library.

We are particularly interested in helping authors of Coq tools to
integrate with the coq-lsp checking engine as to enable them to
provide extra functionality in a modular way.

Changes for coq-lsp 0.1.5: Form
------------------------------

 - Fix a bug when trying to complete in an empty file (@ejgallego,
   #270)
 - Fix a bug with the position reported by the `$/coq/fileProgress`
   notification (#270)
 - Fix messages panel rendering after the port to React (@ejgallego,
   #272)
 - Fix non-compliance with LSP range type due to extra `offset` field
   (@ejgallego, #271)
 - The goal display now numbers goals starting with 1 instead of 0
   (@artagnon, #277, report by Hugo Herbelin)
 - Markdown Coq code blocks now must specify "coq" as a language
   (@ejgallego, #280)
 - Server is now more strict w.r.t. what URIs it will accept for
   documents, see protocol documentation (@ejgallego, #286, reported
   by Alex Sanchez-Stern)
 - Hypotheses with bodies are now correctly displayed (@ejgallego,
   #296, fixes #293, report by Ali Caglayan)
 - `coq-lsp` incorrectly required the optional `rootPath`
   initialization parameter, moreover it ignored `rootUri` if present
   which goes against the LSP spec (@ejgallego, #295, report by Alex
   Sanchez-Stern)
 - `coq-lsp` will now reject opening multiple files when the
   underlying Coq version is buggy (@ejgallego, fixes #275, fixes
   #281)
 - Fix bug when parsing client option for unicode completion
   (@ejgallego #301)
 - Support unicode characters in filenames (@artagnon, #302)
 - Stop checking documents after a maximum number of errors,
   user-configurable (by default 150) (@ejgallego, #303)
 - Coq Markdown files (.mv extension) are now highlighted properly
   using both Coq and Markdown syntax rules (@4ever2, #307)
 - Goal view now supports find (@Alizter, #309, closes #305)
 - coq-lsp now understands a basic version of Coq Waterproof files
   (.wpn) Note that we don't associate to them by default, as to allow
   the waterproof extension to take over the files (@ejgallego, #306)
 - URI validation is now more strict, and some further bugs should be
   solved; note still this can be an issue on some client settings
   (@ejgallego, #313, fixes #187)
 - Display Coq info and debug messages in info panel (@ejgallego,
   #314, fixes #308)
 - Goal display handles background goals better, showing preview,
   goals stack, and focusing information (@ejgallego, #290, fixes
   #288, fixes #304, based on jsCoq code by Shachar Itzhaky)
 - Warnings are now printed in the info view messages panel
   (@ejgallego, #315, fixes #195)
 - Info protocol messages now have location and level
   (@ejgallego, #315)
 - Warnings are not printed in the info view messages panel
   (@ejgallego, #, fixes #195)
 - Improved `documentSymbol` return type for newer `DocumentSymbol[]`
   hierarchical symbol support. This means that sections and modules
   will now be properly represented, as well as constructors for
   inductive types, projections for records, etc...  (@ejgallego,
   #174, fixes #121, #122)
 - [internal] Error recovery can now execute full Coq commands as to
   amend states, required for #319 (@ejallego, #320)
 - Auto-admit the previous bullet goal when a new bullet cannot be
   opened due to an unsolved previous bullet. This also works for {}
   focusing operators. This is very useful when navigating bulleted
   proofs (@ejgallego, @Alizter, #319, fixes #300)
 - Store Ast.Info.t incrementally (@ejgallego, #337, fixes #316)
 - Basic jump to definition support; due to lack of workspace
   metadata, this only works inside the same file (@ejgallego, #318)
 - Show type of identifiers at point on hover (@ejgallego, #321, cc:
   #164)

Kind regards,
The coq-lsp team