Releases · ejgallego/rocq-lsp · GitHub

01 Dec 19:52

ejgallego

0.2.5+9.1

CHANGES:

[build] [wasm] [code] bump esbuild from 0.16 to 0.25, miscellaneous
npm dependencies bump (@ejgallego, #1033)
[meta] Coq -> Rocq documentation rename (@ejgallego, #1034)
[fleche] Support \begin{rocq} in literate Tex files (@ejgallego,
#1034)
[fleche] Fix crash in coq/trimCaches notification (#1035,
@ejgallego, reported by @gbdrt)
[controller] [goals] Fix a couple of bugs where goal printing
didn't respect the pp_format setting, introduced in
#668. (@ejgallego, #1037, fixes #1030, thanks to Will Thomas for
the report)
[opam] Require memprof-limits in OCaml >= 5.3 (@ejgallego, #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, #1039)
[vscode] New command "Serialize Sentence at Point" that will print
the AST of the Rocq sentence at point (@ejgallego, #1048)
[petanque] New request petanque/run_at_pos (@ejgallego, #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, #1049)
[layout-engine] Support for notations with binders (@ejgallego,
#1050)
[layout-engine] Add background color for each box kind (@ejgallego,
#1050)
[compiler] Fix handling of literate files (@ejgallego, #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, #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,
#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 Requires when needed. The algorithm is not
smart at all yet, as it invalidates all the requires for all open
files. (@ejgallego, @helguo, #1059)
[goals] New option (LSP, petanque, API) to display and retrieve
goals without the compacted context. See protocol docs for more
information. (@ejgallego, alexJ, #1065, cc #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, #1069, fixes #353)
[hover] New debug option show_pr_vernac_on_hover, that will
re-print the sentence under point using the Rocq printer
(@ejgallego, alexJ, #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, #1051)
[petanque] New method list_notations_in_statement which returns
an analysis of notations appearing inside a Rocq statement
(@JulesViennotFranca, @ejgallego, #1017)
[tools] New tool rocq-checkdecls for Rocq blueprints, inspired by
the Lean version (#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, #799)
[tools] New tool checkdecls for Coq blueprint, inspired by the
Lean version (#785, @ejgallego, Andrej Bauer)
[lsp] [rocq] Example of Ltac2 AST analysis using serlib's Analzyer
infra (@ejgallego, @jim-portegies, @DikieDick, #1058)
[lsp controller] Log internal errors to user-facing log
(@ejgallego, #1074)
[doc] Example typescript client connecting to the WASM-based lsp
server (@ejgallego, #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, #590)
[plugins] New plugin to dump document data (@ejgallego, Stefania
Dumbrava, #1075)
[fcc] New option --trace-file that will generate trace data for
visualizing with perfetto.dev (@ejgallego, AlexJ, Gaëtan Gilbert,
#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, #1077)
[vscode] Add config manager for handling client configuration
changes in the infoview. Add configuration option for number of
messages displayed (@Durbatuluk1701, #1067)
[wasm] Update interrupt patch to account for timeouts (@ejgallego,
Shachar Itzhaky, #1078)

Contributors

ejgallego, gbdrt, and 5 other contributors

Assets 3

01 Dec 20:14

ejgallego

0.2.5+9.0

CHANGES:

[build] [wasm] [code] bump esbuild from 0.16 to 0.25, miscellaneous
npm dependencies bump (@ejgallego, #1033)
[meta] Coq -> Rocq documentation rename (@ejgallego, #1034)
[fleche] Support \begin{rocq} in literate Tex files (@ejgallego,
#1034)
[fleche] Fix crash in coq/trimCaches notification (#1035,
@ejgallego, reported by @gbdrt)
[controller] [goals] Fix a couple of bugs where goal printing
didn't respect the pp_format setting, introduced in
#668. (@ejgallego, #1037, fixes #1030, thanks to Will Thomas for
the report)
[opam] Require memprof-limits in OCaml >= 5.3 (@ejgallego, #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, #1039)
[vscode] New command "Serialize Sentence at Point" that will print
the AST of the Rocq sentence at point (@ejgallego, #1048)
[petanque] New request petanque/run_at_pos (@ejgallego, #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, #1049)
[layout-engine] Support for notations with binders (@ejgallego,
#1050)
[layout-engine] Add background color for each box kind (@ejgallego,
#1050)
[compiler] Fix handling of literate files (@ejgallego, #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, #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,
#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 Requires when needed. The algorithm is not
smart at all yet, as it invalidates all the requires for all open
files. (@ejgallego, @helguo, #1059)
[goals] New option (LSP, petanque, API) to display and retrieve
goals without the compacted context. See protocol docs for more
information. (@ejgallego, alexJ, #1065, cc #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, #1069, fixes #353)
[hover] New debug option show_pr_vernac_on_hover, that will
re-print the sentence under point using the Rocq printer
(@ejgallego, alexJ, #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, #1051)
[petanque] New method list_notations_in_statement which returns
an analysis of notations appearing inside a Rocq statement
(@JulesViennotFranca, @ejgallego, #1017)
[tools] New tool rocq-checkdecls for Rocq blueprints, inspired by
the Lean version (#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, #799)
[tools] New tool checkdecls for Coq blueprint, inspired by the
Lean version (#785, @ejgallego, Andrej Bauer)
[lsp] [rocq] Example of Ltac2 AST analysis using serlib's Analzyer
infra (@ejgallego, @jim-portegies, @DikieDick, #1058)
[lsp controller] Log internal errors to user-facing log
(@ejgallego, #1074)
[doc] Example typescript client connecting to the WASM-based lsp
server (@ejgallego, #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, #590)
[plugins] New plugin to dump document data (@ejgallego, Stefania
Dumbrava, #1075)
[fcc] New option --trace-file that will generate trace data for
visualizing with perfetto.dev (@ejgallego, AlexJ, Gaëtan Gilbert,
#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, #1077)
[vscode] Add config manager for handling client configuration
changes in the infoview. Add configuration option for number of
messages displayed (@Durbatuluk1701, #1067)
[wasm] Update interrupt patch to account for timeouts (@ejgallego,
Shachar Itzhaky, #1078)

Contributors

ejgallego, gbdrt, and 5 other contributors

Assets 3

01 Dec 20:31

ejgallego

0.2.5+8.20 Latest

Latest

CHANGES:

[build] [wasm] [code] bump esbuild from 0.16 to 0.25, miscellaneous
npm dependencies bump (@ejgallego, #1033)
[meta] Coq -> Rocq documentation rename (@ejgallego, #1034)
[fleche] Support \begin{rocq} in literate Tex files (@ejgallego,
#1034)
[fleche] Fix crash in coq/trimCaches notification (#1035,
@ejgallego, reported by @gbdrt)
[controller] [goals] Fix a couple of bugs where goal printing
didn't respect the pp_format setting, introduced in
#668. (@ejgallego, #1037, fixes #1030, thanks to Will Thomas for
the report)
[opam] Require memprof-limits in OCaml >= 5.3 (@ejgallego, #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, #1039)
[vscode] New command "Serialize Sentence at Point" that will print
the AST of the Rocq sentence at point (@ejgallego, #1048)
[petanque] New request petanque/run_at_pos (@ejgallego, #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, #1049)
[layout-engine] Support for notations with binders (@ejgallego,
#1050)
[layout-engine] Add background color for each box kind (@ejgallego,
#1050)
[compiler] Fix handling of literate files (@ejgallego, #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, #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,
#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 Requires when needed. The algorithm is not
smart at all yet, as it invalidates all the requires for all open
files. (@ejgallego, @helguo, #1059)
[goals] New option (LSP, petanque, API) to display and retrieve
goals without the compacted context. See protocol docs for more
information. (@ejgallego, alexJ, #1065, cc #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, #1069, fixes #353)
[hover] New debug option show_pr_vernac_on_hover, that will
re-print the sentence under point using the Rocq printer
(@ejgallego, alexJ, #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, #1051)
[petanque] New method list_notations_in_statement which returns
an analysis of notations appearing inside a Rocq statement
(@JulesViennotFranca, @ejgallego, #1017)
[tools] New tool rocq-checkdecls for Rocq blueprints, inspired by
the Lean version (#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, #799)
[tools] New tool checkdecls for Coq blueprint, inspired by the
Lean version (#785, @ejgallego, Andrej Bauer)
[lsp] [rocq] Example of Ltac2 AST analysis using serlib's Analzyer
infra (@ejgallego, @jim-portegies, @DikieDick, #1058)
[lsp controller] Log internal errors to user-facing log
(@ejgallego, #1074)
[doc] Example typescript client connecting to the WASM-based lsp
server (@ejgallego, #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, #590)
[plugins] New plugin to dump document data (@ejgallego, Stefania
Dumbrava, #1075)
[fcc] New option --trace-file that will generate trace data for
visualizing with perfetto.dev (@ejgallego, AlexJ, Gaëtan Gilbert,
#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, #1077)
[vscode] Add config manager for handling client configuration
changes in the infoview. Add configuration option for number of
messages displayed (@Durbatuluk1701, #1067)
[wasm] Update interrupt patch to account for timeouts (@ejgallego,
Shachar Itzhaky, #1078)

Contributors

ejgallego, gbdrt, and 5 other contributors

Assets 3

16 Sep 18:18

ejgallego

0.2.4+9.1

CHANGES:

[js] [deps] Bump to findlib 1.9.8, use vanilla API for loading and
remove our own local wrapper (@ejgallego, #975).
[petanque] New petanque/ast and petanque/ast_at_pos
(@ejgallego, @JulesViennotFranca, #980)
[serlib] Support for generic Ast analyzers. This opens the door to
many feature requests such as syntax coloring, dependency
extraction, etc... (@ejgallego, @JulesViennotFranca, #981)
[fleche] Support "rocq" markdown delimiters in .mv files
(@ejgallego, #987)
[workspace] Support _RocqProject (@ejgallego, #988, fixes #934)
[lsp] [getDocument] Allow to get goals in one shot. We also
refactor the response type to accommodate different
meta-data. Note: (!) breaking change. (@ejgallego, #985, fixes
#862, thanks to the Alectryon team)
[lsp] Better error handling in URI parsing (@ejgallego, #994, thanks to
Adrien from Zulip)
[lsp] Better protocol-level handling for our non-standard Lang.Point
and Lang.Diagnostic types, via global flags that allow us to
choose the input/output representation for non-standard field such
as [Point.offset]. This ensures that leaks of these non-standard
fields are rarer. (@ejgallego, #995, cc #279, cc #2, thanks to
Adrien from Zulip)
[lsp] [completion] Rework completion configuration into a
coq-lsp.completion json object. The unicode_completion setting
is now deprecated, and has been replaced by
completion.unicode.enable (@ejgallego, #993)
[lsp] [completion] [vscode] Unicode completion commit characters
are now configurable via the server setting variable
completion.unicode.commit_chars. (@Durbatuluk1701, #993)
[goals] [config] New (global) option for goal display method
proof/goals: messages_follow_goal. If true, proof/goals
will show errors and messages for the same sentence goals are
shown; if false, it will always show errors and messages for the
specified position, if there is a Rocq sentence at hand
(@jpoiret, @ejgallego, #999, fixes: #941)
[coq] Install full state before parsing. Before we did only
Pcoq.unfreeze but that is not enough, in particular the call to
get_default_proof_mode will not be correct (@ejgallego, @pimotte,
#1011, fixes #656)
[misc] Don't depend on Jane Street's base (@patrick-nicodemus
@ejgallego, #1004)
[wasm worker] Add WebAssembly based worker based on waCoq. This is
now the default for the .vsix binary build. For now, we include
Rocq's Stdlib and Waterproof (@corwin-of-amber, @ejgallego,
@pimotte, #1008, cc #833, fixes #907, fixes #908, fixes #913)
[opam] Added x-maintenance-intent intent field. (@ejgallego,
#1020)
[lsp] [didOpen] languageId now takes priority over uri extension
in LSP didOpen. (@ejgallego, #1021, fixes #1005)
[coq] incorporate experimental coq-layout-engine printer, both in
client and server parts (@ejgallego, #668, see also #72 and
jscoq/jscoq#282 )
[lsp] [code] New notification $/coq/executionInformation which
will signal clients when rocq-lsp does intent to start to execute a
sentence. Experimentally, this is used to provide a red glow on
long-running commands in coq-lsp/VSCode, to provide better user
feedback on long-running commands (@ejgallego, suggested by
@jpoiret, #1002)
[lsp] [outline] Support Notation, Ltac and Ltac Notation in
outline entries (@ejgallego, #1025, fixes #632)

Contributors

corwin-of-amber, jpoiret, and 5 other contributors

Assets 3

16 Sep 18:16

ejgallego

0.2.4+9.0

CHANGES:

[js] [deps] Bump to findlib 1.9.8, use vanilla API for loading and
remove our own local wrapper (@ejgallego, #975).
[petanque] New petanque/ast and petanque/ast_at_pos
(@ejgallego, @JulesViennotFranca, #980)
[serlib] Support for generic Ast analyzers. This opens the door to
many feature requests such as syntax coloring, dependency
extraction, etc... (@ejgallego, @JulesViennotFranca, #981)
[fleche] Support "rocq" markdown delimiters in .mv files
(@ejgallego, #987)
[workspace] Support _RocqProject (@ejgallego, #988, fixes #934)
[lsp] [getDocument] Allow to get goals in one shot. We also
refactor the response type to accommodate different
meta-data. Note: (!) breaking change. (@ejgallego, #985, fixes
#862, thanks to the Alectryon team)
[lsp] Better error handling in URI parsing (@ejgallego, #994, thanks to
Adrien from Zulip)
[lsp] Better protocol-level handling for our non-standard Lang.Point
and Lang.Diagnostic types, via global flags that allow us to
choose the input/output representation for non-standard field such
as [Point.offset]. This ensures that leaks of these non-standard
fields are rarer. (@ejgallego, #995, cc #279, cc #2, thanks to
Adrien from Zulip)
[lsp] [completion] Rework completion configuration into a
coq-lsp.completion json object. The unicode_completion setting
is now deprecated, and has been replaced by
completion.unicode.enable (@ejgallego, #993)
[lsp] [completion] [vscode] Unicode completion commit characters
are now configurable via the server setting variable
completion.unicode.commit_chars. (@Durbatuluk1701, #993)
[goals] [config] New (global) option for goal display method
proof/goals: messages_follow_goal. If true, proof/goals
will show errors and messages for the same sentence goals are
shown; if false, it will always show errors and messages for the
specified position, if there is a Rocq sentence at hand
(@jpoiret, @ejgallego, #999, fixes: #941)
[coq] Install full state before parsing. Before we did only
Pcoq.unfreeze but that is not enough, in particular the call to
get_default_proof_mode will not be correct (@ejgallego, @pimotte,
#1011, fixes #656)
[misc] Don't depend on Jane Street's base (@patrick-nicodemus
@ejgallego, #1004)
[wasm worker] Add WebAssembly based worker based on waCoq. This is
now the default for the .vsix binary build. For now, we include
Rocq's Stdlib and Waterproof (@corwin-of-amber, @ejgallego,
@pimotte, #1008, cc #833, fixes #907, fixes #908, fixes #913)
[opam] Added x-maintenance-intent intent field. (@ejgallego,
#1020)
[lsp] [didOpen] languageId now takes priority over uri extension
in LSP didOpen. (@ejgallego, #1021, fixes #1005)
[coq] incorporate experimental coq-layout-engine printer, both in
client and server parts (@ejgallego, #668, see also #72 and
jscoq/jscoq#282 )
[lsp] [code] New notification $/coq/executionInformation which
will signal clients when rocq-lsp does intent to start to execute a
sentence. Experimentally, this is used to provide a red glow on
long-running commands in coq-lsp/VSCode, to provide better user
feedback on long-running commands (@ejgallego, suggested by
@jpoiret, #1002)
[lsp] [outline] Support Notation, Ltac and Ltac Notation in
outline entries (@ejgallego, #1025, fixes #632)

Contributors

corwin-of-amber, jpoiret, and 5 other contributors

Assets 3

16 Sep 18:11

ejgallego

0.2.4+8.20

CHANGES:

[js] [deps] Bump to findlib 1.9.8, use vanilla API for loading and
remove our own local wrapper (@ejgallego, #975).
[petanque] New petanque/ast and petanque/ast_at_pos
(@ejgallego, @JulesViennotFranca, #980)
[serlib] Support for generic Ast analyzers. This opens the door to
many feature requests such as syntax coloring, dependency
extraction, etc... (@ejgallego, @JulesViennotFranca, #981)
[fleche] Support "rocq" markdown delimiters in .mv files
(@ejgallego, #987)
[workspace] Support _RocqProject (@ejgallego, #988, fixes #934)
[lsp] [getDocument] Allow to get goals in one shot. We also
refactor the response type to accommodate different
meta-data. Note: (!) breaking change. (@ejgallego, #985, fixes
#862, thanks to the Alectryon team)
[lsp] Better error handling in URI parsing (@ejgallego, #994, thanks to
Adrien from Zulip)
[lsp] Better protocol-level handling for our non-standard Lang.Point
and Lang.Diagnostic types, via global flags that allow us to
choose the input/output representation for non-standard field such
as [Point.offset]. This ensures that leaks of these non-standard
fields are rarer. (@ejgallego, #995, cc #279, cc #2, thanks to
Adrien from Zulip)
[lsp] [completion] Rework completion configuration into a
coq-lsp.completion json object. The unicode_completion setting
is now deprecated, and has been replaced by
completion.unicode.enable (@ejgallego, #993)
[lsp] [completion] [vscode] Unicode completion commit characters
are now configurable via the server setting variable
completion.unicode.commit_chars. (@Durbatuluk1701, #993)
[goals] [config] New (global) option for goal display method
proof/goals: messages_follow_goal. If true, proof/goals
will show errors and messages for the same sentence goals are
shown; if false, it will always show errors and messages for the
specified position, if there is a Rocq sentence at hand
(@jpoiret, @ejgallego, #999, fixes: #941)
[coq] Install full state before parsing. Before we did only
Pcoq.unfreeze but that is not enough, in particular the call to
get_default_proof_mode will not be correct (@ejgallego, @pimotte,
#1011, fixes #656)
[misc] Don't depend on Jane Street's base (@patrick-nicodemus
@ejgallego, #1004)
[wasm worker] Add WebAssembly based worker based on waCoq. This is
now the default for the .vsix binary build. For now, we include
Rocq's Stdlib and Waterproof (@corwin-of-amber, @ejgallego,
@pimotte, #1008, cc #833, fixes #907, fixes #908, fixes #913)
[opam] Added x-maintenance-intent intent field. (@ejgallego,
#1020)
[lsp] [didOpen] languageId now takes priority over uri extension
in LSP didOpen. (@ejgallego, #1021, fixes #1005)
[coq] incorporate experimental coq-layout-engine printer, both in
client and server parts (@ejgallego, #668, see also #72 and
jscoq/jscoq#282 )
[lsp] [code] New notification $/coq/executionInformation which
will signal clients when rocq-lsp does intent to start to execute a
sentence. Experimentally, this is used to provide a red glow on
long-running commands in coq-lsp/VSCode, to provide better user
feedback on long-running commands (@ejgallego, suggested by
@jpoiret, #1002)
[lsp] [outline] Support Notation, Ltac and Ltac Notation in
outline entries (@ejgallego, #1025, fixes #632)

Contributors

corwin-of-amber, jpoiret, and 5 other contributors

Assets 3

04 Jun 14:36

ejgallego

0.2.3+9.0

CHANGES:

[fleche] fix quick fixes for errors being lost due to incorrect
handling of send_diags_extra_data (@ejgallego, #850)
[vscode] Syntax highlighting for Coq 8.17-8.20 (@4ever2, #872)
[build] Adapt to Coq -> Rocq renaming (@ejgallego, @proux, #879)
[js worker] Update js_of_ocaml to 5.9.1 , thanks a lot to Hugo
Heuzard for longstanding continued support of the jsCoq and coq-lsp
projects (@ejgallego, @hhugo, #881)
[js worker] Update stubs (@ejgallego, @hhugo, #881)
[js worker] Fix build for Coq -> Rocq renaming and stdlib split
(@ejgallego, #881)
[general] Adapt to Coq -> Rocq renaming (@ejgallego, @SkySkimmer,
#883)
[general] [js] Adapt to Rocq stdlib split (@ejgallego, #890)
[ci] Bump setup-ocaml to v3 (@ejgallego, #890)
[ci] [windows] Use Opam 2.2 to build on windows (@ejgallego, #815,
#890)
[petanque] petanque/start now fails when the theorem was parsed
but not successfully executed (@ejgallego, reported by @gbdrt,
#901, fixes #886)
[ci] Test Ocaml 5.3 (@ejgallego, #904)
[js worker] Add Shachar Itzhaky's trampoline patch; this greatly
reduces the Stack Overflow in the proof engine (@ejgallego,
@corwin-of-amber, #905)
[js worker] [build] Include Coq WaterProof in the default Web
Worker build (@ejgallego, waterproof team, #905, closes #888)
[vscode] [web] Fix web extension not exporting the coq-lsp
extension API (@ejgallego, reported by @amblafont, #911, fixes
#877)
[build] [general] Rename our internal Lsp library to
Fleche_lsp; this should help avoiding conflicts with the OCaml
lsp library (@ejgallego, reported by @blackbird1128, #912, fixes
#861)
[workspace] Remove support legacy ML-search path semantics. These
were basically unused since Coq 8.16. As a consequence, coq-lsp /
fcc don't accept the -I flag anymore, use OCAMLPATH or the
--ocamlpath= option to pass extra findlib paths. We still
respect the -I flag in _CoqMakefile (@ejgallego, #916)
[lsp] [debug] Respect $/setTrace call , refactor logging system,
and allow file logging of protocol traces again (@ejgallego, #919,
fixes #868)
[coq] Support Coq relocatable mode (@SkySkimmer, #891)
[ci] [deps] Remove support for OCaml 4.12 and 4.13, following
upstream's rocq-prover/rocq#20576 Note that these compiler versions have
been unsupported for a long time, please upgrade (@ejgallego, #951)
[hover] New option show_state_hash_on_hover that displays state
hash on hover for debug (@ejgallego, #954)
[doc] [faq] Updated FAQ to account for VSCoq 2 release in 2023,
thanks to Patrick Nicodemus for pointing out the outdated
documentation (@ejgallego, #846, fixes #817)
[vscode] [macos] Resolve keybinding conflict with Cmd+N and
Cmd+Enter, we now use Alt+N and Alt+Shift+Enter, (Andrei
Listochkin, #926)
[rocq] [fleche] Disable memprof-limits interruption backend by
default, as released Rocq versions are not safe yet. If you want to
enable it, you can still do it with the --int_backend=Mp command
line option (@ejgallego, #957, fixes #857, reported by @dariusf,
cc: rocq-prover/rocq#19177)
[lsp] [controller] Include Rocq feedback on request errors, using
the optional data field. This is useful to still be able to
obtain feedback messages such as debug messages even when a request
fails. This also opens the door to better protocol handling and
petanque integration (@ejgallego, #959, #961)
[petanque] Add feedback field to Run_result.t, this is important
for many use cases. We also return feedback on petanque errors.
(@ejgallego, @JulesViennotFranca, #960)
[petanque] new get_state_at_pos and get_root_state calls, that
allow to retrieve a petanque proof state from position
(@JulesViennotFranca, @ejgallego, #962)
[doc] [petanque] Document petanque v1, improve readme (@ejgallego,
#963)
[plugin] [astdump] Make the JSON and SEXP output into a line per
object by default (@blackbird1128, @ejgallego, #874)
[doc] [emacs] [protocol] Improve documentation for proof/goals,
add link to official emacs mode by Josselin Poiret (@ejgallego,
#969, thanks to @jpoiret, cc: #941)
[goals] Include range in proof/goals answer. This is useful for
clients willing to do highlighting (@ejgallego, @jpoiret, #970)

Contributors

corwin-of-amber, hhugo, and 10 other contributors

Assets 3

04 Jun 14:38

ejgallego

0.2.3+8.20

CHANGES:

[fleche] fix quick fixes for errors being lost due to incorrect
handling of send_diags_extra_data (@ejgallego, #850)
[vscode] Syntax highlighting for Coq 8.17-8.20 (@4ever2, #872)
[build] Adapt to Coq -> Rocq renaming (@ejgallego, @proux, #879)
[js worker] Update js_of_ocaml to 5.9.1 , thanks a lot to Hugo
Heuzard for longstanding continued support of the jsCoq and coq-lsp
projects (@ejgallego, @hhugo, #881)
[js worker] Update stubs (@ejgallego, @hhugo, #881)
[js worker] Fix build for Coq -> Rocq renaming and stdlib split
(@ejgallego, #881)
[general] Adapt to Coq -> Rocq renaming (@ejgallego, @SkySkimmer,
#883)
[general] [js] Adapt to Rocq stdlib split (@ejgallego, #890)
[ci] Bump setup-ocaml to v3 (@ejgallego, #890)
[ci] [windows] Use Opam 2.2 to build on windows (@ejgallego, #815,
#890)
[petanque] petanque/start now fails when the theorem was parsed
but not successfully executed (@ejgallego, reported by @gbdrt,
#901, fixes #886)
[ci] Test Ocaml 5.3 (@ejgallego, #904)
[js worker] Add Shachar Itzhaky's trampoline patch; this greatly
reduces the Stack Overflow in the proof engine (@ejgallego,
@corwin-of-amber, #905)
[js worker] [build] Include Coq WaterProof in the default Web
Worker build (@ejgallego, waterproof team, #905, closes #888)
[vscode] [web] Fix web extension not exporting the coq-lsp
extension API (@ejgallego, reported by @amblafont, #911, fixes
#877)
[build] [general] Rename our internal Lsp library to
Fleche_lsp; this should help avoiding conflicts with the OCaml
lsp library (@ejgallego, reported by @blackbird1128, #912, fixes
#861)
[workspace] Remove support legacy ML-search path semantics. These
were basically unused since Coq 8.16. As a consequence, coq-lsp /
fcc don't accept the -I flag anymore, use OCAMLPATH or the
--ocamlpath= option to pass extra findlib paths. We still
respect the -I flag in _CoqMakefile (@ejgallego, #916)
[lsp] [debug] Respect $/setTrace call , refactor logging system,
and allow file logging of protocol traces again (@ejgallego, #919,
fixes #868)
[coq] Support Coq relocatable mode (@SkySkimmer, #891)
[ci] [deps] Remove support for OCaml 4.12 and 4.13, following
upstream's rocq-prover/rocq#20576 Note that these compiler versions have
been unsupported for a long time, please upgrade (@ejgallego, #951)
[hover] New option show_state_hash_on_hover that displays state
hash on hover for debug (@ejgallego, #954)
[doc] [faq] Updated FAQ to account for VSCoq 2 release in 2023,
thanks to Patrick Nicodemus for pointing out the outdated
documentation (@ejgallego, #846, fixes #817)
[vscode] [macos] Resolve keybinding conflict with Cmd+N and
Cmd+Enter, we now use Alt+N and Alt+Shift+Enter, (Andrei
Listochkin, #926)
[rocq] [fleche] Disable memprof-limits interruption backend by
default, as released Rocq versions are not safe yet. If you want to
enable it, you can still do it with the --int_backend=Mp command
line option (@ejgallego, #957, fixes #857, reported by @dariusf,
cc: rocq-prover/rocq#19177)
[lsp] [controller] Include Rocq feedback on request errors, using
the optional data field. This is useful to still be able to
obtain feedback messages such as debug messages even when a request
fails. This also opens the door to better protocol handling and
petanque integration (@ejgallego, #959, #961)
[petanque] Add feedback field to Run_result.t, this is important
for many use cases. We also return feedback on petanque errors.
(@ejgallego, @JulesViennotFranca, #960)
[petanque] new get_state_at_pos and get_root_state calls, that
allow to retrieve a petanque proof state from position
(@JulesViennotFranca, @ejgallego, #962)
[doc] [petanque] Document petanque v1, improve readme (@ejgallego,
#963)
[plugin] [astdump] Make the JSON and SEXP output into a line per
object by default (@blackbird1128, @ejgallego, #874)
[doc] [emacs] [protocol] Improve documentation for proof/goals,
add link to official emacs mode by Josselin Poiret (@ejgallego,
#969, thanks to @jpoiret, cc: #941)
[goals] Include range in proof/goals answer. This is useful for
clients willing to do highlighting (@ejgallego, @jpoiret, #970)

Contributors

corwin-of-amber, hhugo, and 10 other contributors

Assets 3

04 Jun 14:42

ejgallego

0.2.3+8.19

CHANGES:

[fleche] fix quick fixes for errors being lost due to incorrect
handling of send_diags_extra_data (@ejgallego, #850)
[vscode] Syntax highlighting for Coq 8.17-8.20 (@4ever2, #872)
[build] Adapt to Coq -> Rocq renaming (@ejgallego, @proux, #879)
[js worker] Update js_of_ocaml to 5.9.1 , thanks a lot to Hugo
Heuzard for longstanding continued support of the jsCoq and coq-lsp
projects (@ejgallego, @hhugo, #881)
[js worker] Update stubs (@ejgallego, @hhugo, #881)
[js worker] Fix build for Coq -> Rocq renaming and stdlib split
(@ejgallego, #881)
[general] Adapt to Coq -> Rocq renaming (@ejgallego, @SkySkimmer,
#883)
[general] [js] Adapt to Rocq stdlib split (@ejgallego, #890)
[ci] Bump setup-ocaml to v3 (@ejgallego, #890)
[ci] [windows] Use Opam 2.2 to build on windows (@ejgallego, #815,
#890)
[petanque] petanque/start now fails when the theorem was parsed
but not successfully executed (@ejgallego, reported by @gbdrt,
#901, fixes #886)
[ci] Test Ocaml 5.3 (@ejgallego, #904)
[js worker] Add Shachar Itzhaky's trampoline patch; this greatly
reduces the Stack Overflow in the proof engine (@ejgallego,
@corwin-of-amber, #905)
[js worker] [build] Include Coq WaterProof in the default Web
Worker build (@ejgallego, waterproof team, #905, closes #888)
[vscode] [web] Fix web extension not exporting the coq-lsp
extension API (@ejgallego, reported by @amblafont, #911, fixes
#877)
[build] [general] Rename our internal Lsp library to
Fleche_lsp; this should help avoiding conflicts with the OCaml
lsp library (@ejgallego, reported by @blackbird1128, #912, fixes
#861)
[workspace] Remove support legacy ML-search path semantics. These
were basically unused since Coq 8.16. As a consequence, coq-lsp /
fcc don't accept the -I flag anymore, use OCAMLPATH or the
--ocamlpath= option to pass extra findlib paths. We still
respect the -I flag in _CoqMakefile (@ejgallego, #916)
[lsp] [debug] Respect $/setTrace call , refactor logging system,
and allow file logging of protocol traces again (@ejgallego, #919,
fixes #868)
[coq] Support Coq relocatable mode (@SkySkimmer, #891)
[ci] [deps] Remove support for OCaml 4.12 and 4.13, following
upstream's rocq-prover/rocq#20576 Note that these compiler versions have
been unsupported for a long time, please upgrade (@ejgallego, #951)
[hover] New option show_state_hash_on_hover that displays state
hash on hover for debug (@ejgallego, #954)
[doc] [faq] Updated FAQ to account for VSCoq 2 release in 2023,
thanks to Patrick Nicodemus for pointing out the outdated
documentation (@ejgallego, #846, fixes #817)
[vscode] [macos] Resolve keybinding conflict with Cmd+N and
Cmd+Enter, we now use Alt+N and Alt+Shift+Enter, (Andrei
Listochkin, #926)
[rocq] [fleche] Disable memprof-limits interruption backend by
default, as released Rocq versions are not safe yet. If you want to
enable it, you can still do it with the --int_backend=Mp command
line option (@ejgallego, #957, fixes #857, reported by @dariusf,
cc: rocq-prover/rocq#19177)
[lsp] [controller] Include Rocq feedback on request errors, using
the optional data field. This is useful to still be able to
obtain feedback messages such as debug messages even when a request
fails. This also opens the door to better protocol handling and
petanque integration (@ejgallego, #959, #961)
[petanque] Add feedback field to Run_result.t, this is important
for many use cases. We also return feedback on petanque errors.
(@ejgallego, @JulesViennotFranca, #960)
[petanque] new get_state_at_pos and get_root_state calls, that
allow to retrieve a petanque proof state from position
(@JulesViennotFranca, @ejgallego, #962)
[doc] [petanque] Document petanque v1, improve readme (@ejgallego,
#963)
[plugin] [astdump] Make the JSON and SEXP output into a line per
object by default (@blackbird1128, @ejgallego, #874)
[doc] [emacs] [protocol] Improve documentation for proof/goals,
add link to official emacs mode by Josselin Poiret (@ejgallego,
#969, thanks to @jpoiret, cc: #941)
[goals] Include range in proof/goals answer. This is useful for
clients willing to do highlighting (@ejgallego, @jpoiret, #970)

Contributors

corwin-of-amber, hhugo, and 10 other contributors

Assets 3

04 Jun 15:02

ejgallego

0.2.3+8.18

CHANGES:

[fleche] fix quick fixes for errors being lost due to incorrect
handling of send_diags_extra_data (@ejgallego, #850)
[vscode] Syntax highlighting for Coq 8.17-8.20 (@4ever2, #872)
[build] Adapt to Coq -> Rocq renaming (@ejgallego, @proux, #879)
[js worker] Update js_of_ocaml to 5.9.1 , thanks a lot to Hugo
Heuzard for longstanding continued support of the jsCoq and coq-lsp
projects (@ejgallego, @hhugo, #881)
[js worker] Update stubs (@ejgallego, @hhugo, #881)
[js worker] Fix build for Coq -> Rocq renaming and stdlib split
(@ejgallego, #881)
[general] Adapt to Coq -> Rocq renaming (@ejgallego, @SkySkimmer,
#883)
[general] [js] Adapt to Rocq stdlib split (@ejgallego, #890)
[ci] Bump setup-ocaml to v3 (@ejgallego, #890)
[ci] [windows] Use Opam 2.2 to build on windows (@ejgallego, #815,
#890)
[petanque] petanque/start now fails when the theorem was parsed
but not successfully executed (@ejgallego, reported by @gbdrt,
#901, fixes #886)
[ci] Test Ocaml 5.3 (@ejgallego, #904)
[js worker] Add Shachar Itzhaky's trampoline patch; this greatly
reduces the Stack Overflow in the proof engine (@ejgallego,
@corwin-of-amber, #905)
[js worker] [build] Include Coq WaterProof in the default Web
Worker build (@ejgallego, waterproof team, #905, closes #888)
[vscode] [web] Fix web extension not exporting the coq-lsp
extension API (@ejgallego, reported by @amblafont, #911, fixes
#877)
[build] [general] Rename our internal Lsp library to
Fleche_lsp; this should help avoiding conflicts with the OCaml
lsp library (@ejgallego, reported by @blackbird1128, #912, fixes
#861)
[workspace] Remove support legacy ML-search path semantics. These
were basically unused since Coq 8.16. As a consequence, coq-lsp /
fcc don't accept the -I flag anymore, use OCAMLPATH or the
--ocamlpath= option to pass extra findlib paths. We still
respect the -I flag in _CoqMakefile (@ejgallego, #916)
[lsp] [debug] Respect $/setTrace call , refactor logging system,
and allow file logging of protocol traces again (@ejgallego, #919,
fixes #868)
[coq] Support Coq relocatable mode (@SkySkimmer, #891)
[ci] [deps] Remove support for OCaml 4.12 and 4.13, following
upstream's rocq-prover/rocq#20576 Note that these compiler versions have
been unsupported for a long time, please upgrade (@ejgallego, #951)
[hover] New option show_state_hash_on_hover that displays state
hash on hover for debug (@ejgallego, #954)
[doc] [faq] Updated FAQ to account for VSCoq 2 release in 2023,
thanks to Patrick Nicodemus for pointing out the outdated
documentation (@ejgallego, #846, fixes #817)
[vscode] [macos] Resolve keybinding conflict with Cmd+N and
Cmd+Enter, we now use Alt+N and Alt+Shift+Enter, (Andrei
Listochkin, #926)
[rocq] [fleche] Disable memprof-limits interruption backend by
default, as released Rocq versions are not safe yet. If you want to
enable it, you can still do it with the --int_backend=Mp command
line option (@ejgallego, #957, fixes #857, reported by @dariusf,
cc: rocq-prover/rocq#19177)
[lsp] [controller] Include Rocq feedback on request errors, using
the optional data field. This is useful to still be able to
obtain feedback messages such as debug messages even when a request
fails. This also opens the door to better protocol handling and
petanque integration (@ejgallego, #959, #961)
[petanque] Add feedback field to Run_result.t, this is important
for many use cases. We also return feedback on petanque errors.
(@ejgallego, @JulesViennotFranca, #960)
[petanque] new get_state_at_pos and get_root_state calls, that
allow to retrieve a petanque proof state from position
(@JulesViennotFranca, @ejgallego, #962)
[doc] [petanque] Document petanque v1, improve readme (@ejgallego,
#963)
[plugin] [astdump] Make the JSON and SEXP output into a line per
object by default (@blackbird1128, @ejgallego, #874)
[doc] [emacs] [protocol] Improve documentation for proof/goals,
add link to official emacs mode by Josselin Poiret (@ejgallego,
#969, thanks to @jpoiret, cc: #941)
[goals] Include range in proof/goals answer. This is useful for
clients willing to do highlighting (@ejgallego, @jpoiret, #970)

Contributors

corwin-of-amber, hhugo, and 10 other contributors

Assets 3