Skip to content

[petanque] New command petanque/list_notations_in_statement#1017

Merged
ejgallego merged 1 commit intorocq-community:mainfrom
LLM4Rocq:v8.20-MoreCommands
Nov 27, 2025
Merged

[petanque] New command petanque/list_notations_in_statement#1017
ejgallego merged 1 commit intorocq-community:mainfrom
LLM4Rocq:v8.20-MoreCommands

Conversation

@JulesViennotFranca
Copy link
Contributor

@JulesViennotFranca JulesViennotFranca commented Sep 10, 2025

Hello @ejgallego, here is the pull request @gbdrt told you about. I added a way to list notations inside of a statement. It should be easy to extend this work to notations inside of Definition and Goal as well. If it could even be improved to definition of notations on hover for coq-lsp that would be incredible !

@ejgallego
Copy link
Collaborator

ejgallego commented Sep 10, 2025

Hi @JulesViennotFranca , thanks so much for the PR! A few notes:

  • as in Rocq upstream, PRs need to target the main branch.
  • as this seems to be using Rocq code, we'd need agreement from Rocq's team about a possible duplication and the impact on Rocq's CI
  • I have a few comments to do about the code, I'll be happy to review once the PR is rebased for main

@ejgallego ejgallego mentioned this pull request Oct 21, 2025
Closed
@ejgallego
Copy link
Collaborator

ejgallego commented Oct 21, 2025

Taking over, rebasing into main, and doing a bit of clean up.

@ejgallego ejgallego added this to the 0.2.5 milestone Oct 21, 2025
@ejgallego ejgallego changed the base branch from v8.20 to main October 21, 2025 13:41
@ejgallego ejgallego changed the title V8.20 more commands [petanque] New command petanque/list_notations_in_statement Oct 21, 2025
@ejgallego ejgallego force-pushed the v8.20-MoreCommands branch 2 times, most recently from d8eeb3c to b619ff9 Compare October 21, 2025 14:15
ejgallego added a commit to ejgallego/coq that referenced this pull request Oct 30, 2025
@ejgallego
[intern] Allow to instrument internalization via open recursion.
d8860f9 
This is similar to rocq-prover#6090, but for the pretyper.

