Adapt to coq/coq#19901 (relocatable mode)#891
Merged
SkySkimmer merged 1 commit intorocq-community:mainfrom Mar 18, 2025
Merged
Conversation
ejgallego
reviewed
Jan 16, 2025
| let cmdline : Coq.Workspace.CmdLine.t = | ||
| { coqlib = Coq_config.coqlib | ||
| ; coqcorelib = Filename.concat Coq_config.coqlib "../rocq-runtime" | ||
| { coqlib = conf_coqlib |
Collaborator
There was a problem hiding this comment.
Seems to me like this should be the same time than the one in coq_config, but see my comment in the original PR.
Collaborator
Author
There was a problem hiding this comment.
Not seeing which comment you mean
Collaborator
There was a problem hiding this comment.
Sorry it wasn't sent yet went I wrote this. I'm happy consuming the new variant type, and following the spec at my side. I'm also happy for coq-lsp to error on relocatable so we don't block on coq-lsp implementing the spec, but we need a spec.
SkySkimmer
force-pushed
the
configure-clean
branch
from
be4f2fe to
5901697
Compare
gmalecha
pushed a commit
to bluerock-io/coq-lsp
that referenced
this pull request
Mar 7, 2025
Original commit: Adapt to rocq-prover/rocq#19901 (relocatable mode) This doesn't feel very satisfying but IDK what else to do.
Contributor
|
@SkySkimmer you need to sign the commits for this to be mergeable. |
SkySkimmer
force-pushed
the
configure-clean
branch
from
5901697 to
bedb83c
Compare
This doesn't feel very satisfying but IDK what else to do.
ejgallego
added a commit
that referenced
this pull request
Mar 18, 2025
We tweak the patch a little bit, and note the change in the changelog as it is user observable.
ejgallego
added a commit
that referenced
this pull request
Mar 18, 2025
[vendor] Bump Coq submodules after #891
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
3 participants
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 doesn't feel very satisfying but IDK what else to do.