Skip to content

[plugins] Baseline plugin for fcc#799

Merged
ejgallego merged 1 commit intomainfrom
baseline
Nov 27, 2025
Merged

[plugins] Baseline plugin for fcc#799
ejgallego merged 1 commit intomainfrom
baseline

Conversation

@ejgallego
Copy link
Collaborator

@ejgallego ejgallego commented Jul 1, 2024

The baseline plugin will try to prove every theorem in a file using a set of predefined tactics, and produce statistics on the way.

Use example:

fcc --plugin=coq-lsp.plugin.baseline foo.v

TODO:

  • cleanup / common parts
  • documentation / changelog
  • read actions from a file
  • tests

@ejgallego ejgallego added this to the 0.2.0 milestone Jul 1, 2024
@ejgallego ejgallego modified the milestones: 0.2.0, 0.2.1 Jul 12, 2024
@ejgallego ejgallego modified the milestones: 0.2.1, 0.2.2 Sep 26, 2024
@ejgallego ejgallego modified the milestones: 0.2.3, 0.2.4 Feb 7, 2025
@ejgallego ejgallego modified the milestones: 0.2.4, 0.2.5 Jun 4, 2025
@ejgallego ejgallego force-pushed the baseline branch 2 times, most recently from 3487d7b to c7f0cf7 Compare June 17, 2025 12:41
@ejgallego ejgallego modified the milestones: 0.2.5, 0.2.6 Sep 16, 2025
@ejgallego ejgallego modified the milestones: 0.2.6, 0.2.5 Nov 27, 2025
@ejgallego ejgallego force-pushed the baseline branch 2 times, most recently from 0cc1192 to 89f0e29 Compare November 27, 2025 14:17
@ejgallego ejgallego added kind: enhancement New feature or request part: plugins labels Nov 27, 2025
@ejgallego @eytans @corwin-of-amber
[plugins] Baseline plugin for fcc
0e95083 
The `baseline` plugin will try to prove every theorem in a file using
a set of predefined tactics, and produce statistics on the way.

Use example:

```
fcc --plugin=coq-lsp.plugin.baseline foo.v
```

TODO:

- cleanup / common parts
- documentation / changelog
- read actions from a file
- tests

Co-authored-by: Eytan Singher <eytan.singher@gmail.com>
Co-authored-by: Shachar Itzhaky <corwin.amber@gmail.com>
@ejgallego ejgallego marked this pull request as ready for review November 27, 2025 14:31
@ejgallego ejgallego merged commit 347727a into main Nov 27, 2025
13 checks passed
@ejgallego ejgallego deleted the baseline branch November 27, 2025 14:32
ejgallego added a commit that referenced this pull request Nov 27, 2025
@ejgallego
[changes] Missing entry for #799
9768f35
@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)
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 part: plugins

Projects

None yet

Milestone

0.2.5

Development

Successfully merging this pull request may close these issues.

1 participant

@ejgallego