I have witnesses ample user need for this, for example to extract the
set of notation or global identifiers used in a
term (c.f. rocq-community/rocq-lsp#1017 for example)
@ejgallego ejgallego mentioned this pull request Oct 30, 2025
Merged
@ejgallego ejgallego force-pushed the v8.20-MoreCommands branch 2 times, most recently from 9688b72 to cc55a8a Compare November 4, 2025 19:13
ejgallego added a commit to ejgallego/coq that referenced this pull request Nov 18, 2025
@ejgallego
[intern] Allow to instrument internalization via open recursion.
a3c47d3 
This is similar to rocq-prover#6090, but for the pretyper.

I have witnesses ample user need for this, for example to extract the
set of notation or global identifiers used in a
term (c.f. rocq-community/rocq-lsp#1017 for example)
ejgallego added a commit to ejgallego/coq that referenced this pull request Nov 24, 2025
@ejgallego
[intern] Allow to instrument internalization via open recursion.
ba41de8 
This is similar to rocq-prover#6090, but for the pretyper.

I have witnesses ample user need for this, for example to extract the
set of notation or global identifiers used in a
term (c.f. rocq-community/rocq-lsp#1017 for example)
ejgallego added a commit to ejgallego/coq that referenced this pull request Nov 24, 2025
@ejgallego
[intern] Allow to instrument internalization via open recursion.
208b424 
This is similar to rocq-prover#6090, but for the pretyper.

I have witnesses ample user need for this, for example to extract the
set of notation or global identifiers used in a
term (c.f. rocq-community/rocq-lsp#1017 for example)
@JulesViennotFranca @ejgallego
[petanque] New command petanque/list_notations_in_statement
40ac8ae 
Co-authored-by: Emilio Jesus Gallego Arias <e+git@x80.org>
@ejgallego ejgallego merged commit 52a29d8 into rocq-community:main Nov 27, 2025
13 checks passed
@ejgallego ejgallego deleted the v8.20-MoreCommands branch November 27, 2025 14:01
@ejgallego ejgallego mentioned this pull request Dec 1, 2025
Merged
ejgallego added a commit to ejgallego/opam-repository that referenced this pull request Dec 1, 2025
@ejgallego
[new release] coq-lsp (0.2.5+9.1)
82562fb 
CHANGES:

--------------------------

 - [build] [wasm] [code] bump esbuild from 0.16 to 0.25, miscellaneous
   npm dependencies bump (@ejgallego, rocq-community/rocq-lsp#1033)
 - [meta] Coq -> Rocq documentation rename (@ejgallego, rocq-community/rocq-lsp#1034)
 - [fleche] Support `\begin{rocq}` in literate Tex files (@ejgallego,
   rocq-community/rocq-lsp#1034)
 - [fleche] Fix crash in `coq/trimCaches` notification (rocq-community/rocq-lsp#1035,
   @ejgallego, reported by @gbdrt)
 - [controller] [goals] Fix a couple of bugs where goal printing
   didn't respect the `pp_format` setting, introduced in
   rocq-community/rocq-lsp#668. (@ejgallego, rocq-community/rocq-lsp#1037, fixes rocq-community/rocq-lsp#1030, thanks to Will Thomas for
   the report)
 - [opam] Require memprof-limits in OCaml >= 5.3 (@ejgallego, rocq-community/rocq-lsp#1038)
 - [ocaml] Support for OCaml 5.4, drop support for OCaml 5.0, 5.1, and
   5.2, drop support for Coq 8.17, 8.18, 8.19 (@ejgallego, rocq-community/rocq-lsp#1039)
 - [vscode] New command "Serialize Sentence at Point" that will print
   the AST of the Rocq sentence at point (@ejgallego, rocq-community/rocq-lsp#1048)
 - [petanque] New request `petanque/run_at_pos` (@ejgallego, rocq-community/rocq-lsp#1049)
 - [petanque] `petanque/get_state_at_pos` will default to the previous
   node state if there is no Rocq node at the current point
   (@ejgallego, rocq-community/rocq-lsp#1049)
 - [layout-engine] Support for notations with binders (@ejgallego,
   rocq-community/rocq-lsp#1050)
 - [layout-engine] Add background color for each box kind (@ejgallego,
   rocq-community/rocq-lsp#1050)
 - [compiler] Fix handling of literate files (@ejgallego, rocq-community/rocq-lsp#1056,
   reported by @jim-portegies)
 - [rocq] Create output directory on .vo file save if it doesn't
   exists. This is very useful in the web context where we don't yet
   have a proper virtual FS setup, thus making the "Save .vo file"
   command fail (@ejgallego, rocq-community/rocq-lsp#1054)
 - [web worker] Add LSP root to Rocq's loadpath, this makes .vo file
   loading work even when no worker FS setup could happen (@ejgallego,
   rocq-community/rocq-lsp#1054)
 - [fleche] New `coq/workspace_update` notification, which tells
   Flèche that `.vo` files in the workspace may have changed. This
   will make coq-lsp pick up changes in the filesystem and restart
   checking of Rocq's `Require`s when needed. The algorithm is not
   smart at all yet, as it invalidates all the requires for all open
   files. (@ejgallego, @helguo, rocq-community/rocq-lsp#1059)
 - [goals] New option (LSP, petanque, API) to display and retrieve
   goals without the compacted context. See protocol docs for more
   information. (@ejgallego, alexJ, rocq-community/rocq-lsp#1065, cc rocq-community/rocq-lsp#1043)
 - [fleche] [rocq] New options and data fields to expose document
   comments. This is experimental, pass the `--record_comments` flags
   to `rocq-lsp`, `fcc`, or `pet-server` to enable it. Once this flag
   is passed, comments for a document will be stored in the new
   `doc.comments` field. (@ejgallego, alexJ, rocq-community/rocq-lsp#1069, fixes rocq-community/rocq-lsp#353)
 - [hover] New debug option `show_pr_vernac_on_hover`, that will
   re-print the sentence under point using the Rocq printer
   (@ejgallego, alexJ, rocq-community/rocq-lsp#1070)
 - [petanque] New methods `proof_info` and `proof_info_at_pos` that
   return information about the current proof. As of today they return
   the proof name, text, range, ... (@DikieDick, @ejgallego, rocq-community/rocq-lsp#1051)
 - [petanque] New method `list_notations_in_statement` which returns
   an analysis of notations appearing inside a Rocq statement
   (@JulesViennotFranca, @ejgallego, rocq-community/rocq-lsp#1017)
 - [tools] New tool `rocq-checkdecls` for Rocq blueprints, inspired by
   the Lean version (rocq-community/rocq-lsp#785, @ejgallego, Andrej Bauer)
 - [plugins] New demo plugin "baseline", that tries to proof existing
   lemmas using a set of pre-fixed tactics (@ejgallego, Shachar
   Itzhaky, Eytan Singher, rocq-community/rocq-lsp#799)
 - [tools] New tool `checkdecls` for Coq blueprint, inspired by the
   Lean version (rocq-community/rocq-lsp#785, @ejgallego, Andrej Bauer)
 - [lsp] [rocq] Example of Ltac2 AST analysis using serlib's Analzyer
   infra (@ejgallego, @jim-portegies, @DikieDick, rocq-community/rocq-lsp#1058)
 - [lsp controller] Log internal errors to user-facing log
   (@ejgallego, rocq-community/rocq-lsp#1074)
 - [doc] Example typescript client connecting to the WASM-based lsp
   server (@ejgallego, rocq-community/rocq-lsp#626)
 - [hover] When the `show_doc_on_hover` option is enabled, hover will
   show coqdoc documentation when hovering on identifiers, using some
   heuristics to infer it from the comment just before
   it. Documentation is treated as Markdown. This feature is
   experimental and limited to documentation comments on the same file.
   (@ejgallego, rocq-community/rocq-lsp#590)
 - [plugins] New plugin to dump document data (@ejgallego, Stefania
   Dumbrava, rocq-community/rocq-lsp#1075)
 - [fcc] New option `--trace-file` that will generate trace data for
   visualizing with perfetto.dev (@ejgallego, AlexJ, Gaëtan Gilbert,
   rocq-community/rocq-lsp#1076)
 - [fcc] New options `--save_vof` and `--load_vof` that can save a
   Fleche version of a document to a `.vof` file, thus avoiding `.vo`
   recompilation for example when calling `fcc --plugin=...` for a
   given file (@ejgallego, Alexj, rocq-community/rocq-lsp#1077)
 - [vscode] Add config manager for handling client configuration
   changes in the infoview. Add configuration option for number of
   messages displayed (@Durbatuluk1701, rocq-community/rocq-lsp#1067)
 - [wasm] Update interrupt patch to account for timeouts (@ejgallego,
   Shachar Itzhaky, rocq-community/rocq-lsp#1078)
ejgallego added a commit to ejgallego/opam-repository that referenced this pull request Dec 1, 2025
@ejgallego
[new release] coq-lsp (0.2.5+9.0)
ac35f40 
CHANGES:

--------------------------

 - [build] [wasm] [code] bump esbuild from 0.16 to 0.25, miscellaneous
   npm dependencies bump (@ejgallego, rocq-community/rocq-lsp#1033)
 - [meta] Coq -> Rocq documentation rename (@ejgallego, rocq-community/rocq-lsp#1034)
 - [fleche] Support `\begin{rocq}` in literate Tex files (@ejgallego,
   rocq-community/rocq-lsp#1034)
 - [fleche] Fix crash in `coq/trimCaches` notification (rocq-community/rocq-lsp#1035,
   @ejgallego, reported by @gbdrt)
 - [controller] [goals] Fix a couple of bugs where goal printing
   didn't respect the `pp_format` setting, introduced in
   rocq-community/rocq-lsp#668. (@ejgallego, rocq-community/rocq-lsp#1037, fixes rocq-community/rocq-lsp#1030, thanks to Will Thomas for
   the report)
 - [opam] Require memprof-limits in OCaml >= 5.3 (@ejgallego, rocq-community/rocq-lsp#1038)
 - [ocaml] Support for OCaml 5.4, drop support for OCaml 5.0, 5.1, and
   5.2, drop support for Coq 8.17, 8.18, 8.19 (@ejgallego, rocq-community/rocq-lsp#1039)
 - [vscode] New command "Serialize Sentence at Point" that will print
   the AST of the Rocq sentence at point (@ejgallego, rocq-community/rocq-lsp#1048)
 - [petanque] New request `petanque/run_at_pos` (@ejgallego, rocq-community/rocq-lsp#1049)
 - [petanque] `petanque/get_state_at_pos` will default to the previous
   node state if there is no Rocq node at the current point
   (@ejgallego, rocq-community/rocq-lsp#1049)
 - [layout-engine] Support for notations with binders (@ejgallego,
   rocq-community/rocq-lsp#1050)
 - [layout-engine] Add background color for each box kind (@ejgallego,
   rocq-community/rocq-lsp#1050)
 - [compiler] Fix handling of literate files (@ejgallego, rocq-community/rocq-lsp#1056,
   reported by @jim-portegies)
 - [rocq] Create output directory on .vo file save if it doesn't
   exists. This is very useful in the web context where we don't yet
   have a proper virtual FS setup, thus making the "Save .vo file"
   command fail (@ejgallego, rocq-community/rocq-lsp#1054)
 - [web worker] Add LSP root to Rocq's loadpath, this makes .vo file
   loading work even when no worker FS setup could happen (@ejgallego,
   rocq-community/rocq-lsp#1054)
 - [fleche] New `coq/workspace_update` notification, which tells
   Flèche that `.vo` files in the workspace may have changed. This
   will make coq-lsp pick up changes in the filesystem and restart
   checking of Rocq's `Require`s when needed. The algorithm is not
   smart at all yet, as it invalidates all the requires for all open
   files. (@ejgallego, @helguo, rocq-community/rocq-lsp#1059)
 - [goals] New option (LSP, petanque, API) to display and retrieve
   goals without the compacted context. See protocol docs for more
   information. (@ejgallego, alexJ, rocq-community/rocq-lsp#1065, cc rocq-community/rocq-lsp#1043)
 - [fleche] [rocq] New options and data fields to expose document
   comments. This is experimental, pass the `--record_comments` flags
   to `rocq-lsp`, `fcc`, or `pet-server` to enable it. Once this flag
   is passed, comments for a document will be stored in the new
   `doc.comments` field. (@ejgallego, alexJ, rocq-community/rocq-lsp#1069, fixes rocq-community/rocq-lsp#353)
 - [hover] New debug option `show_pr_vernac_on_hover`, that will
   re-print the sentence under point using the Rocq printer
   (@ejgallego, alexJ, rocq-community/rocq-lsp#1070)
 - [petanque] New methods `proof_info` and `proof_info_at_pos` that
   return information about the current proof. As of today they return
   the proof name, text, range, ... (@DikieDick, @ejgallego, rocq-community/rocq-lsp#1051)
 - [petanque] New method `list_notations_in_statement` which returns
   an analysis of notations appearing inside a Rocq statement
   (@JulesViennotFranca, @ejgallego, rocq-community/rocq-lsp#1017)
 - [tools] New tool `rocq-checkdecls` for Rocq blueprints, inspired by
   the Lean version (rocq-community/rocq-lsp#785, @ejgallego, Andrej Bauer)
 - [plugins] New demo plugin "baseline", that tries to proof existing
   lemmas using a set of pre-fixed tactics (@ejgallego, Shachar
   Itzhaky, Eytan Singher, rocq-community/rocq-lsp#799)
 - [tools] New tool `checkdecls` for Coq blueprint, inspired by the
   Lean version (rocq-community/rocq-lsp#785, @ejgallego, Andrej Bauer)
 - [lsp] [rocq] Example of Ltac2 AST analysis using serlib's Analzyer
   infra (@ejgallego, @jim-portegies, @DikieDick, rocq-community/rocq-lsp#1058)
 - [lsp controller] Log internal errors to user-facing log
   (@ejgallego, rocq-community/rocq-lsp#1074)
 - [doc] Example typescript client connecting to the WASM-based lsp
   server (@ejgallego, rocq-community/rocq-lsp#626)
 - [hover] When the `show_doc_on_hover` option is enabled, hover will
   show coqdoc documentation when hovering on identifiers, using some
   heuristics to infer it from the comment just before
   it. Documentation is treated as Markdown. This feature is
   experimental and limited to documentation comments on the same file.
   (@ejgallego, rocq-community/rocq-lsp#590)
 - [plugins] New plugin to dump document data (@ejgallego, Stefania
   Dumbrava, rocq-community/rocq-lsp#1075)
 - [fcc] New option `--trace-file` that will generate trace data for
   visualizing with perfetto.dev (@ejgallego, AlexJ, Gaëtan Gilbert,
   rocq-community/rocq-lsp#1076)
 - [fcc] New options `--save_vof` and `--load_vof` that can save a
   Fleche version of a document to a `.vof` file, thus avoiding `.vo`
   recompilation for example when calling `fcc --plugin=...` for a
   given file (@ejgallego, Alexj, rocq-community/rocq-lsp#1077)
 - [vscode] Add config manager for handling client configuration
   changes in the infoview. Add configuration option for number of
   messages displayed (@Durbatuluk1701, rocq-community/rocq-lsp#1067)
 - [wasm] Update interrupt patch to account for timeouts (@ejgallego,
   Shachar Itzhaky, rocq-community/rocq-lsp#1078)
@ejgallego ejgallego mentioned this pull request Dec 1, 2025
Merged
ejgallego added a commit to ejgallego/opam-repository that referenced this pull request Dec 1, 2025
@ejgallego
[new release] coq-lsp (0.2.5+9.0)
9879373 
CHANGES:

--------------------------

 - [build] [wasm] [code] bump esbuild from 0.16 to 0.25, miscellaneous
   npm dependencies bump (@ejgallego, rocq-community/rocq-lsp#1033)
 - [meta] Coq -> Rocq documentation rename (@ejgallego, rocq-community/rocq-lsp#1034)
 - [fleche] Support `\begin{rocq}` in literate Tex files (@ejgallego,
   rocq-community/rocq-lsp#1034)
 - [fleche] Fix crash in `coq/trimCaches` notification (rocq-community/rocq-lsp#1035,
   @ejgallego, reported by @gbdrt)
 - [controller] [goals] Fix a couple of bugs where goal printing
   didn't respect the `pp_format` setting, introduced in
   rocq-community/rocq-lsp#668. (@ejgallego, rocq-community/rocq-lsp#1037, fixes rocq-community/rocq-lsp#1030, thanks to Will Thomas for
   the report)
 - [opam] Require memprof-limits in OCaml >= 5.3 (@ejgallego, rocq-community/rocq-lsp#1038)
 - [ocaml] Support for OCaml 5.4, drop support for OCaml 5.0, 5.1, and
   5.2, drop support for Coq 8.17, 8.18, 8.19 (@ejgallego, rocq-community/rocq-lsp#1039)
 - [vscode] New command "Serialize Sentence at Point" that will print
   the AST of the Rocq sentence at point (@ejgallego, rocq-community/rocq-lsp#1048)
 - [petanque] New request `petanque/run_at_pos` (@ejgallego, rocq-community/rocq-lsp#1049)
 - [petanque] `petanque/get_state_at_pos` will default to the previous
   node state if there is no Rocq node at the current point
   (@ejgallego, rocq-community/rocq-lsp#1049)
 - [layout-engine] Support for notations with binders (@ejgallego,
   rocq-community/rocq-lsp#1050)
 - [layout-engine] Add background color for each box kind (@ejgallego,
   rocq-community/rocq-lsp#1050)
 - [compiler] Fix handling of literate files (@ejgallego, rocq-community/rocq-lsp#1056,
   reported by @jim-portegies)
 - [rocq] Create output directory on .vo file save if it doesn't
   exists. This is very useful in the web context where we don't yet
   have a proper virtual FS setup, thus making the "Save .vo file"
   command fail (@ejgallego, rocq-community/rocq-lsp#1054)
 - [web worker] Add LSP root to Rocq's loadpath, this makes .vo file
   loading work even when no worker FS setup could happen (@ejgallego,
   rocq-community/rocq-lsp#1054)
 - [fleche] New `coq/workspace_update` notification, which tells
   Flèche that `.vo` files in the workspace may have changed. This
   will make coq-lsp pick up changes in the filesystem and restart
   checking of Rocq's `Require`s when needed. The algorithm is not
   smart at all yet, as it invalidates all the requires for all open
   files. (@ejgallego, @helguo, rocq-community/rocq-lsp#1059)
 - [goals] New option (LSP, petanque, API) to display and retrieve
   goals without the compacted context. See protocol docs for more
   information. (@ejgallego, alexJ, rocq-community/rocq-lsp#1065, cc rocq-community/rocq-lsp#1043)
 - [fleche] [rocq] New options and data fields to expose document
   comments. This is experimental, pass the `--record_comments` flags
   to `rocq-lsp`, `fcc`, or `pet-server` to enable it. Once this flag
   is passed, comments for a document will be stored in the new
   `doc.comments` field. (@ejgallego, alexJ, rocq-community/rocq-lsp#1069, fixes rocq-community/rocq-lsp#353)
 - [hover] New debug option `show_pr_vernac_on_hover`, that will
   re-print the sentence under point using the Rocq printer
   (@ejgallego, alexJ, rocq-community/rocq-lsp#1070)
 - [petanque] New methods `proof_info` and `proof_info_at_pos` that
   return information about the current proof. As of today they return
   the proof name, text, range, ... (@DikieDick, @ejgallego, rocq-community/rocq-lsp#1051)
 - [petanque] New method `list_notations_in_statement` which returns
   an analysis of notations appearing inside a Rocq statement
   (@JulesViennotFranca, @ejgallego, rocq-community/rocq-lsp#1017)
 - [tools] New tool `rocq-checkdecls` for Rocq blueprints, inspired by
   the Lean version (rocq-community/rocq-lsp#785, @ejgallego, Andrej Bauer)
 - [plugins] New demo plugin "baseline", that tries to proof existing
   lemmas using a set of pre-fixed tactics (@ejgallego, Shachar
   Itzhaky, Eytan Singher, rocq-community/rocq-lsp#799)
 - [tools] New tool `checkdecls` for Coq blueprint, inspired by the
   Lean version (rocq-community/rocq-lsp#785, @ejgallego, Andrej Bauer)
 - [lsp] [rocq] Example of Ltac2 AST analysis using serlib's Analzyer
   infra (@ejgallego, @jim-portegies, @DikieDick, rocq-community/rocq-lsp#1058)
 - [lsp controller] Log internal errors to user-facing log
   (@ejgallego, rocq-community/rocq-lsp#1074)
 - [doc] Example typescript client connecting to the WASM-based lsp
   server (@ejgallego, rocq-community/rocq-lsp#626)
 - [hover] When the `show_doc_on_hover` option is enabled, hover will
   show coqdoc documentation when hovering on identifiers, using some
   heuristics to infer it from the comment just before
   it. Documentation is treated as Markdown. This feature is
   experimental and limited to documentation comments on the same file.
   (@ejgallego, rocq-community/rocq-lsp#590)
 - [plugins] New plugin to dump document data (@ejgallego, Stefania
   Dumbrava, rocq-community/rocq-lsp#1075)
 - [fcc] New option `--trace-file` that will generate trace data for
   visualizing with perfetto.dev (@ejgallego, AlexJ, Gaëtan Gilbert,
   rocq-community/rocq-lsp#1076)
 - [fcc] New options `--save_vof` and `--load_vof` that can save a
   Fleche version of a document to a `.vof` file, thus avoiding `.vo`
   recompilation for example when calling `fcc --plugin=...` for a
   given file (@ejgallego, Alexj, rocq-community/rocq-lsp#1077)
 - [vscode] Add config manager for handling client configuration
   changes in the infoview. Add configuration option for number of
   messages displayed (@Durbatuluk1701, rocq-community/rocq-lsp#1067)
 - [wasm] Update interrupt patch to account for timeouts (@ejgallego,
   Shachar Itzhaky, rocq-community/rocq-lsp#1078)
ejgallego added a commit to ejgallego/opam-repository that referenced this pull request Dec 1, 2025
@ejgallego
[new release] coq-lsp (0.2.5+8.20)
3c2f2b5 
CHANGES:

--------------------------

 - [build] [wasm] [code] bump esbuild from 0.16 to 0.25, miscellaneous
   npm dependencies bump (@ejgallego, rocq-community/rocq-lsp#1033)
 - [meta] Coq -> Rocq documentation rename (@ejgallego, rocq-community/rocq-lsp#1034)
 - [fleche] Support `\begin{rocq}` in literate Tex files (@ejgallego,
   rocq-community/rocq-lsp#1034)
 - [fleche] Fix crash in `coq/trimCaches` notification (rocq-community/rocq-lsp#1035,
   @ejgallego, reported by @gbdrt)
 - [controller] [goals] Fix a couple of bugs where goal printing
   didn't respect the `pp_format` setting, introduced in
   rocq-community/rocq-lsp#668. (@ejgallego, rocq-community/rocq-lsp#1037, fixes rocq-community/rocq-lsp#1030, thanks to Will Thomas for
   the report)
 - [opam] Require memprof-limits in OCaml >= 5.3 (@ejgallego, rocq-community/rocq-lsp#1038)
 - [ocaml] Support for OCaml 5.4, drop support for OCaml 5.0, 5.1, and
   5.2, drop support for Coq 8.17, 8.18, 8.19 (@ejgallego, rocq-community/rocq-lsp#1039)
 - [vscode] New command "Serialize Sentence at Point" that will print
   the AST of the Rocq sentence at point (@ejgallego, rocq-community/rocq-lsp#1048)
 - [petanque] New request `petanque/run_at_pos` (@ejgallego, rocq-community/rocq-lsp#1049)
 - [petanque] `petanque/get_state_at_pos` will default to the previous
   node state if there is no Rocq node at the current point
   (@ejgallego, rocq-community/rocq-lsp#1049)
 - [layout-engine] Support for notations with binders (@ejgallego,
   rocq-community/rocq-lsp#1050)
 - [layout-engine] Add background color for each box kind (@ejgallego,
   rocq-community/rocq-lsp#1050)
 - [compiler] Fix handling of literate files (@ejgallego, rocq-community/rocq-lsp#1056,
   reported by @jim-portegies)
 - [rocq] Create output directory on .vo file save if it doesn't
   exists. This is very useful in the web context where we don't yet
   have a proper virtual FS setup, thus making the "Save .vo file"
   command fail (@ejgallego, rocq-community/rocq-lsp#1054)
 - [web worker] Add LSP root to Rocq's loadpath, this makes .vo file
   loading work even when no worker FS setup could happen (@ejgallego,
   rocq-community/rocq-lsp#1054)
 - [fleche] New `coq/workspace_update` notification, which tells
   Flèche that `.vo` files in the workspace may have changed. This
   will make coq-lsp pick up changes in the filesystem and restart
   checking of Rocq's `Require`s when needed. The algorithm is not
   smart at all yet, as it invalidates all the requires for all open
   files. (@ejgallego, @helguo, rocq-community/rocq-lsp#1059)
 - [goals] New option (LSP, petanque, API) to display and retrieve
   goals without the compacted context. See protocol docs for more
   information. (@ejgallego, alexJ, rocq-community/rocq-lsp#1065, cc rocq-community/rocq-lsp#1043)
 - [fleche] [rocq] New options and data fields to expose document
   comments. This is experimental, pass the `--record_comments` flags
   to `rocq-lsp`, `fcc`, or `pet-server` to enable it. Once this flag
   is passed, comments for a document will be stored in the new
   `doc.comments` field. (@ejgallego, alexJ, rocq-community/rocq-lsp#1069, fixes rocq-community/rocq-lsp#353)
 - [hover] New debug option `show_pr_vernac_on_hover`, that will
   re-print the sentence under point using the Rocq printer
   (@ejgallego, alexJ, rocq-community/rocq-lsp#1070)
 - [petanque] New methods `proof_info` and `proof_info_at_pos` that
   return information about the current proof. As of today they return
   the proof name, text, range, ... (@DikieDick, @ejgallego, rocq-community/rocq-lsp#1051)
 - [petanque] New method `list_notations_in_statement` which returns
   an analysis of notations appearing inside a Rocq statement
   (@JulesViennotFranca, @ejgallego, rocq-community/rocq-lsp#1017)
 - [tools] New tool `rocq-checkdecls` for Rocq blueprints, inspired by
   the Lean version (rocq-community/rocq-lsp#785, @ejgallego, Andrej Bauer)
 - [plugins] New demo plugin "baseline", that tries to proof existing
   lemmas using a set of pre-fixed tactics (@ejgallego, Shachar
   Itzhaky, Eytan Singher, rocq-community/rocq-lsp#799)
 - [tools] New tool `checkdecls` for Coq blueprint, inspired by the
   Lean version (rocq-community/rocq-lsp#785, @ejgallego, Andrej Bauer)
 - [lsp] [rocq] Example of Ltac2 AST analysis using serlib's Analzyer
   infra (@ejgallego, @jim-portegies, @DikieDick, rocq-community/rocq-lsp#1058)
 - [lsp controller] Log internal errors to user-facing log
   (@ejgallego, rocq-community/rocq-lsp#1074)
 - [doc] Example typescript client connecting to the WASM-based lsp
   server (@ejgallego, rocq-community/rocq-lsp#626)
 - [hover] When the `show_doc_on_hover` option is enabled, hover will
   show coqdoc documentation when hovering on identifiers, using some
   heuristics to infer it from the comment just before
   it. Documentation is treated as Markdown. This feature is
   experimental and limited to documentation comments on the same file.
   (@ejgallego, rocq-community/rocq-lsp#590)
 - [plugins] New plugin to dump document data (@ejgallego, Stefania
   Dumbrava, rocq-community/rocq-lsp#1075)
 - [fcc] New option `--trace-file` that will generate trace data for
   visualizing with perfetto.dev (@ejgallego, AlexJ, Gaëtan Gilbert,
   rocq-community/rocq-lsp#1076)
 - [fcc] New options `--save_vof` and `--load_vof` that can save a
   Fleche version of a document to a `.vof` file, thus avoiding `.vo`
   recompilation for example when calling `fcc --plugin=...` for a
   given file (@ejgallego, Alexj, rocq-community/rocq-lsp#1077)
 - [vscode] Add config manager for handling client configuration
   changes in the infoview. Add configuration option for number of
   messages displayed (@Durbatuluk1701, rocq-community/rocq-lsp#1067)
 - [wasm] Update interrupt patch to account for timeouts (@ejgallego,
   Shachar Itzhaky, rocq-community/rocq-lsp#1078)
@ejgallego ejgallego mentioned this pull request Dec 1, 2025
Merged
ejgallego added a commit to ejgallego/opam-repository that referenced this pull request Dec 1, 2025
@ejgallego
[new release] coq-lsp (0.2.5+9.1)
423b35e 
CHANGES:

--------------------------

 - [build] [wasm] [code] bump esbuild from 0.16 to 0.25, miscellaneous
   npm dependencies bump (@ejgallego, rocq-community/rocq-lsp#1033)
 - [meta] Coq -> Rocq documentation rename (@ejgallego, rocq-community/rocq-lsp#1034)
 - [fleche] Support `\begin{rocq}` in literate Tex files (@ejgallego,
   rocq-community/rocq-lsp#1034)
 - [fleche] Fix crash in `coq/trimCaches` notification (rocq-community/rocq-lsp#1035,
   @ejgallego, reported by @gbdrt)
 - [controller] [goals] Fix a couple of bugs where goal printing
   didn't respect the `pp_format` setting, introduced in
   rocq-community/rocq-lsp#668. (@ejgallego, rocq-community/rocq-lsp#1037, fixes rocq-community/rocq-lsp#1030, thanks to Will Thomas for
   the report)
 - [opam] Require memprof-limits in OCaml >= 5.3 (@ejgallego, rocq-community/rocq-lsp#1038)
 - [ocaml] Support for OCaml 5.4, drop support for OCaml 5.0, 5.1, and
   5.2, drop support for Coq 8.17, 8.18, 8.19 (@ejgallego, rocq-community/rocq-lsp#1039)
 - [vscode] New command "Serialize Sentence at Point" that will print
   the AST of the Rocq sentence at point (@ejgallego, rocq-community/rocq-lsp#1048)
 - [petanque] New request `petanque/run_at_pos` (@ejgallego, rocq-community/rocq-lsp#1049)
 - [petanque] `petanque/get_state_at_pos` will default to the previous
   node state if there is no Rocq node at the current point
   (@ejgallego, rocq-community/rocq-lsp#1049)
 - [layout-engine] Support for notations with binders (@ejgallego,
   rocq-community/rocq-lsp#1050)
 - [layout-engine] Add background color for each box kind (@ejgallego,
   rocq-community/rocq-lsp#1050)
 - [compiler] Fix handling of literate files (@ejgallego, rocq-community/rocq-lsp#1056,
   reported by @jim-portegies)
 - [rocq] Create output directory on .vo file save if it doesn't
   exists. This is very useful in the web context where we don't yet
   have a proper virtual FS setup, thus making the "Save .vo file"
   command fail (@ejgallego, rocq-community/rocq-lsp#1054)
 - [web worker] Add LSP root to Rocq's loadpath, this makes .vo file
   loading work even when no worker FS setup could happen (@ejgallego,
   rocq-community/rocq-lsp#1054)
 - [fleche] New `coq/workspace_update` notification, which tells
   Flèche that `.vo` files in the workspace may have changed. This
   will make coq-lsp pick up changes in the filesystem and restart
   checking of Rocq's `Require`s when needed. The algorithm is not
   smart at all yet, as it invalidates all the requires for all open
   files. (@ejgallego, @helguo, rocq-community/rocq-lsp#1059)
 - [goals] New option (LSP, petanque, API) to display and retrieve
   goals without the compacted context. See protocol docs for more
   information. (@ejgallego, alexJ, rocq-community/rocq-lsp#1065, cc rocq-community/rocq-lsp#1043)
 - [fleche] [rocq] New options and data fields to expose document
   comments. This is experimental, pass the `--record_comments` flags
   to `rocq-lsp`, `fcc`, or `pet-server` to enable it. Once this flag
   is passed, comments for a document will be stored in the new
   `doc.comments` field. (@ejgallego, alexJ, rocq-community/rocq-lsp#1069, fixes rocq-community/rocq-lsp#353)
 - [hover] New debug option `show_pr_vernac_on_hover`, that will
   re-print the sentence under point using the Rocq printer
   (@ejgallego, alexJ, rocq-community/rocq-lsp#1070)
 - [petanque] New methods `proof_info` and `proof_info_at_pos` that
   return information about the current proof. As of today they return
   the proof name, text, range, ... (@DikieDick, @ejgallego, rocq-community/rocq-lsp#1051)
 - [petanque] New method `list_notations_in_statement` which returns
   an analysis of notations appearing inside a Rocq statement
   (@JulesViennotFranca, @ejgallego, rocq-community/rocq-lsp#1017)
 - [tools] New tool `rocq-checkdecls` for Rocq blueprints, inspired by
   the Lean version (rocq-community/rocq-lsp#785, @ejgallego, Andrej Bauer)
 - [plugins] New demo plugin "baseline", that tries to proof existing
   lemmas using a set of pre-fixed tactics (@ejgallego, Shachar
   Itzhaky, Eytan Singher, rocq-community/rocq-lsp#799)
 - [tools] New tool `checkdecls` for Coq blueprint, inspired by the
   Lean version (rocq-community/rocq-lsp#785, @ejgallego, Andrej Bauer)
 - [lsp] [rocq] Example of Ltac2 AST analysis using serlib's Analzyer
   infra (@ejgallego, @jim-portegies, @DikieDick, rocq-community/rocq-lsp#1058)
 - [lsp controller] Log internal errors to user-facing log
   (@ejgallego, rocq-community/rocq-lsp#1074)
 - [doc] Example typescript client connecting to the WASM-based lsp
   server (@ejgallego, rocq-community/rocq-lsp#626)
 - [hover] When the `show_doc_on_hover` option is enabled, hover will
   show coqdoc documentation when hovering on identifiers, using some
   heuristics to infer it from the comment just before
   it. Documentation is treated as Markdown. This feature is
   experimental and limited to documentation comments on the same file.
   (@ejgallego, rocq-community/rocq-lsp#590)
 - [plugins] New plugin to dump document data (@ejgallego, Stefania
   Dumbrava, rocq-community/rocq-lsp#1075)
 - [fcc] New option `--trace-file` that will generate trace data for
   visualizing with perfetto.dev (@ejgallego, AlexJ, Gaëtan Gilbert,
   rocq-community/rocq-lsp#1076)
 - [fcc] New options `--save_vof` and `--load_vof` that can save a
   Fleche version of a document to a `.vof` file, thus avoiding `.vo`
   recompilation for example when calling `fcc --plugin=...` for a
   given file (@ejgallego, Alexj, rocq-community/rocq-lsp#1077)
 - [vscode] Add config manager for handling client configuration
   changes in the infoview. Add configuration option for number of
   messages displayed (@Durbatuluk1701, rocq-community/rocq-lsp#1067)
 - [wasm] Update interrupt patch to account for timeouts (@ejgallego,
   Shachar Itzhaky, rocq-community/rocq-lsp#1078)
@JulesViennotFranca JulesViennotFranca mentioned this pull request Dec 12, 2025
Merged
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

No reviews

Assignees

No one assigned

Labels

kind: enhancement New feature or request needs: test-case part: petanque

Projects

None yet

Milestone

0.2.5

Development

Successfully merging this pull request may close these issues.

2 participants

@JulesViennotFranca @ejgallego