[ANN] coq-lsp release 0.1.5

Announcements
, ,
1

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 the project’s page.

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

1 Like