The Coq mailing list

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

Dear all,

We are happy to announce the 0.2.3 release of `coq-lsp`.

Highlights of the 0.2.x series:

- `serlib` is now part of `coq-lsp`. Thus, `coq-lsp` no longer depends
  on SerAPI.

  We recommend all SerAPI users migrate to `coq-lsp`, which together
  with `petanque` offers equivalent or significantly improved
  functionality.

- SerAPI has officially entered archival mode [1]. We'd like to thank
  all contributors!

- Starting with the 0.3.x series, `coq-lsp` will be renamed to `rocq-lsp`.

- Windows support: `coq-lsp` can be installed on Windows using stock
  Opam. `opam install coq-lsp` will do the trick!

- Supported versions: Coq 8.17 up to Rocq master are
  supported. Notably, support for Rocq 9.0 is new in 0.2.3.

- `petanque` has seen many improvements, thanks to Guillaume Baudart,
  Marc Lelarge, and Jules Viennot Franca,

- Rocq Emacs users can take advantage of Josselin Poiret's excellent
  rocq-mode.el: https://codeberg.org/jpoiret/rocq-mode.el

- Many other improvements and bugfixes, including:
  + quickFix support from Rocq upstream
  + improvements to on-demand mode
  + memory sharing among files (joint work with Gaëtan Gilbert)

- We will be around for the Rocq'n'share workshop [2], feel free to
  get in touch!

We'd like to thank to all the contributors and bug reporters for their
work on the 0.2.x series: 4ever2, Guillaume Baudart, Andrei
Listochkin, Gaëtan Gilbert, Josselin Poiret, Léo Stefanesco, Jules
Viennot Franca, as well as all the authors of Rocq overlays for Rocq's
CI system.

[1] https://github.com/rocq-community/manifesto/issues/160
[2] https://github.com/rocq-prover/rocq/wiki/Rocq'n'share-2025

Detailed changelog:

