Skip to content

[faq] Update FAQ for VsCoq 2 release.#846

Merged
ejgallego merged 1 commit intomainfrom
reamde_vscoq
May 18, 2025
Merged

[faq] Update FAQ for VsCoq 2 release.#846
ejgallego merged 1 commit intomainfrom
reamde_vscoq

Conversation

@ejgallego
Copy link
Collaborator

@ejgallego ejgallego commented Oct 4, 2024 •
edited
Loading

Fixes #817

Rendered

@ejgallego ejgallego added this to the 0.2.1 milestone Oct 4, 2024
@ejgallego ejgallego requested a review from Alizter October 4, 2024 08:29
@ejgallego
Copy link
Collaborator Author

ejgallego commented Oct 4, 2024 •
edited
Loading

cc: @patrick-nicodemus @corwin-of-amber

@patrick-nicodemus
Copy link
Contributor

patrick-nicodemus commented Oct 4, 2024

Thanks for this! I'll start looking into the documentation module and writing a LaTeX converter when I have some time.

@ejgallego
Copy link
Collaborator Author

ejgallego commented Oct 4, 2024

Thanks for this! I'll start looking into the documentation module and writing a LaTeX converter when I have some time.

I assume it looks good to you?

I did work a bit on the skeleton LaTeX converter we discussed actually, if you can wait a few more days I'll push a branch with a minimal working example. Sorry for the delay but got a lot of deadlines these last weeks.

@patrick-nicodemus
Copy link
Contributor

patrick-nicodemus commented Oct 4, 2024 via email

@ejgallego ejgallego modified the milestones: 0.2.1, 0.2.2 Oct 4, 2024
@ejgallego ejgallego force-pushed the reamde_vscoq branch 2 times, most recently from b0ac44d to c4373e4 Compare May 18, 2025 09:05
@ejgallego
Copy link
Collaborator Author

ejgallego commented May 18, 2025

Updated and merged, happy to further tweak, but I'd rather not delay this more.

@ejgallego ejgallego merged commit 471e289 into main May 18, 2025
13 checks passed
@ejgallego ejgallego deleted the reamde_vscoq branch May 18, 2025 09:06
@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

@Alizter Alizter Awaiting requested review from Alizter

Assignees

No one assigned

Labels

kind: enhancement New feature or request kind: fix part: documentation

Projects

None yet

Milestone

0.2.3

Development

Successfully merging this pull request may close these issues.

Clarify the difference between VsCoq 1 and VsCoq 2 here?

2 participants

@ejgallego @patrick-nicodemus