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 ofcoq-lsp
. Thus,coq-lsp
no longer depends
on SerAPI.We recommend all SerAPI users migrate to
coq-lsp
, which together
withpetanque
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 torocq-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: jpoiret/rocq-mode.el: An Emacs mode for the Rocq theorem prover, using coq-lsp - Codeberg.org -
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] Proposal to move project coq-serapi to coq-community · Issue #160 · rocq-community/manifesto · GitHub
[2] Rocq'n'share 2025 · rocq-prover/rocq Wiki · GitHub
Detailed changelog:
coq-lsp 0.2.3: Barrage
- [fleche] fix quick fixes for errors being lost due to incorrect
handling ofsend_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, useOCAMLPATH
or the
--ocamlpath=
option to pass extrafindlib
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 optionaldata
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
andget_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
someppx_import
oddities. This means our lower bound for the Jane
Street packages is nowv0.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 invscode.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.21quickFix
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
tostart
which allows
instrumenting the goal before starting the proof (@ejgallego, Alex
Sanchez-Stern #769) - [petanque] New
http_headers={yes,no}
parameter forpet
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
parametermemo
(@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
andstate/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)