# coq-lsp 0.2.3: Barrage
------------------------

 - [fleche] fix quick fixes for errors being lost due to incorrect
   handling of `send_diags_extra_data` (@ejgallego, #850)
 - [vscode] Syntax highlighting for Coq 8.17-8.20 (@4ever2, #872)
 - [build] Adapt to Coq -> Rocq renaming (@ejgallego, @proux, #879)
 - [js worker] Update js_of_ocaml to 5.9.1 , thanks a lot to Hugo
   Heuzard for longstanding continued support of the jsCoq and coq-lsp
   projects (@ejgallego, @hhugo, #881)
 - [js worker] Update stubs (@ejgallego, @hhugo, #881)
 - [js worker] Fix build for Coq -> Rocq renaming and stdlib split
   (@ejgallego, #881)
 - [general] Adapt to Coq -> Rocq renaming (@ejgallego, @SkySkimmer,
   #883)
 - [general] [js] Adapt to Rocq stdlib split (@ejgallego, #890)
 - [ci] Bump setup-ocaml to v3 (@ejgallego, #890)
 - [ci] [windows] Use Opam 2.2 to build on windows (@ejgallego, #815,
   #890)
 - [petanque] `petanque/start` now fails when the theorem was parsed
   but not successfully executed (@ejgallego, reported by @gbdrt,
   #901, fixes #886)
 - [ci] Test Ocaml 5.3 (@ejgallego, #904)
 - [js worker] Add Shachar Itzhaky's trampoline patch; this greatly
   reduces the Stack Overflow in the proof engine (@ejgallego,
   @corwin-of-amber, #905)
 - [js worker] [build] Include Coq WaterProof in the default Web
   Worker build (@ejgallego, waterproof team, #905, closes #888)
 - [vscode] [web] Fix web extension not exporting the coq-lsp
   extension API (@ejgallego, reported by @amblafont, #911, fixes
   #877)
 - [build] [general] Rename our internal `Lsp` library to
   `Fleche_lsp`; this should help avoiding conflicts with the OCaml
   `lsp` library (@ejgallego, reported by @blackbird1128, #912, fixes
   #861)
 - [workspace] Remove support legacy ML-search path semantics. These
   were basically unused since Coq 8.16. As a consequence, `coq-lsp` /
   `fcc` don't accept the `-I` flag anymore, use `OCAMLPATH` or the
   `--ocamlpath=` option to pass extra `findlib` paths. We still
   respect the -I flag in `_CoqMakefile` (@ejgallego, #916)
 - [lsp] [debug] Respect `$/setTrace` call , refactor logging system,
   and allow file logging of protocol traces again (@ejgallego, #919,
   fixes #868)
 - [coq] Support Coq relocatable mode (@SkySkimmer, #891)
 - [ci] [deps] Remove support for OCaml 4.12 and 4.13, following
   upstream's coq/coq#20576 Note that these compiler versions have
   been unsupported for a long time, please upgrade (@ejgallego, #951)
 - [hover] New option `show_state_hash_on_hover` that displays state
    hash on hover for debug (@ejgallego, #954)
 - [doc] [faq] Updated FAQ to account for VSCoq 2 release in 2023,
   thanks to Patrick Nicodemus for pointing out the outdated
   documentation (@ejgallego, #846, fixes #817)
 - [vscode] [macos] Resolve keybinding conflict with Cmd+N and
   Cmd+Enter, we now use Alt+N and Alt+Shift+Enter, (Andrei
   Listochkin, #926)
 - [rocq] [fleche] Disable memprof-limits interruption backend by
   default, as released Rocq versions are not safe yet. If you want to
   enable it, you can still do it with the `--int_backend=Mp` command
   line option (@ejgallego, #957, fixes #857, reported by @dariusf,
   cc: rocq-prover/rocq#19177)
 - [lsp] [controller] Include Rocq feedback on request errors, using
   the optional `data` field. This is useful to still be able to
   obtain feedback messages such as debug messages even when a request
   fails. This also opens the door to better protocol handling and
   petanque integration (@ejgallego, #959, #961)
 - [petanque] Add feedback field to `Run_result.t`, this is important
   for many use cases. We also return feedback on petanque errors.
   (@ejgallego, @JulesViennotFranca, #960)
 - [petanque] new `get_state_at_pos` and `get_root_state` calls, that
   allow to retrieve a petanque proof state from position
   (@JulesViennotFranca, @ejgallego, #962)
 - [doc] [petanque] Document petanque v1, improve readme (@ejgallego,
   #963)

# coq-lsp 0.2.2: To Virtual or not To Virtual
---------------------------------------------

 - [vscode] Expand selectors to include `vscode-vfs://` URIs used in
   `github.dev`, document limited virtual workspace support in
   `package.json` (@ejgallego, #849)

# coq-lsp 0.2.1: Click !
------------------------

 - [deps] Bump toolchain so minimal `ppxlib` is 0.26, in order to fix
   some `ppx_import` oddities. This means our lower bound for the Jane
   Street packages is now `v0.15`, which should be fine for the
   foreseeable future (@ejgallego, #813)
 - [workspace] [coq] Support _CoqProject arguments `-type-in-type` and
   `-allow-rewrite-rules` (for 8.20) (@ejgallego, #819)
 - [serlib] Support for ltac2_ltac1 plugin (@ejgallego, #820)
 - [serlib] Fix Ltac2 AST piercing bug, add test case that should help
   in the future (@ejgallego, @jim-portegies, #821)
 - [fleche] [8.20] understand rewrite rules and symbols on document
   outline (@ejgallego, @Alizter, #825, fixes #824)
 - [fleche] [coq] support `Restart` meta command (@ejgallego,
   @Alizter, #828, fixes #827)
 - [fleche] [plugins] New plugin example `explain_errors`, that will
   print all errors on a file, with their goal context (@ejgallego,
   #829, thanks to @gmalecha for the idea, c.f. Coq issue 19601)
 - [fleche] Highlight the full first line of the document on
   initialization error (@ejgallego, #832)
 - [fleche] [jscoq] [js] Build worker version of `coq-lsp`. This
   provides a full working Coq enviroment in `vscode.dev`. The web
   worker version is build as an artifact on CI (@ejgallego
   @corwin-of-amber, #433)
 - [hover] Fix universe and level printing in hover (#839, fixes #835
   , @ejgallego , @Alizter)
 - [fleche] New immediate request serving mode. In this mode, requests
   are served with whatever document state we have. This is very
   useful when we are not in continuous mode, and we don't have a good
   reference as to what to build, for example in
   `documentSymbols`. The mode actually works pretty well in practice
   as often language requests will come after goals requests, so the
   info that is needed is at hand. It could also be tried to set the
   build target for immediate requests to the view hint, but we should
   see some motivation for that (@ejgallego, #841)
 - [lsp] [diagnostics] (! breaking change) change type of diagnostics
   extra data from list to named record (@ejgallego, #843)
 - [lsp] Implement support for `textDocument/codeAction`. For now, we
   support Coq's 8.21 `quickFix` data (@ejgallego, #840, #843, #845)
 - [petanque] Fix bug for detection of proof finished in deep stacks
   (@ejgallego, @gbdrt, #847)
 - [goals request] allow multiple Coq sentences in `command`. This is
   backwards compatible in the case that commands do not error, and
   users were sending just one command. (@ejgallego, #823, thanks to
   CoqPilot devs and G. Baudart for feedback)
 - [goals request] (! breaking) fail the request if the commands in
   `command` fail (@ejgallego, #823)

# coq-lsp 0.2.0: From Green to Blue
-----------------------------------

 - [deps] merge serlib into coq-lsp. This allow us to drop the SerAPI
   dependency, and will greatly easy the development of tools that
   require AST manipulation (@ejgallego, #698)
 - [fleche] Remove 8.16 compatibility layer (@ejgallego, #747)
 - [fleche] Preserve view hint across document changes. With this
   change, we get local continuous checking mode when the view-port
   heuristic is enabled (@ejgallego, #748)
 - [memo] More precise hashing for Coq states, this improves cache
   performance quite a bit (@ejgallego, #751)
 - [fleche] Enable sharing of `.vo` file parsing. This enables better
   sharing, achieving an almost 50% memory reduction for example when
   opening all of HoTT .v files (@ejgallego, @SkySkimmer, @bhaktishh,
   #744)
 - [memo] Provide API to query Hashtbl stats (@ejgallego, #753)
 - [nix] Add `pet-server` deps to flake.nix (Léo Stefanesco, #754)
 - [coq-lsp] Fix crash on `--help` option (Léo Stefanesco, @ejgallego,
   #754)
 - [vscode] Fix focus race when a Coq file is in column 2 (@ejgallego,
   #755, cc: #722, #725)
 - [hover] Show input howto for unicode characters on hover
   (@ejgallego, Léo Stefanesco, #756)
 - [lsp] [definition] Support for jump to definition across workspace
   files. The location information is obtained from `.glob` files, so
   it is often not perfect. (@ejgallego, #762, fixes #317)
 - [lsp] [hover] Show full name and provenance of identifiers
   (@ejgallego, #762)
 - [lsp] [definition] Try also to resolve and locate module imports
   (@ejgallego, #764)
 - [code] Don't start server on extension activation, unless an editor
   we own is active. We also auto-start the server if a document that
   we own is opened later (@ejgallego, #758, fixes #750)
 - [petanque] Allow `init` to be called multiple times (@ejgallego,
   @gbdrt, #766)
 - [petanque] Faster query for goals status after `run_tac`
   (@ejgallego, #768)
 - [petanque] New parameter `pre_commands` to `start` which allows
   instrumenting the goal before starting the proof (@ejgallego, Alex
   Sanchez-Stern #769)
 - [petanque] New `http_headers={yes,no}` parameter for `pet` json
   shell, plus some improvements on protocol handling (@ejgallego,
   #770)
 - [petanque] Make agent agnostic of environment, allowing embedding
   inside LSP (@ejgallego, #771)
 - [diagnostics] Ensure extra diagnostics info is present in all
   errors, not only on those sentences that did parse successfully
   (@ejgallego, Diego Rivera, #772)
 - [hover] New option `show_universes_on_hover` that will display
   universe data on hover (@ejgallego, @SkySkimmer, #666)
 - [hover] New plugin `unidiff` that will elaborate a summary of
   universe data a file, in particular regarding universes added at
   `Qed` time (@ejgallego, #773)
 - [fleche] Support meta-command `Abort All` (@ejgallego, #774, fixes
   #550)
 - [petanque] Allow memoization control on `petanque/run` via a new
   parameter `memo` (@ejgallego, #780)
 - [lsp] [petanque] Allow acces to `petanque` protocol from the lsp
   server (@ejgallego, #778)
 - [petanque] Always initialize a workspace. This made `pet` crash if
   `--root` was not used and client didn't issue the optimal
   `setWorkspace` call (#782, @ejgallego, @gbdrt)
 - [lsp] [petanque] New methods `state/eq` and `state/hash`; this
   allows clients to implement a client-side hash; equality is
   configurable with different methods; moreover, `petanque/run` can
   compute some extra data like state hashing without a round-trip
   (@ejgallego @gbdrt, #779)
 - [petanque] New methods to hash proof states; use proof state hash
   by default in petanque agent (@ejgallego, @gbdrt, #808)
 - [petanque] New shell method `petanque/toc` that returns a document
   outline in LSP-style (@ejgallego, #794)