Skip to content

[lsp] Cleanup of LSP IO#919

Merged
ejgallego merged 3 commits intomainfrom
fix_setTrace_off
Mar 17, 2025
Merged

[lsp] Cleanup of LSP IO#919
ejgallego merged 3 commits intomainfrom
fix_setTrace_off

Conversation

@ejgallego
Copy link
Collaborator

@ejgallego ejgallego commented Feb 16, 2025 •
edited
Loading

This is a step towards fixing an apparent bug in coq-lsp not respecting $/setTrace("off").

We consolidate tracing in Fleche.Io as tracing is really a Flèche facility.

We add a way to log to a file (as to help with #868 ), so we can see the low-level protocol format better. This corrects a minor regression from #130.

@ejgallego ejgallego added this to the 0.2.3 milestone Feb 16, 2025
@ejgallego ejgallego marked this pull request as ready for review March 17, 2025 13:39
@ejgallego
[lsp] Cleanup of LSP IO
880ad0b 
This is a step towards fixing an apparent bug in coq-lsp not
respecting `$/setTrace("off")`.
@ejgallego
[logging] Consolidate trace logging in Fleche.IO
7d5e799 
As of today, log tracing is part of Flèche, so we handle that with the
regular IO callback mechanisms in Flèche and remove it from the Lsp
module, where it was for historical reasons.
@ejgallego
[lsp] Allow to debug LSP traces to a file.
308d8ea 
Cc #868, restores functionality lost by #130
@ejgallego ejgallego merged commit 47d9724 into main Mar 17, 2025
15 checks passed
@ejgallego ejgallego deleted the fix_setTrace_off branch March 17, 2025 22:22
@ejgallego ejgallego mentioned this pull request Jun 4, 2025
Merged
ejgallego added a commit to ejgallego/opam-repository that referenced this pull request Jun 4, 2025
@ejgallego
[new release] coq-lsp (0.2.3+8.20)
1355ba2 
CHANGES:

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

 - [fleche] fix quick fixes for errors being lost due to incorrect
   handling of `send_diags_extra_data` (@ejgallego, rocq-community/rocq-lsp#850)
 - [vscode] Syntax highlighting for Coq 8.17-8.20 (@4ever2, rocq-community/rocq-lsp#872)
 - [build] Adapt to Coq -> Rocq renaming (@ejgallego, @proux, rocq-community/rocq-lsp#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, rocq-community/rocq-lsp#881)
 - [js worker] Update stubs (@ejgallego, @hhugo, rocq-community/rocq-lsp#881)
 - [js worker] Fix build for Coq -> Rocq renaming and stdlib split
   (@ejgallego, rocq-community/rocq-lsp#881)
 - [general] Adapt to Coq -> Rocq renaming (@ejgallego, @SkySkimmer,
   rocq-community/rocq-lsp#883)
 - [general] [js] Adapt to Rocq stdlib split (@ejgallego, rocq-community/rocq-lsp#890)
 - [ci] Bump setup-ocaml to v3 (@ejgallego, rocq-community/rocq-lsp#890)
 - [ci] [windows] Use Opam 2.2 to build on windows (@ejgallego, rocq-community/rocq-lsp#815,
   rocq-community/rocq-lsp#890)
 - [petanque] `petanque/start` now fails when the theorem was parsed
   but not successfully executed (@ejgallego, reported by @gbdrt,
   rocq-community/rocq-lsp#901, fixes rocq-community/rocq-lsp#886)
 - [ci] Test Ocaml 5.3 (@ejgallego, rocq-community/rocq-lsp#904)
 - [js worker] Add Shachar Itzhaky's trampoline patch; this greatly
   reduces the Stack Overflow in the proof engine (@ejgallego,
   @corwin-of-amber, rocq-community/rocq-lsp#905)
 - [js worker] [build] Include Coq WaterProof in the default Web
   Worker build (@ejgallego, waterproof team, rocq-community/rocq-lsp#905, closes rocq-community/rocq-lsp#888)
 - [vscode] [web] Fix web extension not exporting the coq-lsp
   extension API (@ejgallego, reported by @amblafont, rocq-community/rocq-lsp#911, fixes
   rocq-community/rocq-lsp#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, rocq-community/rocq-lsp#912, fixes
   rocq-community/rocq-lsp#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, rocq-community/rocq-lsp#916)
 - [lsp] [debug] Respect `$/setTrace` call , refactor logging system,
   and allow file logging of protocol traces again (@ejgallego, rocq-community/rocq-lsp#919,
   fixes rocq-community/rocq-lsp#868)
 - [coq] Support Coq relocatable mode (@SkySkimmer, rocq-community/rocq-lsp#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, rocq-community/rocq-lsp#951)
 - [hover] New option `show_state_hash_on_hover` that displays state
    hash on hover for debug (@ejgallego, rocq-community/rocq-lsp#954)
 - [doc] [faq] Updated FAQ to account for VSCoq 2 release in 2023,
   thanks to Patrick Nicodemus for pointing out the outdated
   documentation (@ejgallego, rocq-community/rocq-lsp#846, fixes rocq-community/rocq-lsp#817)
 - [vscode] [macos] Resolve keybinding conflict with Cmd+N and
   Cmd+Enter, we now use Alt+N and Alt+Shift+Enter, (Andrei
   Listochkin, rocq-community/rocq-lsp#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, rocq-community/rocq-lsp#957, fixes rocq-community/rocq-lsp#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, rocq-community/rocq-lsp#959, rocq-community/rocq-lsp#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, rocq-community/rocq-lsp#960)
 - [petanque] new `get_state_at_pos` and `get_root_state` calls, that
   allow to retrieve a petanque proof state from position
   (@JulesViennotFranca, @ejgallego, rocq-community/rocq-lsp#962)
 - [doc] [petanque] Document petanque v1, improve readme (@ejgallego,
   rocq-community/rocq-lsp#963)
 - [plugin] [astdump] Make the JSON and SEXP output into a line per
   object by default (@blackbird1128, @ejgallego, rocq-community/rocq-lsp#874)
 - [doc] [emacs] [protocol] Improve documentation for `proof/goals`,
   add link to official emacs mode by Josselin Poiret (@ejgallego,
   rocq-community/rocq-lsp#969, thanks to @jpoiret, cc: rocq-community/rocq-lsp#941)
 - [goals] Include `range` in `proof/goals` answer. This is useful for
   clients willing to do highlighting (@ejgallego, @jpoiret, rocq-community/rocq-lsp#970)
@ejgallego ejgallego mentioned this pull request Jun 4, 2025
Merged
ejgallego added a commit to ejgallego/opam-repository that referenced this pull request Jun 4, 2025
@ejgallego
[new release] coq-lsp (0.2.3+8.19)
7e4149c 
CHANGES:

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

 - [fleche] fix quick fixes for errors being lost due to incorrect
   handling of `send_diags_extra_data` (@ejgallego, rocq-community/rocq-lsp#850)
 - [vscode] Syntax highlighting for Coq 8.17-8.20 (@4ever2, rocq-community/rocq-lsp#872)
 - [build] Adapt to Coq -> Rocq renaming (@ejgallego, @proux, rocq-community/rocq-lsp#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, rocq-community/rocq-lsp#881)
 - [js worker] Update stubs (@ejgallego, @hhugo, rocq-community/rocq-lsp#881)
 - [js worker] Fix build for Coq -> Rocq renaming and stdlib split
   (@ejgallego, rocq-community/rocq-lsp#881)
 - [general] Adapt to Coq -> Rocq renaming (@ejgallego, @SkySkimmer,
   rocq-community/rocq-lsp#883)
 - [general] [js] Adapt to Rocq stdlib split (@ejgallego, rocq-community/rocq-lsp#890)
 - [ci] Bump setup-ocaml to v3 (@ejgallego, rocq-community/rocq-lsp#890)
 - [ci] [windows] Use Opam 2.2 to build on windows (@ejgallego, rocq-community/rocq-lsp#815,
   rocq-community/rocq-lsp#890)
 - [petanque] `petanque/start` now fails when the theorem was parsed
   but not successfully executed (@ejgallego, reported by @gbdrt,
   rocq-community/rocq-lsp#901, fixes rocq-community/rocq-lsp#886)
 - [ci] Test Ocaml 5.3 (@ejgallego, rocq-community/rocq-lsp#904)
 - [js worker] Add Shachar Itzhaky's trampoline patch; this greatly
   reduces the Stack Overflow in the proof engine (@ejgallego,
   @corwin-of-amber, rocq-community/rocq-lsp#905)
 - [js worker] [build] Include Coq WaterProof in the default Web
   Worker build (@ejgallego, waterproof team, rocq-community/rocq-lsp#905, closes rocq-community/rocq-lsp#888)
 - [vscode] [web] Fix web extension not exporting the coq-lsp
   extension API (@ejgallego, reported by @amblafont, rocq-community/rocq-lsp#911, fixes
   rocq-community/rocq-lsp#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, rocq-community/rocq-lsp#912, fixes
   rocq-community/rocq-lsp#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, rocq-community/rocq-lsp#916)
 - [lsp] [debug] Respect `$/setTrace` call , refactor logging system,
   and allow file logging of protocol traces again (@ejgallego, rocq-community/rocq-lsp#919,
   fixes rocq-community/rocq-lsp#868)
 - [coq] Support Coq relocatable mode (@SkySkimmer, rocq-community/rocq-lsp#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, rocq-community/rocq-lsp#951)
 - [hover] New option `show_state_hash_on_hover` that displays state
    hash on hover for debug (@ejgallego, rocq-community/rocq-lsp#954)
 - [doc] [faq] Updated FAQ to account for VSCoq 2 release in 2023,
   thanks to Patrick Nicodemus for pointing out the outdated
   documentation (@ejgallego, rocq-community/rocq-lsp#846, fixes rocq-community/rocq-lsp#817)
 - [vscode] [macos] Resolve keybinding conflict with Cmd+N and
   Cmd+Enter, we now use Alt+N and Alt+Shift+Enter, (Andrei
   Listochkin, rocq-community/rocq-lsp#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, rocq-community/rocq-lsp#957, fixes rocq-community/rocq-lsp#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, rocq-community/rocq-lsp#959, rocq-community/rocq-lsp#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, rocq-community/rocq-lsp#960)
 - [petanque] new `get_state_at_pos` and `get_root_state` calls, that
   allow to retrieve a petanque proof state from position
   (@JulesViennotFranca, @ejgallego, rocq-community/rocq-lsp#962)
 - [doc] [petanque] Document petanque v1, improve readme (@ejgallego,
   rocq-community/rocq-lsp#963)
 - [plugin] [astdump] Make the JSON and SEXP output into a line per
   object by default (@blackbird1128, @ejgallego, rocq-community/rocq-lsp#874)
 - [doc] [emacs] [protocol] Improve documentation for `proof/goals`,
   add link to official emacs mode by Josselin Poiret (@ejgallego,
   rocq-community/rocq-lsp#969, thanks to @jpoiret, cc: rocq-community/rocq-lsp#941)
 - [goals] Include `range` in `proof/goals` answer. This is useful for
   clients willing to do highlighting (@ejgallego, @jpoiret, rocq-community/rocq-lsp#970)
@ejgallego ejgallego mentioned this pull request Jun 4, 2025
Merged
ejgallego added a commit to ejgallego/opam-repository that referenced this pull request Jun 4, 2025
@ejgallego
[new release] coq-lsp (0.2.3+8.18)
4052cf1 
CHANGES:

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

 - [fleche] fix quick fixes for errors being lost due to incorrect
   handling of `send_diags_extra_data` (@ejgallego, rocq-community/rocq-lsp#850)
 - [vscode] Syntax highlighting for Coq 8.17-8.20 (@4ever2, rocq-community/rocq-lsp#872)
 - [build] Adapt to Coq -> Rocq renaming (@ejgallego, @proux, rocq-community/rocq-lsp#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, rocq-community/rocq-lsp#881)
 - [js worker] Update stubs (@ejgallego, @hhugo, rocq-community/rocq-lsp#881)
 - [js worker] Fix build for Coq -> Rocq renaming and stdlib split
   (@ejgallego, rocq-community/rocq-lsp#881)
 - [general] Adapt to Coq -> Rocq renaming (@ejgallego, @SkySkimmer,
   rocq-community/rocq-lsp#883)
 - [general] [js] Adapt to Rocq stdlib split (@ejgallego, rocq-community/rocq-lsp#890)
 - [ci] Bump setup-ocaml to v3 (@ejgallego, rocq-community/rocq-lsp#890)
 - [ci] [windows] Use Opam 2.2 to build on windows (@ejgallego, rocq-community/rocq-lsp#815,
   rocq-community/rocq-lsp#890)
 - [petanque] `petanque/start` now fails when the theorem was parsed
   but not successfully executed (@ejgallego, reported by @gbdrt,
   rocq-community/rocq-lsp#901, fixes rocq-community/rocq-lsp#886)
 - [ci] Test Ocaml 5.3 (@ejgallego, rocq-community/rocq-lsp#904)
 - [js worker] Add Shachar Itzhaky's trampoline patch; this greatly
   reduces the Stack Overflow in the proof engine (@ejgallego,
   @corwin-of-amber, rocq-community/rocq-lsp#905)
 - [js worker] [build] Include Coq WaterProof in the default Web
   Worker build (@ejgallego, waterproof team, rocq-community/rocq-lsp#905, closes rocq-community/rocq-lsp#888)
 - [vscode] [web] Fix web extension not exporting the coq-lsp
   extension API (@ejgallego, reported by @amblafont, rocq-community/rocq-lsp#911, fixes
   rocq-community/rocq-lsp#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, rocq-community/rocq-lsp#912, fixes
   rocq-community/rocq-lsp#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, rocq-community/rocq-lsp#916)
 - [lsp] [debug] Respect `$/setTrace` call , refactor logging system,
   and allow file logging of protocol traces again (@ejgallego, rocq-community/rocq-lsp#919,
   fixes rocq-community/rocq-lsp#868)
 - [coq] Support Coq relocatable mode (@SkySkimmer, rocq-community/rocq-lsp#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, rocq-community/rocq-lsp#951)
 - [hover] New option `show_state_hash_on_hover` that displays state
    hash on hover for debug (@ejgallego, rocq-community/rocq-lsp#954)
 - [doc] [faq] Updated FAQ to account for VSCoq 2 release in 2023,
   thanks to Patrick Nicodemus for pointing out the outdated
   documentation (@ejgallego, rocq-community/rocq-lsp#846, fixes rocq-community/rocq-lsp#817)
 - [vscode] [macos] Resolve keybinding conflict with Cmd+N and
   Cmd+Enter, we now use Alt+N and Alt+Shift+Enter, (Andrei
   Listochkin, rocq-community/rocq-lsp#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, rocq-community/rocq-lsp#957, fixes rocq-community/rocq-lsp#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, rocq-community/rocq-lsp#959, rocq-community/rocq-lsp#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, rocq-community/rocq-lsp#960)
 - [petanque] new `get_state_at_pos` and `get_root_state` calls, that
   allow to retrieve a petanque proof state from position
   (@JulesViennotFranca, @ejgallego, rocq-community/rocq-lsp#962)
 - [doc] [petanque] Document petanque v1, improve readme (@ejgallego,
   rocq-community/rocq-lsp#963)
 - [plugin] [astdump] Make the JSON and SEXP output into a line per
   object by default (@blackbird1128, @ejgallego, rocq-community/rocq-lsp#874)
 - [doc] [emacs] [protocol] Improve documentation for `proof/goals`,
   add link to official emacs mode by Josselin Poiret (@ejgallego,
   rocq-community/rocq-lsp#969, thanks to @jpoiret, cc: rocq-community/rocq-lsp#941)
 - [goals] Include `range` in `proof/goals` answer. This is useful for
   clients willing to do highlighting (@ejgallego, @jpoiret, rocq-community/rocq-lsp#970)
@ejgallego ejgallego mentioned this pull request Jun 4, 2025
Merged
ejgallego added a commit to ejgallego/opam-repository that referenced this pull request Jun 4, 2025
@ejgallego
[new release] coq-lsp (0.2.3+8.17)
2416148 
CHANGES:

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

 - [fleche] fix quick fixes for errors being lost due to incorrect
   handling of `send_diags_extra_data` (@ejgallego, rocq-community/rocq-lsp#850)
 - [vscode] Syntax highlighting for Coq 8.17-8.20 (@4ever2, rocq-community/rocq-lsp#872)
 - [build] Adapt to Coq -> Rocq renaming (@ejgallego, @proux, rocq-community/rocq-lsp#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, rocq-community/rocq-lsp#881)
 - [js worker] Update stubs (@ejgallego, @hhugo, rocq-community/rocq-lsp#881)
 - [js worker] Fix build for Coq -> Rocq renaming and stdlib split
   (@ejgallego, rocq-community/rocq-lsp#881)
 - [general] Adapt to Coq -> Rocq renaming (@ejgallego, @SkySkimmer,
   rocq-community/rocq-lsp#883)
 - [general] [js] Adapt to Rocq stdlib split (@ejgallego, rocq-community/rocq-lsp#890)
 - [ci] Bump setup-ocaml to v3 (@ejgallego, rocq-community/rocq-lsp#890)
 - [ci] [windows] Use Opam 2.2 to build on windows (@ejgallego, rocq-community/rocq-lsp#815,
   rocq-community/rocq-lsp#890)
 - [petanque] `petanque/start` now fails when the theorem was parsed
   but not successfully executed (@ejgallego, reported by @gbdrt,
   rocq-community/rocq-lsp#901, fixes rocq-community/rocq-lsp#886)
 - [ci] Test Ocaml 5.3 (@ejgallego, rocq-community/rocq-lsp#904)
 - [js worker] Add Shachar Itzhaky's trampoline patch; this greatly
   reduces the Stack Overflow in the proof engine (@ejgallego,
   @corwin-of-amber, rocq-community/rocq-lsp#905)
 - [js worker] [build] Include Coq WaterProof in the default Web
   Worker build (@ejgallego, waterproof team, rocq-community/rocq-lsp#905, closes rocq-community/rocq-lsp#888)
 - [vscode] [web] Fix web extension not exporting the coq-lsp
   extension API (@ejgallego, reported by @amblafont, rocq-community/rocq-lsp#911, fixes
   rocq-community/rocq-lsp#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, rocq-community/rocq-lsp#912, fixes
   rocq-community/rocq-lsp#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, rocq-community/rocq-lsp#916)
 - [lsp] [debug] Respect `$/setTrace` call , refactor logging system,
   and allow file logging of protocol traces again (@ejgallego, rocq-community/rocq-lsp#919,
   fixes rocq-community/rocq-lsp#868)
 - [coq] Support Coq relocatable mode (@SkySkimmer, rocq-community/rocq-lsp#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, rocq-community/rocq-lsp#951)
 - [hover] New option `show_state_hash_on_hover` that displays state
    hash on hover for debug (@ejgallego, rocq-community/rocq-lsp#954)
 - [doc] [faq] Updated FAQ to account for VSCoq 2 release in 2023,
   thanks to Patrick Nicodemus for pointing out the outdated
   documentation (@ejgallego, rocq-community/rocq-lsp#846, fixes rocq-community/rocq-lsp#817)
 - [vscode] [macos] Resolve keybinding conflict with Cmd+N and
   Cmd+Enter, we now use Alt+N and Alt+Shift+Enter, (Andrei
   Listochkin, rocq-community/rocq-lsp#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, rocq-community/rocq-lsp#957, fixes rocq-community/rocq-lsp#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, rocq-community/rocq-lsp#959, rocq-community/rocq-lsp#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, rocq-community/rocq-lsp#960)
 - [petanque] new `get_state_at_pos` and `get_root_state` calls, that
   allow to retrieve a petanque proof state from position
   (@JulesViennotFranca, @ejgallego, rocq-community/rocq-lsp#962)
 - [doc] [petanque] Document petanque v1, improve readme (@ejgallego,
   rocq-community/rocq-lsp#963)
 - [plugin] [astdump] Make the JSON and SEXP output into a line per
   object by default (@blackbird1128, @ejgallego, rocq-community/rocq-lsp#874)
 - [doc] [emacs] [protocol] Improve documentation for `proof/goals`,
   add link to official emacs mode by Josselin Poiret (@ejgallego,
   rocq-community/rocq-lsp#969, thanks to @jpoiret, cc: rocq-community/rocq-lsp#941)
 - [goals] Include `range` in `proof/goals` answer. This is useful for
   clients willing to do highlighting (@ejgallego, @jpoiret, rocq-community/rocq-lsp#970)
@ejgallego ejgallego mentioned this pull request Jun 4, 2025
Merged
ejgallego added a commit to ejgallego/opam-repository that referenced this pull request Jun 4, 2025
@ejgallego
[new release] coq-lsp (0.2.3+9.0)
6f267ea 
CHANGES:

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

 - [fleche] fix quick fixes for errors being lost due to incorrect
   handling of `send_diags_extra_data` (@ejgallego, rocq-community/rocq-lsp#850)
 - [vscode] Syntax highlighting for Coq 8.17-8.20 (@4ever2, rocq-community/rocq-lsp#872)
 - [build] Adapt to Coq -> Rocq renaming (@ejgallego, @proux, rocq-community/rocq-lsp#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, rocq-community/rocq-lsp#881)
 - [js worker] Update stubs (@ejgallego, @hhugo, rocq-community/rocq-lsp#881)
 - [js worker] Fix build for Coq -> Rocq renaming and stdlib split
   (@ejgallego, rocq-community/rocq-lsp#881)
 - [general] Adapt to Coq -> Rocq renaming (@ejgallego, @SkySkimmer,
   rocq-community/rocq-lsp#883)
 - [general] [js] Adapt to Rocq stdlib split (@ejgallego, rocq-community/rocq-lsp#890)
 - [ci] Bump setup-ocaml to v3 (@ejgallego, rocq-community/rocq-lsp#890)
 - [ci] [windows] Use Opam 2.2 to build on windows (@ejgallego, rocq-community/rocq-lsp#815,
   rocq-community/rocq-lsp#890)
 - [petanque] `petanque/start` now fails when the theorem was parsed
   but not successfully executed (@ejgallego, reported by @gbdrt,
   rocq-community/rocq-lsp#901, fixes rocq-community/rocq-lsp#886)
 - [ci] Test Ocaml 5.3 (@ejgallego, rocq-community/rocq-lsp#904)
 - [js worker] Add Shachar Itzhaky's trampoline patch; this greatly
   reduces the Stack Overflow in the proof engine (@ejgallego,
   @corwin-of-amber, rocq-community/rocq-lsp#905)
 - [js worker] [build] Include Coq WaterProof in the default Web
   Worker build (@ejgallego, waterproof team, rocq-community/rocq-lsp#905, closes rocq-community/rocq-lsp#888)
 - [vscode] [web] Fix web extension not exporting the coq-lsp
   extension API (@ejgallego, reported by @amblafont, rocq-community/rocq-lsp#911, fixes
   rocq-community/rocq-lsp#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, rocq-community/rocq-lsp#912, fixes
   rocq-community/rocq-lsp#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, rocq-community/rocq-lsp#916)
 - [lsp] [debug] Respect `$/setTrace` call , refactor logging system,
   and allow file logging of protocol traces again (@ejgallego, rocq-community/rocq-lsp#919,
   fixes rocq-community/rocq-lsp#868)
 - [coq] Support Coq relocatable mode (@SkySkimmer, rocq-community/rocq-lsp#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, rocq-community/rocq-lsp#951)
 - [hover] New option `show_state_hash_on_hover` that displays state
    hash on hover for debug (@ejgallego, rocq-community/rocq-lsp#954)
 - [doc] [faq] Updated FAQ to account for VSCoq 2 release in 2023,
   thanks to Patrick Nicodemus for pointing out the outdated
   documentation (@ejgallego, rocq-community/rocq-lsp#846, fixes rocq-community/rocq-lsp#817)
 - [vscode] [macos] Resolve keybinding conflict with Cmd+N and
   Cmd+Enter, we now use Alt+N and Alt+Shift+Enter, (Andrei
   Listochkin, rocq-community/rocq-lsp#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, rocq-community/rocq-lsp#957, fixes rocq-community/rocq-lsp#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, rocq-community/rocq-lsp#959, rocq-community/rocq-lsp#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, rocq-community/rocq-lsp#960)
 - [petanque] new `get_state_at_pos` and `get_root_state` calls, that
   allow to retrieve a petanque proof state from position
   (@JulesViennotFranca, @ejgallego, rocq-community/rocq-lsp#962)
 - [doc] [petanque] Document petanque v1, improve readme (@ejgallego,
   rocq-community/rocq-lsp#963)
 - [plugin] [astdump] Make the JSON and SEXP output into a line per
   object by default (@blackbird1128, @ejgallego, rocq-community/rocq-lsp#874)
 - [doc] [emacs] [protocol] Improve documentation for `proof/goals`,
   add link to official emacs mode by Josselin Poiret (@ejgallego,
   rocq-community/rocq-lsp#969, thanks to @jpoiret, cc: rocq-community/rocq-lsp#941)
 - [goals] Include `range` in `proof/goals` answer. This is useful for
   clients willing to do highlighting (@ejgallego, @jpoiret, rocq-community/rocq-lsp#970)
dkalinichenko-js pushed a commit to dkalinichenko-js/opam-repository that referenced this pull request Jun 10, 2025
@ejgallego @d-kalinichenko
[new release] coq-lsp (0.2.3+9.0)
dc1cd64 
CHANGES:

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

 - [fleche] fix quick fixes for errors being lost due to incorrect
   handling of `send_diags_extra_data` (@ejgallego, rocq-community/rocq-lsp#850)
 - [vscode] Syntax highlighting for Coq 8.17-8.20 (@4ever2, rocq-community/rocq-lsp#872)
 - [build] Adapt to Coq -> Rocq renaming (@ejgallego, @proux, rocq-community/rocq-lsp#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, rocq-community/rocq-lsp#881)
 - [js worker] Update stubs (@ejgallego, @hhugo, rocq-community/rocq-lsp#881)
 - [js worker] Fix build for Coq -> Rocq renaming and stdlib split
   (@ejgallego, rocq-community/rocq-lsp#881)
 - [general] Adapt to Coq -> Rocq renaming (@ejgallego, @SkySkimmer,
   rocq-community/rocq-lsp#883)
 - [general] [js] Adapt to Rocq stdlib split (@ejgallego, rocq-community/rocq-lsp#890)
 - [ci] Bump setup-ocaml to v3 (@ejgallego, rocq-community/rocq-lsp#890)
 - [ci] [windows] Use Opam 2.2 to build on windows (@ejgallego, rocq-community/rocq-lsp#815,
   rocq-community/rocq-lsp#890)
 - [petanque] `petanque/start` now fails when the theorem was parsed
   but not successfully executed (@ejgallego, reported by @gbdrt,
   rocq-community/rocq-lsp#901, fixes rocq-community/rocq-lsp#886)
 - [ci] Test Ocaml 5.3 (@ejgallego, rocq-community/rocq-lsp#904)
 - [js worker] Add Shachar Itzhaky's trampoline patch; this greatly
   reduces the Stack Overflow in the proof engine (@ejgallego,
   @corwin-of-amber, rocq-community/rocq-lsp#905)
 - [js worker] [build] Include Coq WaterProof in the default Web
   Worker build (@ejgallego, waterproof team, rocq-community/rocq-lsp#905, closes rocq-community/rocq-lsp#888)
 - [vscode] [web] Fix web extension not exporting the coq-lsp
   extension API (@ejgallego, reported by @amblafont, rocq-community/rocq-lsp#911, fixes
   rocq-community/rocq-lsp#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, rocq-community/rocq-lsp#912, fixes
   rocq-community/rocq-lsp#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, rocq-community/rocq-lsp#916)
 - [lsp] [debug] Respect `$/setTrace` call , refactor logging system,
   and allow file logging of protocol traces again (@ejgallego, rocq-community/rocq-lsp#919,
   fixes rocq-community/rocq-lsp#868)
 - [coq] Support Coq relocatable mode (@SkySkimmer, rocq-community/rocq-lsp#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, rocq-community/rocq-lsp#951)
 - [hover] New option `show_state_hash_on_hover` that displays state
    hash on hover for debug (@ejgallego, rocq-community/rocq-lsp#954)
 - [doc] [faq] Updated FAQ to account for VSCoq 2 release in 2023,
   thanks to Patrick Nicodemus for pointing out the outdated
   documentation (@ejgallego, rocq-community/rocq-lsp#846, fixes rocq-community/rocq-lsp#817)
 - [vscode] [macos] Resolve keybinding conflict with Cmd+N and
   Cmd+Enter, we now use Alt+N and Alt+Shift+Enter, (Andrei
   Listochkin, rocq-community/rocq-lsp#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, rocq-community/rocq-lsp#957, fixes rocq-community/rocq-lsp#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, rocq-community/rocq-lsp#959, rocq-community/rocq-lsp#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, rocq-community/rocq-lsp#960)
 - [petanque] new `get_state_at_pos` and `get_root_state` calls, that
   allow to retrieve a petanque proof state from position
   (@JulesViennotFranca, @ejgallego, rocq-community/rocq-lsp#962)
 - [doc] [petanque] Document petanque v1, improve readme (@ejgallego,
   rocq-community/rocq-lsp#963)
 - [plugin] [astdump] Make the JSON and SEXP output into a line per
   object by default (@blackbird1128, @ejgallego, rocq-community/rocq-lsp#874)
 - [doc] [emacs] [protocol] Improve documentation for `proof/goals`,
   add link to official emacs mode by Josselin Poiret (@ejgallego,
   rocq-community/rocq-lsp#969, thanks to @jpoiret, cc: rocq-community/rocq-lsp#941)
 - [goals] Include `range` in `proof/goals` answer. This is useful for
   clients willing to do highlighting (@ejgallego, @jpoiret, rocq-community/rocq-lsp#970)
dkalinichenko-js pushed a commit to dkalinichenko-js/opam-repository that referenced this pull request Jun 10, 2025
@ejgallego @d-kalinichenko
[new release] coq-lsp (0.2.3+8.17)
5c30b17 
CHANGES:

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

 - [fleche] fix quick fixes for errors being lost due to incorrect
   handling of `send_diags_extra_data` (@ejgallego, rocq-community/rocq-lsp#850)
 - [vscode] Syntax highlighting for Coq 8.17-8.20 (@4ever2, rocq-community/rocq-lsp#872)
 - [build] Adapt to Coq -> Rocq renaming (@ejgallego, @proux, rocq-community/rocq-lsp#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, rocq-community/rocq-lsp#881)
 - [js worker] Update stubs (@ejgallego, @hhugo, rocq-community/rocq-lsp#881)
 - [js worker] Fix build for Coq -> Rocq renaming and stdlib split
   (@ejgallego, rocq-community/rocq-lsp#881)
 - [general] Adapt to Coq -> Rocq renaming (@ejgallego, @SkySkimmer,
   rocq-community/rocq-lsp#883)
 - [general] [js] Adapt to Rocq stdlib split (@ejgallego, rocq-community/rocq-lsp#890)
 - [ci] Bump setup-ocaml to v3 (@ejgallego, rocq-community/rocq-lsp#890)
 - [ci] [windows] Use Opam 2.2 to build on windows (@ejgallego, rocq-community/rocq-lsp#815,
   rocq-community/rocq-lsp#890)
 - [petanque] `petanque/start` now fails when the theorem was parsed
   but not successfully executed (@ejgallego, reported by @gbdrt,
   rocq-community/rocq-lsp#901, fixes rocq-community/rocq-lsp#886)
 - [ci] Test Ocaml 5.3 (@ejgallego, rocq-community/rocq-lsp#904)
 - [js worker] Add Shachar Itzhaky's trampoline patch; this greatly
   reduces the Stack Overflow in the proof engine (@ejgallego,
   @corwin-of-amber, rocq-community/rocq-lsp#905)
 - [js worker] [build] Include Coq WaterProof in the default Web
   Worker build (@ejgallego, waterproof team, rocq-community/rocq-lsp#905, closes rocq-community/rocq-lsp#888)
 - [vscode] [web] Fix web extension not exporting the coq-lsp
   extension API (@ejgallego, reported by @amblafont, rocq-community/rocq-lsp#911, fixes
   rocq-community/rocq-lsp#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, rocq-community/rocq-lsp#912, fixes
   rocq-community/rocq-lsp#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, rocq-community/rocq-lsp#916)
 - [lsp] [debug] Respect `$/setTrace` call , refactor logging system,
   and allow file logging of protocol traces again (@ejgallego, rocq-community/rocq-lsp#919,
   fixes rocq-community/rocq-lsp#868)
 - [coq] Support Coq relocatable mode (@SkySkimmer, rocq-community/rocq-lsp#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, rocq-community/rocq-lsp#951)
 - [hover] New option `show_state_hash_on_hover` that displays state
    hash on hover for debug (@ejgallego, rocq-community/rocq-lsp#954)
 - [doc] [faq] Updated FAQ to account for VSCoq 2 release in 2023,
   thanks to Patrick Nicodemus for pointing out the outdated
   documentation (@ejgallego, rocq-community/rocq-lsp#846, fixes rocq-community/rocq-lsp#817)
 - [vscode] [macos] Resolve keybinding conflict with Cmd+N and
   Cmd+Enter, we now use Alt+N and Alt+Shift+Enter, (Andrei
   Listochkin, rocq-community/rocq-lsp#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, rocq-community/rocq-lsp#957, fixes rocq-community/rocq-lsp#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, rocq-community/rocq-lsp#959, rocq-community/rocq-lsp#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, rocq-community/rocq-lsp#960)
 - [petanque] new `get_state_at_pos` and `get_root_state` calls, that
   allow to retrieve a petanque proof state from position
   (@JulesViennotFranca, @ejgallego, rocq-community/rocq-lsp#962)
 - [doc] [petanque] Document petanque v1, improve readme (@ejgallego,
   rocq-community/rocq-lsp#963)
 - [plugin] [astdump] Make the JSON and SEXP output into a line per
   object by default (@blackbird1128, @ejgallego, rocq-community/rocq-lsp#874)
 - [doc] [emacs] [protocol] Improve documentation for `proof/goals`,
   add link to official emacs mode by Josselin Poiret (@ejgallego,
   rocq-community/rocq-lsp#969, thanks to @jpoiret, cc: rocq-community/rocq-lsp#941)
 - [goals] Include `range` in `proof/goals` answer. This is useful for
   clients willing to do highlighting (@ejgallego, @jpoiret, rocq-community/rocq-lsp#970)
dkalinichenko-js pushed a commit to dkalinichenko-js/opam-repository that referenced this pull request Jun 10, 2025
@ejgallego @d-kalinichenko
[new release] coq-lsp (0.2.3+8.18)
f3c3e00 
CHANGES:

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

 - [fleche] fix quick fixes for errors being lost due to incorrect
   handling of `send_diags_extra_data` (@ejgallego, rocq-community/rocq-lsp#850)
 - [vscode] Syntax highlighting for Coq 8.17-8.20 (@4ever2, rocq-community/rocq-lsp#872)
 - [build] Adapt to Coq -> Rocq renaming (@ejgallego, @proux, rocq-community/rocq-lsp#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, rocq-community/rocq-lsp#881)
 - [js worker] Update stubs (@ejgallego, @hhugo, rocq-community/rocq-lsp#881)
 - [js worker] Fix build for Coq -> Rocq renaming and stdlib split
   (@ejgallego, rocq-community/rocq-lsp#881)
 - [general] Adapt to Coq -> Rocq renaming (@ejgallego, @SkySkimmer,
   rocq-community/rocq-lsp#883)
 - [general] [js] Adapt to Rocq stdlib split (@ejgallego, rocq-community/rocq-lsp#890)
 - [ci] Bump setup-ocaml to v3 (@ejgallego, rocq-community/rocq-lsp#890)
 - [ci] [windows] Use Opam 2.2 to build on windows (@ejgallego, rocq-community/rocq-lsp#815,
   rocq-community/rocq-lsp#890)
 - [petanque] `petanque/start` now fails when the theorem was parsed
   but not successfully executed (@ejgallego, reported by @gbdrt,
   rocq-community/rocq-lsp#901, fixes rocq-community/rocq-lsp#886)
 - [ci] Test Ocaml 5.3 (@ejgallego, rocq-community/rocq-lsp#904)
 - [js worker] Add Shachar Itzhaky's trampoline patch; this greatly
   reduces the Stack Overflow in the proof engine (@ejgallego,
   @corwin-of-amber, rocq-community/rocq-lsp#905)
 - [js worker] [build] Include Coq WaterProof in the default Web
   Worker build (@ejgallego, waterproof team, rocq-community/rocq-lsp#905, closes rocq-community/rocq-lsp#888)
 - [vscode] [web] Fix web extension not exporting the coq-lsp
   extension API (@ejgallego, reported by @amblafont, rocq-community/rocq-lsp#911, fixes
   rocq-community/rocq-lsp#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, rocq-community/rocq-lsp#912, fixes
   rocq-community/rocq-lsp#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, rocq-community/rocq-lsp#916)
 - [lsp] [debug] Respect `$/setTrace` call , refactor logging system,
   and allow file logging of protocol traces again (@ejgallego, rocq-community/rocq-lsp#919,
   fixes rocq-community/rocq-lsp#868)
 - [coq] Support Coq relocatable mode (@SkySkimmer, rocq-community/rocq-lsp#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, rocq-community/rocq-lsp#951)
 - [hover] New option `show_state_hash_on_hover` that displays state
    hash on hover for debug (@ejgallego, rocq-community/rocq-lsp#954)
 - [doc] [faq] Updated FAQ to account for VSCoq 2 release in 2023,
   thanks to Patrick Nicodemus for pointing out the outdated
   documentation (@ejgallego, rocq-community/rocq-lsp#846, fixes rocq-community/rocq-lsp#817)
 - [vscode] [macos] Resolve keybinding conflict with Cmd+N and
   Cmd+Enter, we now use Alt+N and Alt+Shift+Enter, (Andrei
   Listochkin, rocq-community/rocq-lsp#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, rocq-community/rocq-lsp#957, fixes rocq-community/rocq-lsp#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, rocq-community/rocq-lsp#959, rocq-community/rocq-lsp#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, rocq-community/rocq-lsp#960)
 - [petanque] new `get_state_at_pos` and `get_root_state` calls, that
   allow to retrieve a petanque proof state from position
   (@JulesViennotFranca, @ejgallego, rocq-community/rocq-lsp#962)
 - [doc] [petanque] Document petanque v1, improve readme (@ejgallego,
   rocq-community/rocq-lsp#963)
 - [plugin] [astdump] Make the JSON and SEXP output into a line per
   object by default (@blackbird1128, @ejgallego, rocq-community/rocq-lsp#874)
 - [doc] [emacs] [protocol] Improve documentation for `proof/goals`,
   add link to official emacs mode by Josselin Poiret (@ejgallego,
   rocq-community/rocq-lsp#969, thanks to @jpoiret, cc: rocq-community/rocq-lsp#941)
 - [goals] Include `range` in `proof/goals` answer. This is useful for
   clients willing to do highlighting (@ejgallego, @jpoiret, rocq-community/rocq-lsp#970)
dkalinichenko-js pushed a commit to dkalinichenko-js/opam-repository that referenced this pull request Jun 10, 2025
@ejgallego @d-kalinichenko
[new release] coq-lsp (0.2.3+8.19)
3f7faad 
CHANGES:

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

 - [fleche] fix quick fixes for errors being lost due to incorrect
   handling of `send_diags_extra_data` (@ejgallego, rocq-community/rocq-lsp#850)
 - [vscode] Syntax highlighting for Coq 8.17-8.20 (@4ever2, rocq-community/rocq-lsp#872)
 - [build] Adapt to Coq -> Rocq renaming (@ejgallego, @proux, rocq-community/rocq-lsp#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, rocq-community/rocq-lsp#881)
 - [js worker] Update stubs (@ejgallego, @hhugo, rocq-community/rocq-lsp#881)
 - [js worker] Fix build for Coq -> Rocq renaming and stdlib split
   (@ejgallego, rocq-community/rocq-lsp#881)
 - [general] Adapt to Coq -> Rocq renaming (@ejgallego, @SkySkimmer,
   rocq-community/rocq-lsp#883)
 - [general] [js] Adapt to Rocq stdlib split (@ejgallego, rocq-community/rocq-lsp#890)
 - [ci] Bump setup-ocaml to v3 (@ejgallego, rocq-community/rocq-lsp#890)
 - [ci] [windows] Use Opam 2.2 to build on windows (@ejgallego, rocq-community/rocq-lsp#815,
   rocq-community/rocq-lsp#890)
 - [petanque] `petanque/start` now fails when the theorem was parsed
   but not successfully executed (@ejgallego, reported by @gbdrt,
   rocq-community/rocq-lsp#901, fixes rocq-community/rocq-lsp#886)
 - [ci] Test Ocaml 5.3 (@ejgallego, rocq-community/rocq-lsp#904)
 - [js worker] Add Shachar Itzhaky's trampoline patch; this greatly
   reduces the Stack Overflow in the proof engine (@ejgallego,
   @corwin-of-amber, rocq-community/rocq-lsp#905)
 - [js worker] [build] Include Coq WaterProof in the default Web
   Worker build (@ejgallego, waterproof team, rocq-community/rocq-lsp#905, closes rocq-community/rocq-lsp#888)
 - [vscode] [web] Fix web extension not exporting the coq-lsp
   extension API (@ejgallego, reported by @amblafont, rocq-community/rocq-lsp#911, fixes
   rocq-community/rocq-lsp#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, rocq-community/rocq-lsp#912, fixes
   rocq-community/rocq-lsp#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, rocq-community/rocq-lsp#916)
 - [lsp] [debug] Respect `$/setTrace` call , refactor logging system,
   and allow file logging of protocol traces again (@ejgallego, rocq-community/rocq-lsp#919,
   fixes rocq-community/rocq-lsp#868)
 - [coq] Support Coq relocatable mode (@SkySkimmer, rocq-community/rocq-lsp#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, rocq-community/rocq-lsp#951)
 - [hover] New option `show_state_hash_on_hover` that displays state
    hash on hover for debug (@ejgallego, rocq-community/rocq-lsp#954)
 - [doc] [faq] Updated FAQ to account for VSCoq 2 release in 2023,
   thanks to Patrick Nicodemus for pointing out the outdated
   documentation (@ejgallego, rocq-community/rocq-lsp#846, fixes rocq-community/rocq-lsp#817)
 - [vscode] [macos] Resolve keybinding conflict with Cmd+N and
   Cmd+Enter, we now use Alt+N and Alt+Shift+Enter, (Andrei
   Listochkin, rocq-community/rocq-lsp#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, rocq-community/rocq-lsp#957, fixes rocq-community/rocq-lsp#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, rocq-community/rocq-lsp#959, rocq-community/rocq-lsp#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, rocq-community/rocq-lsp#960)
 - [petanque] new `get_state_at_pos` and `get_root_state` calls, that
   allow to retrieve a petanque proof state from position
   (@JulesViennotFranca, @ejgallego, rocq-community/rocq-lsp#962)
 - [doc] [petanque] Document petanque v1, improve readme (@ejgallego,
   rocq-community/rocq-lsp#963)
 - [plugin] [astdump] Make the JSON and SEXP output into a line per
   object by default (@blackbird1128, @ejgallego, rocq-community/rocq-lsp#874)
 - [doc] [emacs] [protocol] Improve documentation for `proof/goals`,
   add link to official emacs mode by Josselin Poiret (@ejgallego,
   rocq-community/rocq-lsp#969, thanks to @jpoiret, cc: rocq-community/rocq-lsp#941)
 - [goals] Include `range` in `proof/goals` answer. This is useful for
   clients willing to do highlighting (@ejgallego, @jpoiret, rocq-community/rocq-lsp#970)
dkalinichenko-js pushed a commit to dkalinichenko-js/opam-repository that referenced this pull request Jun 10, 2025
@ejgallego @d-kalinichenko
[new release] coq-lsp (0.2.3+8.20)
dd10fc3 
CHANGES:

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

 - [fleche] fix quick fixes for errors being lost due to incorrect
   handling of `send_diags_extra_data` (@ejgallego, rocq-community/rocq-lsp#850)
 - [vscode] Syntax highlighting for Coq 8.17-8.20 (@4ever2, rocq-community/rocq-lsp#872)
 - [build] Adapt to Coq -> Rocq renaming (@ejgallego, @proux, rocq-community/rocq-lsp#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, rocq-community/rocq-lsp#881)
 - [js worker] Update stubs (@ejgallego, @hhugo, rocq-community/rocq-lsp#881)
 - [js worker] Fix build for Coq -> Rocq renaming and stdlib split
   (@ejgallego, rocq-community/rocq-lsp#881)
 - [general] Adapt to Coq -> Rocq renaming (@ejgallego, @SkySkimmer,
   rocq-community/rocq-lsp#883)
 - [general] [js] Adapt to Rocq stdlib split (@ejgallego, rocq-community/rocq-lsp#890)
 - [ci] Bump setup-ocaml to v3 (@ejgallego, rocq-community/rocq-lsp#890)
 - [ci] [windows] Use Opam 2.2 to build on windows (@ejgallego, rocq-community/rocq-lsp#815,
   rocq-community/rocq-lsp#890)
 - [petanque] `petanque/start` now fails when the theorem was parsed
   but not successfully executed (@ejgallego, reported by @gbdrt,
   rocq-community/rocq-lsp#901, fixes rocq-community/rocq-lsp#886)
 - [ci] Test Ocaml 5.3 (@ejgallego, rocq-community/rocq-lsp#904)
 - [js worker] Add Shachar Itzhaky's trampoline patch; this greatly
   reduces the Stack Overflow in the proof engine (@ejgallego,
   @corwin-of-amber, rocq-community/rocq-lsp#905)
 - [js worker] [build] Include Coq WaterProof in the default Web
   Worker build (@ejgallego, waterproof team, rocq-community/rocq-lsp#905, closes rocq-community/rocq-lsp#888)
 - [vscode] [web] Fix web extension not exporting the coq-lsp
   extension API (@ejgallego, reported by @amblafont, rocq-community/rocq-lsp#911, fixes
   rocq-community/rocq-lsp#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, rocq-community/rocq-lsp#912, fixes
   rocq-community/rocq-lsp#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, rocq-community/rocq-lsp#916)
 - [lsp] [debug] Respect `$/setTrace` call , refactor logging system,
   and allow file logging of protocol traces again (@ejgallego, rocq-community/rocq-lsp#919,
   fixes rocq-community/rocq-lsp#868)
 - [coq] Support Coq relocatable mode (@SkySkimmer, rocq-community/rocq-lsp#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, rocq-community/rocq-lsp#951)
 - [hover] New option `show_state_hash_on_hover` that displays state
    hash on hover for debug (@ejgallego, rocq-community/rocq-lsp#954)
 - [doc] [faq] Updated FAQ to account for VSCoq 2 release in 2023,
   thanks to Patrick Nicodemus for pointing out the outdated
   documentation (@ejgallego, rocq-community/rocq-lsp#846, fixes rocq-community/rocq-lsp#817)
 - [vscode] [macos] Resolve keybinding conflict with Cmd+N and
   Cmd+Enter, we now use Alt+N and Alt+Shift+Enter, (Andrei
   Listochkin, rocq-community/rocq-lsp#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, rocq-community/rocq-lsp#957, fixes rocq-community/rocq-lsp#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, rocq-community/rocq-lsp#959, rocq-community/rocq-lsp#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, rocq-community/rocq-lsp#960)
 - [petanque] new `get_state_at_pos` and `get_root_state` calls, that
   allow to retrieve a petanque proof state from position
   (@JulesViennotFranca, @ejgallego, rocq-community/rocq-lsp#962)
 - [doc] [petanque] Document petanque v1, improve readme (@ejgallego,
   rocq-community/rocq-lsp#963)
 - [plugin] [astdump] Make the JSON and SEXP output into a line per
   object by default (@blackbird1128, @ejgallego, rocq-community/rocq-lsp#874)
 - [doc] [emacs] [protocol] Improve documentation for `proof/goals`,
   add link to official emacs mode by Josselin Poiret (@ejgallego,
   rocq-community/rocq-lsp#969, thanks to @jpoiret, cc: rocq-community/rocq-lsp#941)
 - [goals] Include `range` in `proof/goals` answer. This is useful for
   clients willing to do highlighting (@ejgallego, @jpoiret, rocq-community/rocq-lsp#970)
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: bug Something isn't working kind: cleanup kind: fix kind: internal needs: test-case part: flèche part: protocol (LSP)

Projects

None yet

Milestone

0.2.3

Development

Successfully merging this pull request may close these issues.

1 participant

@ejgallego