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.
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.
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
- 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.
- 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/getDocumentrequests due to a
parsing problem with extra fields in their requests (@ejgallego,
#547, reported by @Zimmi48)
fccnow understands the
-Rarguments (@ejgallego, #555)
- Describe findlib status in
Workspace.describe, which is printed
in the output windows (@ejgallego, #556)
coq-lspplugin 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)
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
- Hover request can now be extended by plugins (@ejgallego, #562)
- Updated LSP and JS client libs, notably to vscode-languageclient 9
- 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
- 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-lspis now supported by the
@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
_CoqProjectand 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)
pretacfield for preprocessing of goals with a tactic using
speculative execution, this is experimental for now (@amblafont,
@ejgallego, #573, helps with #558)
textDocument/selectionRangerequest, 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)