[ANN] coq-lsp 0.2.3

Announcements
,
1

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: 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 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)
2 Likes