[goals] Include sentence range in proof/goals answer.#970
Merged
Conversation
ejgallego
added
kind: enhancement
ejgallego
changed the title
range in proof/goals answer.range in proof/goals answer.
This is useful for clients willing to do highlighting
ejgallego
force-pushed
the
reply_goal_range
branch
from
c723d8d to
ac1b56d
Compare
ejgallego
added a commit
to ejgallego/opam-repository
that referenced
this pull request
Jun 4, 2025
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
added a commit
to ejgallego/opam-repository
that referenced
this pull request
Jun 4, 2025
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
added a commit
to ejgallego/opam-repository
that referenced
this pull request
Jun 4, 2025
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
added a commit
to ejgallego/opam-repository
that referenced
this pull request
Jun 4, 2025
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
added a commit
to ejgallego/opam-repository
that referenced
this pull request
Jun 4, 2025
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
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
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
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
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
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)
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
This is useful for clients willing to do highlighting.