[wasm] Update interrupt patch to account for timeouts #1078
Conversation
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
ejgallego
added
kind: enhancement
ejgallego
added a commit
to ejgallego/opam-repository
that referenced
this pull request
Dec 1, 2025
CHANGES: -------------------------- - [build] [wasm] [code] bump esbuild from 0.16 to 0.25, miscellaneous npm dependencies bump (@ejgallego, ejgallego/rocq-lsp#1033) - [meta] Coq -> Rocq documentation rename (@ejgallego, ejgallego/rocq-lsp#1034) - [fleche] Support `\begin{rocq}` in literate Tex files (@ejgallego, ejgallego/rocq-lsp#1034) - [fleche] Fix crash in `coq/trimCaches` notification (ejgallego/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 ejgallego/rocq-lsp#668. (@ejgallego, ejgallego/rocq-lsp#1037, fixes ejgallego/rocq-lsp#1030, thanks to Will Thomas for the report) - [opam] Require memprof-limits in OCaml >= 5.3 (@ejgallego, ejgallego/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, ejgallego/rocq-lsp#1039) - [vscode] New command "Serialize Sentence at Point" that will print the AST of the Rocq sentence at point (@ejgallego, ejgallego/rocq-lsp#1048) - [petanque] New request `petanque/run_at_pos` (@ejgallego, ejgallego/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, ejgallego/rocq-lsp#1049) - [layout-engine] Support for notations with binders (@ejgallego, ejgallego/rocq-lsp#1050) - [layout-engine] Add background color for each box kind (@ejgallego, ejgallego/rocq-lsp#1050) - [compiler] Fix handling of literate files (@ejgallego, ejgallego/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, ejgallego/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, ejgallego/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, ejgallego/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, ejgallego/rocq-lsp#1065, cc ejgallego/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, ejgallego/rocq-lsp#1069, fixes ejgallego/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, ejgallego/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, ejgallego/rocq-lsp#1051) - [petanque] New method `list_notations_in_statement` which returns an analysis of notations appearing inside a Rocq statement (@JulesViennotFranca, @ejgallego, ejgallego/rocq-lsp#1017) - [tools] New tool `rocq-checkdecls` for Rocq blueprints, inspired by the Lean version (ejgallego/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, ejgallego/rocq-lsp#799) - [tools] New tool `checkdecls` for Coq blueprint, inspired by the Lean version (ejgallego/rocq-lsp#785, @ejgallego, Andrej Bauer) - [lsp] [rocq] Example of Ltac2 AST analysis using serlib's Analzyer infra (@ejgallego, @jim-portegies, @DikieDick, ejgallego/rocq-lsp#1058) - [lsp controller] Log internal errors to user-facing log (@ejgallego, ejgallego/rocq-lsp#1074) - [doc] Example typescript client connecting to the WASM-based lsp server (@ejgallego, ejgallego/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, ejgallego/rocq-lsp#590) - [plugins] New plugin to dump document data (@ejgallego, Stefania Dumbrava, ejgallego/rocq-lsp#1075) - [fcc] New option `--trace-file` that will generate trace data for visualizing with perfetto.dev (@ejgallego, AlexJ, Gaëtan Gilbert, ejgallego/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, ejgallego/rocq-lsp#1077) - [vscode] Add config manager for handling client configuration changes in the infoview. Add configuration option for number of messages displayed (@Durbatuluk1701, ejgallego/rocq-lsp#1067) - [wasm] Update interrupt patch to account for timeouts (@ejgallego, Shachar Itzhaky, ejgallego/rocq-lsp#1078)
ejgallego
added a commit
to ejgallego/opam-repository
that referenced
this pull request
Dec 1, 2025
CHANGES: -------------------------- - [build] [wasm] [code] bump esbuild from 0.16 to 0.25, miscellaneous npm dependencies bump (@ejgallego, ejgallego/rocq-lsp#1033) - [meta] Coq -> Rocq documentation rename (@ejgallego, ejgallego/rocq-lsp#1034) - [fleche] Support `\begin{rocq}` in literate Tex files (@ejgallego, ejgallego/rocq-lsp#1034) - [fleche] Fix crash in `coq/trimCaches` notification (ejgallego/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 ejgallego/rocq-lsp#668. (@ejgallego, ejgallego/rocq-lsp#1037, fixes ejgallego/rocq-lsp#1030, thanks to Will Thomas for the report) - [opam] Require memprof-limits in OCaml >= 5.3 (@ejgallego, ejgallego/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, ejgallego/rocq-lsp#1039) - [vscode] New command "Serialize Sentence at Point" that will print the AST of the Rocq sentence at point (@ejgallego, ejgallego/rocq-lsp#1048) - [petanque] New request `petanque/run_at_pos` (@ejgallego, ejgallego/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, ejgallego/rocq-lsp#1049) - [layout-engine] Support for notations with binders (@ejgallego, ejgallego/rocq-lsp#1050) - [layout-engine] Add background color for each box kind (@ejgallego, ejgallego/rocq-lsp#1050) - [compiler] Fix handling of literate files (@ejgallego, ejgallego/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, ejgallego/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, ejgallego/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, ejgallego/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, ejgallego/rocq-lsp#1065, cc ejgallego/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, ejgallego/rocq-lsp#1069, fixes ejgallego/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, ejgallego/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, ejgallego/rocq-lsp#1051) - [petanque] New method `list_notations_in_statement` which returns an analysis of notations appearing inside a Rocq statement (@JulesViennotFranca, @ejgallego, ejgallego/rocq-lsp#1017) - [tools] New tool `rocq-checkdecls` for Rocq blueprints, inspired by the Lean version (ejgallego/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, ejgallego/rocq-lsp#799) - [tools] New tool `checkdecls` for Coq blueprint, inspired by the Lean version (ejgallego/rocq-lsp#785, @ejgallego, Andrej Bauer) - [lsp] [rocq] Example of Ltac2 AST analysis using serlib's Analzyer infra (@ejgallego, @jim-portegies, @DikieDick, ejgallego/rocq-lsp#1058) - [lsp controller] Log internal errors to user-facing log (@ejgallego, ejgallego/rocq-lsp#1074) - [doc] Example typescript client connecting to the WASM-based lsp server (@ejgallego, ejgallego/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, ejgallego/rocq-lsp#590) - [plugins] New plugin to dump document data (@ejgallego, Stefania Dumbrava, ejgallego/rocq-lsp#1075) - [fcc] New option `--trace-file` that will generate trace data for visualizing with perfetto.dev (@ejgallego, AlexJ, Gaëtan Gilbert, ejgallego/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, ejgallego/rocq-lsp#1077) - [vscode] Add config manager for handling client configuration changes in the infoview. Add configuration option for number of messages displayed (@Durbatuluk1701, ejgallego/rocq-lsp#1067) - [wasm] Update interrupt patch to account for timeouts (@ejgallego, Shachar Itzhaky, ejgallego/rocq-lsp#1078)
ejgallego
added a commit
to ejgallego/opam-repository
that referenced
this pull request
Dec 1, 2025
CHANGES: -------------------------- - [build] [wasm] [code] bump esbuild from 0.16 to 0.25, miscellaneous npm dependencies bump (@ejgallego, ejgallego/rocq-lsp#1033) - [meta] Coq -> Rocq documentation rename (@ejgallego, ejgallego/rocq-lsp#1034) - [fleche] Support `\begin{rocq}` in literate Tex files (@ejgallego, ejgallego/rocq-lsp#1034) - [fleche] Fix crash in `coq/trimCaches` notification (ejgallego/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 ejgallego/rocq-lsp#668. (@ejgallego, ejgallego/rocq-lsp#1037, fixes ejgallego/rocq-lsp#1030, thanks to Will Thomas for the report) - [opam] Require memprof-limits in OCaml >= 5.3 (@ejgallego, ejgallego/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, ejgallego/rocq-lsp#1039) - [vscode] New command "Serialize Sentence at Point" that will print the AST of the Rocq sentence at point (@ejgallego, ejgallego/rocq-lsp#1048) - [petanque] New request `petanque/run_at_pos` (@ejgallego, ejgallego/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, ejgallego/rocq-lsp#1049) - [layout-engine] Support for notations with binders (@ejgallego, ejgallego/rocq-lsp#1050) - [layout-engine] Add background color for each box kind (@ejgallego, ejgallego/rocq-lsp#1050) - [compiler] Fix handling of literate files (@ejgallego, ejgallego/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, ejgallego/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, ejgallego/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, ejgallego/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, ejgallego/rocq-lsp#1065, cc ejgallego/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, ejgallego/rocq-lsp#1069, fixes ejgallego/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, ejgallego/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, ejgallego/rocq-lsp#1051) - [petanque] New method `list_notations_in_statement` which returns an analysis of notations appearing inside a Rocq statement (@JulesViennotFranca, @ejgallego, ejgallego/rocq-lsp#1017) - [tools] New tool `rocq-checkdecls` for Rocq blueprints, inspired by the Lean version (ejgallego/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, ejgallego/rocq-lsp#799) - [tools] New tool `checkdecls` for Coq blueprint, inspired by the Lean version (ejgallego/rocq-lsp#785, @ejgallego, Andrej Bauer) - [lsp] [rocq] Example of Ltac2 AST analysis using serlib's Analzyer infra (@ejgallego, @jim-portegies, @DikieDick, ejgallego/rocq-lsp#1058) - [lsp controller] Log internal errors to user-facing log (@ejgallego, ejgallego/rocq-lsp#1074) - [doc] Example typescript client connecting to the WASM-based lsp server (@ejgallego, ejgallego/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, ejgallego/rocq-lsp#590) - [plugins] New plugin to dump document data (@ejgallego, Stefania Dumbrava, ejgallego/rocq-lsp#1075) - [fcc] New option `--trace-file` that will generate trace data for visualizing with perfetto.dev (@ejgallego, AlexJ, Gaëtan Gilbert, ejgallego/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, ejgallego/rocq-lsp#1077) - [vscode] Add config manager for handling client configuration changes in the infoview. Add configuration option for number of messages displayed (@Durbatuluk1701, ejgallego/rocq-lsp#1067) - [wasm] Update interrupt patch to account for timeouts (@ejgallego, Shachar Itzhaky, ejgallego/rocq-lsp#1078)
ejgallego
added a commit
to ejgallego/opam-repository
that referenced
this pull request
Dec 1, 2025
CHANGES: -------------------------- - [build] [wasm] [code] bump esbuild from 0.16 to 0.25, miscellaneous npm dependencies bump (@ejgallego, ejgallego/rocq-lsp#1033) - [meta] Coq -> Rocq documentation rename (@ejgallego, ejgallego/rocq-lsp#1034) - [fleche] Support `\begin{rocq}` in literate Tex files (@ejgallego, ejgallego/rocq-lsp#1034) - [fleche] Fix crash in `coq/trimCaches` notification (ejgallego/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 ejgallego/rocq-lsp#668. (@ejgallego, ejgallego/rocq-lsp#1037, fixes ejgallego/rocq-lsp#1030, thanks to Will Thomas for the report) - [opam] Require memprof-limits in OCaml >= 5.3 (@ejgallego, ejgallego/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, ejgallego/rocq-lsp#1039) - [vscode] New command "Serialize Sentence at Point" that will print the AST of the Rocq sentence at point (@ejgallego, ejgallego/rocq-lsp#1048) - [petanque] New request `petanque/run_at_pos` (@ejgallego, ejgallego/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, ejgallego/rocq-lsp#1049) - [layout-engine] Support for notations with binders (@ejgallego, ejgallego/rocq-lsp#1050) - [layout-engine] Add background color for each box kind (@ejgallego, ejgallego/rocq-lsp#1050) - [compiler] Fix handling of literate files (@ejgallego, ejgallego/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, ejgallego/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, ejgallego/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, ejgallego/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, ejgallego/rocq-lsp#1065, cc ejgallego/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, ejgallego/rocq-lsp#1069, fixes ejgallego/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, ejgallego/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, ejgallego/rocq-lsp#1051) - [petanque] New method `list_notations_in_statement` which returns an analysis of notations appearing inside a Rocq statement (@JulesViennotFranca, @ejgallego, ejgallego/rocq-lsp#1017) - [tools] New tool `rocq-checkdecls` for Rocq blueprints, inspired by the Lean version (ejgallego/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, ejgallego/rocq-lsp#799) - [tools] New tool `checkdecls` for Coq blueprint, inspired by the Lean version (ejgallego/rocq-lsp#785, @ejgallego, Andrej Bauer) - [lsp] [rocq] Example of Ltac2 AST analysis using serlib's Analzyer infra (@ejgallego, @jim-portegies, @DikieDick, ejgallego/rocq-lsp#1058) - [lsp controller] Log internal errors to user-facing log (@ejgallego, ejgallego/rocq-lsp#1074) - [doc] Example typescript client connecting to the WASM-based lsp server (@ejgallego, ejgallego/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, ejgallego/rocq-lsp#590) - [plugins] New plugin to dump document data (@ejgallego, Stefania Dumbrava, ejgallego/rocq-lsp#1075) - [fcc] New option `--trace-file` that will generate trace data for visualizing with perfetto.dev (@ejgallego, AlexJ, Gaëtan Gilbert, ejgallego/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, ejgallego/rocq-lsp#1077) - [vscode] Add config manager for handling client configuration changes in the infoview. Add configuration option for number of messages displayed (@Durbatuluk1701, ejgallego/rocq-lsp#1067) - [wasm] Update interrupt patch to account for timeouts (@ejgallego, Shachar Itzhaky, ejgallego/rocq-lsp#1078)
ejgallego
added a commit
to ejgallego/opam-repository
that referenced
this pull request
Dec 1, 2025
CHANGES: -------------------------- - [build] [wasm] [code] bump esbuild from 0.16 to 0.25, miscellaneous npm dependencies bump (@ejgallego, ejgallego/rocq-lsp#1033) - [meta] Coq -> Rocq documentation rename (@ejgallego, ejgallego/rocq-lsp#1034) - [fleche] Support `\begin{rocq}` in literate Tex files (@ejgallego, ejgallego/rocq-lsp#1034) - [fleche] Fix crash in `coq/trimCaches` notification (ejgallego/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 ejgallego/rocq-lsp#668. (@ejgallego, ejgallego/rocq-lsp#1037, fixes ejgallego/rocq-lsp#1030, thanks to Will Thomas for the report) - [opam] Require memprof-limits in OCaml >= 5.3 (@ejgallego, ejgallego/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, ejgallego/rocq-lsp#1039) - [vscode] New command "Serialize Sentence at Point" that will print the AST of the Rocq sentence at point (@ejgallego, ejgallego/rocq-lsp#1048) - [petanque] New request `petanque/run_at_pos` (@ejgallego, ejgallego/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, ejgallego/rocq-lsp#1049) - [layout-engine] Support for notations with binders (@ejgallego, ejgallego/rocq-lsp#1050) - [layout-engine] Add background color for each box kind (@ejgallego, ejgallego/rocq-lsp#1050) - [compiler] Fix handling of literate files (@ejgallego, ejgallego/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, ejgallego/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, ejgallego/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, ejgallego/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, ejgallego/rocq-lsp#1065, cc ejgallego/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, ejgallego/rocq-lsp#1069, fixes ejgallego/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, ejgallego/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, ejgallego/rocq-lsp#1051) - [petanque] New method `list_notations_in_statement` which returns an analysis of notations appearing inside a Rocq statement (@JulesViennotFranca, @ejgallego, ejgallego/rocq-lsp#1017) - [tools] New tool `rocq-checkdecls` for Rocq blueprints, inspired by the Lean version (ejgallego/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, ejgallego/rocq-lsp#799) - [tools] New tool `checkdecls` for Coq blueprint, inspired by the Lean version (ejgallego/rocq-lsp#785, @ejgallego, Andrej Bauer) - [lsp] [rocq] Example of Ltac2 AST analysis using serlib's Analzyer infra (@ejgallego, @jim-portegies, @DikieDick, ejgallego/rocq-lsp#1058) - [lsp controller] Log internal errors to user-facing log (@ejgallego, ejgallego/rocq-lsp#1074) - [doc] Example typescript client connecting to the WASM-based lsp server (@ejgallego, ejgallego/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, ejgallego/rocq-lsp#590) - [plugins] New plugin to dump document data (@ejgallego, Stefania Dumbrava, ejgallego/rocq-lsp#1075) - [fcc] New option `--trace-file` that will generate trace data for visualizing with perfetto.dev (@ejgallego, AlexJ, Gaëtan Gilbert, ejgallego/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, ejgallego/rocq-lsp#1077) - [vscode] Add config manager for handling client configuration changes in the infoview. Add configuration option for number of messages displayed (@Durbatuluk1701, ejgallego/rocq-lsp#1067) - [wasm] Update interrupt patch to account for timeouts (@ejgallego, Shachar Itzhaky, ejgallego/rocq-lsp#1078)
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
No description provided.