[ANN] coq-lsp 0.1.8

Announcements
,
1

Dear all,

the 0.1.8 release of coq-lsp is out.

This release brings important fixes and a few performance improvements; in particular editing inside opaque proofs should behave much better w.r.t. incremental engine; formatting inside the error and
message panels has been fixed, as well as display for light mode.

On the protocol side, the LSP textDocument/selectionRange method is now supported, allowing clients to easily select full Coq sentences.

On the developer side, the Plugin API has seen some enhancements, and hover plugins can now be declared.

We consider coq-lsp to be in beta, but fully usable status for a large majority of setups; we encourage Coq users to try coq-lsp now and report back. Documentation seems to be the main hurdle new users
are facing, please let us know about problems in this area so we can improve.

We’d like to thank to all the contributors and bug reporters for their work; contributions, bug reports, and feedback over coq-lsp are much welcome, get in touch with us at GitHub or Zulip if you have
questions or comments.

See coq-lsp’s README for detailed installation instructions.

Also new in this release are the official windows installers, built on the Coq platform. Nix support has also been generously improved by contributors.

Note that currently released Coq versions do contain critical bugs w.r.t. async interruptions. We strongly recommend that you install a fixed Coq version as outlined in coq-lsp’s README. Windows
installers are already built with a fixed Coq version.

We take this opportunity to highlight a couple of recently released projects built over coq-lsp:

  • WaterProof “2.0” (link), by the WaterProof team, an educational mathematical environment for Coq
  • CoREACT Yade (link), by Ambroise Lafont, a graphical editor for diagrammatic category theory proofs in Coq

coq-lsp is compatible with Coq 8.16-8.18 and master. We will be phasing out Coq 8.16 support soon due to lack of manpower, contact us if you are interested in helping maintaining it.

Detailed Changelog:

  • Update VSCode client dependencies, should bring some performance
    improvements to goal pretty printing (@ejgallego, #530)
  • Update goal display colors for light mode so they are actually
    readable now. (@bhaktishh, #539, fixes #532)
  • Added link to Python coq-lsp client by Pedro Carrot and Nuno
    Saavedra (@Nfsaavedra, #536)
  • Properly concatenate warnings from _CoqProject (@ejgallego,
    reported by @mituharu, #541, fixes #540)
  • Fix broken coq/saveVo and coq/getDocument requests due to a
    parsing problem with extra fields in their requests (@ejgallego,
    #547, reported by @Zimmi48)
  • fcc now understands the --coqlib, --coqcorelib,
    --ocamlpath, -Q and -R arguments (@ejgallego, #555)
  • Describe findlib status in Workspace.describe, which is printed
    in the output windows (@ejgallego, #556)
  • coq-lsp plugin loader will now be strict in case of a plugin
    failure, the previous loose behavior was more convenient for the
    early releases, but it doesn’t make sense now and made things
    pretty hard to debug on the Windows installer (@ejgallego, #557)
  • Add pointers to Windows installers (@ejgallego, #559)
  • Recognize Goal and Definition $id : ... . as proof starters
    (@ejgallego, #561, reported by @Zimmi48, fixes #548)
  • Provide basic notation information on hover. This is intended for
    people to build their own more refined notation feedback systems
    (@ejgallego, #562)
  • Hover request can now be extended by plugins (@ejgallego, #562)
  • Updated LSP and JS client libs, notably to vscode-languageclient 9
    (@ejgallego, #565)
  • Implement a LIFO document scheduler, this is heavier in the
    background as more documents will be checked, but provides a few
    usability improvements (@ejgallego, #566, fixes #563, reported by
    Ali Caglayan)
  • New lexical qed detection error recovery rule; this makes a very
    large usability difference in practice when editing inside proofs.
    (@ejgallego, #567, fixes #33)
  • coq-lsp is now supported by the coq-nix-toolbox (@Zimmi48,
    @CohenCyril, #572, via
    Add coq-lsp server in nix-shell when available. by Zimmi48 · Pull Request #164 · coq-community/coq-nix-toolbox · GitHub )
  • Support for -rifrom in _CoqProject and in command line
    (--rifrom). Thanks to Lasse Blaauwbroek for the report.
    (@ejgallego, #581, fixes #579)
  • Export Query Goals API in VSCode client; this way other extensions
    can implement their own commands that query Coq goals (@amblafont,
    @ejgallego, #576, closes #558)
  • New pretac field for preprocessing of goals with a tactic using
    speculative execution, this is experimental for now (@amblafont,
    @ejgallego, #573, helps with #558)
  • Implement textDocument/selectionRange request, that will return
    the range of the Coq sentence underlying the cursor. In VSCode,
    this is triggered by the “Expand Selection” command. The
    implementation is partial: we only take into account the first
    position, and we only return a single range (Coq sentence) without
    parents. (@ejgallego, #582)
  • Be more robust to mixed-separator windows paths in workspace
    detection (@ejgallego, #583, fixes #569)
  • Adjust printing breaks in error and message panels (@ejgallego,
    @Alizter, #586, fixes #457 , fixes #458 , fixes #571)

Kind regards,
Emilio