# \[ANN\] coq-lsp 0.1.7

**URL:** <https://discourse.rocq-prover.org/t/ann-coq-lsp-0-1-7/1996>\
**Category:** Announcements\
**Tags:** coq-lsp, ui\
**Created:** [July 11, 2023, 10:57am UTC](https://discourse.rocq-prover.org/t/ann-coq-lsp-0-1-7/1996 "2023-07-11T10:57:23Z")\
**Posts on this page:** 1\
**Page:** 1

<div class="post-metadata">

**Author:** ![ejgallego](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/ejgallego/32/10_2.png) [@ejgallego](https://discourse.rocq-prover.org/u/ejgallego)\
**Post date:** [July 11, 2023, 10:57am UTC](https://discourse.rocq-prover.org/t/ann-coq-lsp-0-1-7/1996/1 "2023-07-11T10:57:24Z")

</div>

Hi folks,

it’s been a while, but we are happy to announce a new release of `coq-lsp`.

Install for Coq 8.17 and Visual Studio Code is as easy as:

```shell
$ opam install coq-lsp && code --install-extension ejgallego.coq-lsp

```

The 0.1.7 release has been focused on refinement and bugfixes; we’d like to thank all the users and contributors for their feedback and work, and in particular Alex Sanchez-Stern who did a large amount of beta testing and tweaks.

Following a suggestion by Hugo Herbelin, we now follow a naming scheme reminiscent of Isabelle’s:

- `coq-lsp` refers to the Coq LSP server
- `coq-lsp/Editor` refers to a particular client for `Editor`, such as  
`coq-lsp/Emacs`, `coq-lsp/VSCode`, or `coq-lsp/NeoVIM`.

This release also ships with some new features:

- `fcc`, the “Flèche Coq Compiler”, an extensible, machine-friendly command line compiler that provides direct access to `coq-lsp` internal checking engine (Flèche). A very preliminary plugin API for Flèche is also available. `fcc` does understand Coq markdown files (`.mv`), and can use the programmable error recovery mode from Flèche, etc…

- Coq Markdown files (`.mv`) are now regular Markdown files in `coq-lsp/VSCode`, thus one can do live proofs and use standard Markdown mode commands like preview at the same time (contributed by @4ever2)

- The UI for error display was improved by Tomás Díaz.

- The goal panel now display information about open and solved obligations.

- `coq-lsp/VSCode` is now a web extension, and thus it will activate on `github.dev` and `vscode.dev`. The server has been refactored so it can run on the Browser context, full support is expected in the next release.

- A new notification for performance data has been added to server, and a prototype panel displaying this data is now available for `coq-lsp/VSCode`.

`coq-lsp` release notes are archived at [rocq-lsp/etc/release\_notes at main · ejgallego/rocq-lsp · GitHub](https://github.com/ejgallego/coq-lsp/tree/main/etc/release_notes)

We’d like to highlight some interesting third party contributions we are aware of, and that could be of your interest:

- Bhakti Shah contributed support for her [ZX Calculus Visualizer](https://github.com/inQWIRE/ViZX)
- Arthur Azevedo de Amorim started an [Emacs client for coq-lsp](https://coq.zulipchat.com/#narrow/stream/329642-coq-lsp/topic/coq-lsp.20under.20Emacs.2E)
- Pedro Carrott and Nuno Saavedra are developing a [Python `coq-lsp` client](https://github.com/pcarrott/coq-lsp-pyclient)

Please find below the full list of changes:

# coq-lsp 0.1.7: Just-in-time

* * *

- New command line compiler `fcc`. `fcc` allows to access most  
features of `coq-lsp` without the need for a command line client,  
and it has been designed to be extensible and machine-friendly  
(@ejgallego, #507, fixes #472)
- Enable web extension support. For now this will not try to start  
the coq-lsp worker as it is not yet built. (@ejgallego, #430, fixes  
#234)
- Improvements and clenaups on hover display, in particular we don’t  
print repeated `Notation` strings (@ejgallego, #422)
- Don’t fail on missing serlib plugins, they are indeed an  
optimization; this mostly impacts 8.16 by lowering the SerAPI  
requirements (@ejgallego, #421)
- Fix bug that prevented “Goal after tactic” from working properly  
(@ejgallego, #438, reported by David Ilcinkas)
- Fix “Error message browser becomes non-visible when there are many  
goals” by using a fixed-position separated error display (@TDiazT,  
#445, fixes #441)
- Message about workspace detection was printing the wrong file,  
(@ejgallego, #444, reported by Alex Sanchez-Stern)
- Display the list of pending obligations in info panel (@ejgallego,  
#262)
- Preliminary support to display document performance data in panel  
(@ejgallego, #181)
- Fix cases when workspace / root URIs are `null`, as per LSP spec,  
(#453 , reported by orilahav, fixes #283)
- Pass implicit argument information to hover printer (@ejgallego, #453,  
fixes #448)
- Fix keybinding for the “Show Goals at Point” command (@4ever2, #460)
- Alert when `rootPath` is relative (#465, @ejgallego, report by Alex  
Sanchez-Stern)
- Hook coq-lsp to ViZX extension (@bhaktishh, #469)
- `proof/goals` request now takes an optional formatting parameter  
so clients can specify it per-request (@ejgallego, @bhaktishh, #470)
- New command line argument `--idle-delay=$secs` that controls how  
much an idle server will sleep before going back to request  
processing. Default setting is `0.1`, using more aggressive  
settings like `0.01` can decrease latency of requests by ~4x  
(@ejgallego, @hazardouspeach, #467, #471)
- Warnings from `_CoqProject` files are now applied (@ejgallego,  
reported by @arthuraa, #500)
- Be more resilient when serializing unknowns Asts (@ejgallego, #503,  
reported by Gijs Pennings)
- Coq’s STM is not linked anymore to `coq-lsp` (@ejgallego, #511)
- More granular options `send_perf_data` `send_diags`, `verbosity`  
will set them now (@ejgallego, #517)
- Preliminary plugin API for completion events (@ejgallego, #518,  
fixes #506)
- Limit the number of messages displayed in the goal window to 101,  
as to workaround slow render of Coq’s pretty printing format. This  
is an issue for example in Search where we can get thousand of  
results. We also speed up the rendering a bit by not hashing twice,  
and fix a parameter-passing bug. (@ejgallego, #523, reported by  
Anton Podkopaev)

Kind regards,  
The coq-lsp team