coq-lsp connection errors showing in non-Coq projects #750
Labels
Milestone
Comments
|
Hi @dariusf , I'm sorry to hear of this problem, it shouldn't happen! Do you mind sharing I was not able to reproduce this problem in my testing, but indeed I am sure there are cases we didn't anticipate. |
|
By the way, I agree this "red button" is annoying, in fact I have the same problem with We will likely remove this button and favor the new LanguageStatusItem API. |
|
No worries, and good to know! 😄 Here's my environment and the steps I took: VS Code versionCoq LSP VS Code extension: v0.1.10
Coq LSP Server Events after |
|
I see thanks, indeed I can reproduce. Will work on a fix ASAP. For now you can workaround this by right clicking on the toolbar, and selecting hide. Use instead the new indicator in the language section (bottom-right corner |
|
Great, thank you! |
ejgallego
added a commit
that referenced
this issue
Jun 5, 2024
…or for us This seems like the right setup, making the server start lazy. Still it would be better that VSCode API allowed us to activate our extension in a more fine-grained fashion. Fixes #750
ejgallego
added a commit
that referenced
this issue
Jun 5, 2024
…or for us This seems like the right setup, making the server start lazy. Still it would be better that VSCode API allowed us to activate our extension in a more fine-grained fashion. Fixes #750
ejgallego
added a commit
that referenced
this issue
Jun 5, 2024
…or for us This seems like the right setup, making the server start lazy. Still it would be better that VSCode API allowed us to activate our extension in a more fine-grained fashion. Fixes #750
ejgallego
added a commit
that referenced
this issue
Jun 6, 2024
…or for us This seems like the right setup, making the server start lazy. Still it would be better that VSCode API allowed us to activate our extension in a more fine-grained fashion. Fixes #750
ejgallego
added a commit
that referenced
this issue
Jun 6, 2024
…or for us This seems like the right setup, making the server start lazy. Still it would be better that VSCode API allowed us to activate our extension in a more fine-grained fashion. Fixes #750
ejgallego
added a commit
that referenced
this issue
Jun 7, 2024
…or for us This seems like the right setup, making the server start lazy. Still it would be better that VSCode API allowed us to activate our extension in a more fine-grained fashion. Fixes #750
ejgallego
added a commit
to ejgallego/opam-repository
that referenced
this issue
Aug 29, 2024
CHANGES: ----------------------------------- - [deps] merge serlib into coq-lsp. This allow us to drop the SerAPI dependency, and will greatly easy the development of tools that require AST manipulation (@ejgallego, ejgallego/coq-lsp#698) - [fleche] Remove 8.16 compatibility layer (@ejgallego, ejgallego/coq-lsp#747) - [fleche] Preserve view hint across document changes. With this change, we get local continuous checking mode when the view-port heuristic is enabled (@ejgallego, ejgallego/coq-lsp#748) - [memo] More precise hashing for Coq states, this improves cache performance quite a bit (@ejgallego, ejgallego/coq-lsp#751) - [fleche] Enable sharing of `.vo` file parsing. This enables better sharing, achieving an almost 50% memory reduction for example when opening all of HoTT .v files (@ejgallego, @SkySkimmer, @bhaktishh, ejgallego/coq-lsp#744) - [memo] Provide API to query Hashtbl stats (@ejgallego, ejgallego/coq-lsp#753) - [nix] Add `pet-server` deps to flake.nix (Léo Stefanesco, ejgallego/coq-lsp#754) - [coq-lsp] Fix crash on `--help` option (Léo Stefanesco, @ejgallego, ejgallego/coq-lsp#754) - [vscode] Fix focus race when a Coq file is in column 2 (@ejgallego, ejgallego/coq-lsp#755, cc: ejgallego/coq-lsp#722, ejgallego/coq-lsp#725) - [hover] Show input howto for unicode characters on hover (@ejgallego, Léo Stefanesco, ejgallego/coq-lsp#756) - [lsp] [definition] Support for jump to definition across workspace files. The location information is obtained from `.glob` files, so it is often not perfect. (@ejgallego, ejgallego/coq-lsp#762, fixes ejgallego/coq-lsp#317) - [lsp] [hover] Show full name and provenance of identifiers (@ejgallego, ejgallego/coq-lsp#762) - [lsp] [definition] Try also to resolve and locate module imports (@ejgallego, ejgallego/coq-lsp#764) - [code] Don't start server on extension activation, unless an editor we own is active. We also auto-start the server if a document that we own is opened later (@ejgallego, ejgallego/coq-lsp#758, fixes ejgallego/coq-lsp#750) - [petanque] Allow `init` to be called multiple times (@ejgallego, @gbdrt, ejgallego/coq-lsp#766) - [petanque] Faster query for goals status after `run_tac` (@ejgallego, ejgallego/coq-lsp#768) - [petanque] New parameter `pre_commands` to `start` which allows instrumenting the goal before starting the proof (@ejgallego, Alex Sanchez-Stern ejgallego/coq-lsp#769) - [petanque] New `http_headers={yes,no}` parameter for `pet` json shell, plus some improvements on protocol handling (@ejgallego, ejgallego/coq-lsp#770) - [petanque] Make agent agnostic of environment, allowing embedding inside LSP (@ejgallego, ejgallego/coq-lsp#771) - [diagnostics] Ensure extra diagnostics info is present in all errors, not only on those sentences that did parse successfully (@ejgallego, Diego Rivera, ejgallego/coq-lsp#772) - [hover] New option `show_universes_on_hover` that will display universe data on hover (@ejgallego, @SkySkimmer, ejgallego/coq-lsp#666) - [hover] New plugin `unidiff` that will elaborate a summary of universe data a file, in particular regarding universes added at `Qed` time (@ejgallego, ejgallego/coq-lsp#773) - [fleche] Support meta-command `Abort All` (@ejgallego, ejgallego/coq-lsp#774, fixes ejgallego/coq-lsp#550) - [petanque] Allow memoization control on `petanque/run` via a new parameter `memo` (@ejgallego, ejgallego/coq-lsp#780) - [lsp] [petanque] Allow acces to `petanque` protocol from the lsp server (@ejgallego, ejgallego/coq-lsp#778) - [petanque] Always initialize a workspace. This made `pet` crash if `--root` was not used and client didn't issue the optimal `setWorkspace` call (ejgallego/coq-lsp#782, @ejgallego, @gbdrt) - [lsp] [petanque] New methods `state/eq` and `state/hash`; this allows clients to implement a client-side hash; equality is configurable with different methods; moreover, `petanque/run` can compute some extra data like state hashing without a round-trip (@ejgallego @gbdrt, ejgallego/coq-lsp#779) - [petanque] New methods to hash proof states; use proof state hash by default in petanque agent (@ejgallego, @gbdrt, ejgallego/coq-lsp#808) - [petanque] New shell method `petanque/toc` that returns a document outline in LSP-style (@ejgallego, ejgallego/coq-lsp#794)
ejgallego
added a commit
to ejgallego/opam-repository
that referenced
this issue
Aug 29, 2024
CHANGES: ----------------------------------- - [deps] merge serlib into coq-lsp. This allow us to drop the SerAPI dependency, and will greatly easy the development of tools that require AST manipulation (@ejgallego, ejgallego/coq-lsp#698) - [fleche] Remove 8.16 compatibility layer (@ejgallego, ejgallego/coq-lsp#747) - [fleche] Preserve view hint across document changes. With this change, we get local continuous checking mode when the view-port heuristic is enabled (@ejgallego, ejgallego/coq-lsp#748) - [memo] More precise hashing for Coq states, this improves cache performance quite a bit (@ejgallego, ejgallego/coq-lsp#751) - [fleche] Enable sharing of `.vo` file parsing. This enables better sharing, achieving an almost 50% memory reduction for example when opening all of HoTT .v files (@ejgallego, @SkySkimmer, @bhaktishh, ejgallego/coq-lsp#744) - [memo] Provide API to query Hashtbl stats (@ejgallego, ejgallego/coq-lsp#753) - [nix] Add `pet-server` deps to flake.nix (Léo Stefanesco, ejgallego/coq-lsp#754) - [coq-lsp] Fix crash on `--help` option (Léo Stefanesco, @ejgallego, ejgallego/coq-lsp#754) - [vscode] Fix focus race when a Coq file is in column 2 (@ejgallego, ejgallego/coq-lsp#755, cc: ejgallego/coq-lsp#722, ejgallego/coq-lsp#725) - [hover] Show input howto for unicode characters on hover (@ejgallego, Léo Stefanesco, ejgallego/coq-lsp#756) - [lsp] [definition] Support for jump to definition across workspace files. The location information is obtained from `.glob` files, so it is often not perfect. (@ejgallego, ejgallego/coq-lsp#762, fixes ejgallego/coq-lsp#317) - [lsp] [hover] Show full name and provenance of identifiers (@ejgallego, ejgallego/coq-lsp#762) - [lsp] [definition] Try also to resolve and locate module imports (@ejgallego, ejgallego/coq-lsp#764) - [code] Don't start server on extension activation, unless an editor we own is active. We also auto-start the server if a document that we own is opened later (@ejgallego, ejgallego/coq-lsp#758, fixes ejgallego/coq-lsp#750) - [petanque] Allow `init` to be called multiple times (@ejgallego, @gbdrt, ejgallego/coq-lsp#766) - [petanque] Faster query for goals status after `run_tac` (@ejgallego, ejgallego/coq-lsp#768) - [petanque] New parameter `pre_commands` to `start` which allows instrumenting the goal before starting the proof (@ejgallego, Alex Sanchez-Stern ejgallego/coq-lsp#769) - [petanque] New `http_headers={yes,no}` parameter for `pet` json shell, plus some improvements on protocol handling (@ejgallego, ejgallego/coq-lsp#770) - [petanque] Make agent agnostic of environment, allowing embedding inside LSP (@ejgallego, ejgallego/coq-lsp#771) - [diagnostics] Ensure extra diagnostics info is present in all errors, not only on those sentences that did parse successfully (@ejgallego, Diego Rivera, ejgallego/coq-lsp#772) - [hover] New option `show_universes_on_hover` that will display universe data on hover (@ejgallego, @SkySkimmer, ejgallego/coq-lsp#666) - [hover] New plugin `unidiff` that will elaborate a summary of universe data a file, in particular regarding universes added at `Qed` time (@ejgallego, ejgallego/coq-lsp#773) - [fleche] Support meta-command `Abort All` (@ejgallego, ejgallego/coq-lsp#774, fixes ejgallego/coq-lsp#550) - [petanque] Allow memoization control on `petanque/run` via a new parameter `memo` (@ejgallego, ejgallego/coq-lsp#780) - [lsp] [petanque] Allow acces to `petanque` protocol from the lsp server (@ejgallego, ejgallego/coq-lsp#778) - [petanque] Always initialize a workspace. This made `pet` crash if `--root` was not used and client didn't issue the optimal `setWorkspace` call (ejgallego/coq-lsp#782, @ejgallego, @gbdrt) - [lsp] [petanque] New methods `state/eq` and `state/hash`; this allows clients to implement a client-side hash; equality is configurable with different methods; moreover, `petanque/run` can compute some extra data like state hashing without a round-trip (@ejgallego @gbdrt, ejgallego/coq-lsp#779) - [petanque] New methods to hash proof states; use proof state hash by default in petanque agent (@ejgallego, @gbdrt, ejgallego/coq-lsp#808) - [petanque] New shell method `petanque/toc` that returns a document outline in LSP-style (@ejgallego, ejgallego/coq-lsp#794)
ejgallego
added a commit
to ejgallego/opam-repository
that referenced
this issue
Aug 29, 2024
CHANGES: ----------------------------------- - [deps] merge serlib into coq-lsp. This allow us to drop the SerAPI dependency, and will greatly easy the development of tools that require AST manipulation (@ejgallego, ejgallego/coq-lsp#698) - [fleche] Remove 8.16 compatibility layer (@ejgallego, ejgallego/coq-lsp#747) - [fleche] Preserve view hint across document changes. With this change, we get local continuous checking mode when the view-port heuristic is enabled (@ejgallego, ejgallego/coq-lsp#748) - [memo] More precise hashing for Coq states, this improves cache performance quite a bit (@ejgallego, ejgallego/coq-lsp#751) - [fleche] Enable sharing of `.vo` file parsing. This enables better sharing, achieving an almost 50% memory reduction for example when opening all of HoTT .v files (@ejgallego, @SkySkimmer, @bhaktishh, ejgallego/coq-lsp#744) - [memo] Provide API to query Hashtbl stats (@ejgallego, ejgallego/coq-lsp#753) - [nix] Add `pet-server` deps to flake.nix (Léo Stefanesco, ejgallego/coq-lsp#754) - [coq-lsp] Fix crash on `--help` option (Léo Stefanesco, @ejgallego, ejgallego/coq-lsp#754) - [vscode] Fix focus race when a Coq file is in column 2 (@ejgallego, ejgallego/coq-lsp#755, cc: ejgallego/coq-lsp#722, ejgallego/coq-lsp#725) - [hover] Show input howto for unicode characters on hover (@ejgallego, Léo Stefanesco, ejgallego/coq-lsp#756) - [lsp] [definition] Support for jump to definition across workspace files. The location information is obtained from `.glob` files, so it is often not perfect. (@ejgallego, ejgallego/coq-lsp#762, fixes ejgallego/coq-lsp#317) - [lsp] [hover] Show full name and provenance of identifiers (@ejgallego, ejgallego/coq-lsp#762) - [lsp] [definition] Try also to resolve and locate module imports (@ejgallego, ejgallego/coq-lsp#764) - [code] Don't start server on extension activation, unless an editor we own is active. We also auto-start the server if a document that we own is opened later (@ejgallego, ejgallego/coq-lsp#758, fixes ejgallego/coq-lsp#750) - [petanque] Allow `init` to be called multiple times (@ejgallego, @gbdrt, ejgallego/coq-lsp#766) - [petanque] Faster query for goals status after `run_tac` (@ejgallego, ejgallego/coq-lsp#768) - [petanque] New parameter `pre_commands` to `start` which allows instrumenting the goal before starting the proof (@ejgallego, Alex Sanchez-Stern ejgallego/coq-lsp#769) - [petanque] New `http_headers={yes,no}` parameter for `pet` json shell, plus some improvements on protocol handling (@ejgallego, ejgallego/coq-lsp#770) - [petanque] Make agent agnostic of environment, allowing embedding inside LSP (@ejgallego, ejgallego/coq-lsp#771) - [diagnostics] Ensure extra diagnostics info is present in all errors, not only on those sentences that did parse successfully (@ejgallego, Diego Rivera, ejgallego/coq-lsp#772) - [hover] New option `show_universes_on_hover` that will display universe data on hover (@ejgallego, @SkySkimmer, ejgallego/coq-lsp#666) - [hover] New plugin `unidiff` that will elaborate a summary of universe data a file, in particular regarding universes added at `Qed` time (@ejgallego, ejgallego/coq-lsp#773) - [fleche] Support meta-command `Abort All` (@ejgallego, ejgallego/coq-lsp#774, fixes ejgallego/coq-lsp#550) - [petanque] Allow memoization control on `petanque/run` via a new parameter `memo` (@ejgallego, ejgallego/coq-lsp#780) - [lsp] [petanque] Allow acces to `petanque` protocol from the lsp server (@ejgallego, ejgallego/coq-lsp#778) - [petanque] Always initialize a workspace. This made `pet` crash if `--root` was not used and client didn't issue the optimal `setWorkspace` call (ejgallego/coq-lsp#782, @ejgallego, @gbdrt) - [lsp] [petanque] New methods `state/eq` and `state/hash`; this allows clients to implement a client-side hash; equality is configurable with different methods; moreover, `petanque/run` can compute some extra data like state hashing without a round-trip (@ejgallego @gbdrt, ejgallego/coq-lsp#779) - [petanque] New methods to hash proof states; use proof state hash by default in petanque agent (@ejgallego, @gbdrt, ejgallego/coq-lsp#808) - [petanque] New shell method `petanque/toc` that returns a document outline in LSP-style (@ejgallego, ejgallego/coq-lsp#794)
ejgallego
added a commit
to ejgallego/opam-repository
that referenced
this issue
Aug 29, 2024
CHANGES: ----------------------------------- - [deps] merge serlib into coq-lsp. This allow us to drop the SerAPI dependency, and will greatly easy the development of tools that require AST manipulation (@ejgallego, ejgallego/coq-lsp#698) - [fleche] Remove 8.16 compatibility layer (@ejgallego, ejgallego/coq-lsp#747) - [fleche] Preserve view hint across document changes. With this change, we get local continuous checking mode when the view-port heuristic is enabled (@ejgallego, ejgallego/coq-lsp#748) - [memo] More precise hashing for Coq states, this improves cache performance quite a bit (@ejgallego, ejgallego/coq-lsp#751) - [fleche] Enable sharing of `.vo` file parsing. This enables better sharing, achieving an almost 50% memory reduction for example when opening all of HoTT .v files (@ejgallego, @SkySkimmer, @bhaktishh, ejgallego/coq-lsp#744) - [memo] Provide API to query Hashtbl stats (@ejgallego, ejgallego/coq-lsp#753) - [nix] Add `pet-server` deps to flake.nix (Léo Stefanesco, ejgallego/coq-lsp#754) - [coq-lsp] Fix crash on `--help` option (Léo Stefanesco, @ejgallego, ejgallego/coq-lsp#754) - [vscode] Fix focus race when a Coq file is in column 2 (@ejgallego, ejgallego/coq-lsp#755, cc: ejgallego/coq-lsp#722, ejgallego/coq-lsp#725) - [hover] Show input howto for unicode characters on hover (@ejgallego, Léo Stefanesco, ejgallego/coq-lsp#756) - [lsp] [definition] Support for jump to definition across workspace files. The location information is obtained from `.glob` files, so it is often not perfect. (@ejgallego, ejgallego/coq-lsp#762, fixes ejgallego/coq-lsp#317) - [lsp] [hover] Show full name and provenance of identifiers (@ejgallego, ejgallego/coq-lsp#762) - [lsp] [definition] Try also to resolve and locate module imports (@ejgallego, ejgallego/coq-lsp#764) - [code] Don't start server on extension activation, unless an editor we own is active. We also auto-start the server if a document that we own is opened later (@ejgallego, ejgallego/coq-lsp#758, fixes ejgallego/coq-lsp#750) - [petanque] Allow `init` to be called multiple times (@ejgallego, @gbdrt, ejgallego/coq-lsp#766) - [petanque] Faster query for goals status after `run_tac` (@ejgallego, ejgallego/coq-lsp#768) - [petanque] New parameter `pre_commands` to `start` which allows instrumenting the goal before starting the proof (@ejgallego, Alex Sanchez-Stern ejgallego/coq-lsp#769) - [petanque] New `http_headers={yes,no}` parameter for `pet` json shell, plus some improvements on protocol handling (@ejgallego, ejgallego/coq-lsp#770) - [petanque] Make agent agnostic of environment, allowing embedding inside LSP (@ejgallego, ejgallego/coq-lsp#771) - [diagnostics] Ensure extra diagnostics info is present in all errors, not only on those sentences that did parse successfully (@ejgallego, Diego Rivera, ejgallego/coq-lsp#772) - [hover] New option `show_universes_on_hover` that will display universe data on hover (@ejgallego, @SkySkimmer, ejgallego/coq-lsp#666) - [hover] New plugin `unidiff` that will elaborate a summary of universe data a file, in particular regarding universes added at `Qed` time (@ejgallego, ejgallego/coq-lsp#773) - [fleche] Support meta-command `Abort All` (@ejgallego, ejgallego/coq-lsp#774, fixes ejgallego/coq-lsp#550) - [petanque] Allow memoization control on `petanque/run` via a new parameter `memo` (@ejgallego, ejgallego/coq-lsp#780) - [lsp] [petanque] Allow acces to `petanque` protocol from the lsp server (@ejgallego, ejgallego/coq-lsp#778) - [petanque] Always initialize a workspace. This made `pet` crash if `--root` was not used and client didn't issue the optimal `setWorkspace` call (ejgallego/coq-lsp#782, @ejgallego, @gbdrt) - [lsp] [petanque] New methods `state/eq` and `state/hash`; this allows clients to implement a client-side hash; equality is configurable with different methods; moreover, `petanque/run` can compute some extra data like state hashing without a round-trip (@ejgallego @gbdrt, ejgallego/coq-lsp#779) - [petanque] New methods to hash proof states; use proof state hash by default in petanque agent (@ejgallego, @gbdrt, ejgallego/coq-lsp#808) - [petanque] New shell method `petanque/toc` that returns a document outline in LSP-style (@ejgallego, ejgallego/coq-lsp#794)
ejgallego
added a commit
to ejgallego/opam-repository
that referenced
this issue
Aug 29, 2024
CHANGES: ----------------------------------- - [deps] merge serlib into coq-lsp. This allow us to drop the SerAPI dependency, and will greatly easy the development of tools that require AST manipulation (@ejgallego, ejgallego/coq-lsp#698) - [fleche] Remove 8.16 compatibility layer (@ejgallego, ejgallego/coq-lsp#747) - [fleche] Preserve view hint across document changes. With this change, we get local continuous checking mode when the view-port heuristic is enabled (@ejgallego, ejgallego/coq-lsp#748) - [memo] More precise hashing for Coq states, this improves cache performance quite a bit (@ejgallego, ejgallego/coq-lsp#751) - [fleche] Enable sharing of `.vo` file parsing. This enables better sharing, achieving an almost 50% memory reduction for example when opening all of HoTT .v files (@ejgallego, @SkySkimmer, @bhaktishh, ejgallego/coq-lsp#744) - [memo] Provide API to query Hashtbl stats (@ejgallego, ejgallego/coq-lsp#753) - [nix] Add `pet-server` deps to flake.nix (Léo Stefanesco, ejgallego/coq-lsp#754) - [coq-lsp] Fix crash on `--help` option (Léo Stefanesco, @ejgallego, ejgallego/coq-lsp#754) - [vscode] Fix focus race when a Coq file is in column 2 (@ejgallego, ejgallego/coq-lsp#755, cc: ejgallego/coq-lsp#722, ejgallego/coq-lsp#725) - [hover] Show input howto for unicode characters on hover (@ejgallego, Léo Stefanesco, ejgallego/coq-lsp#756) - [lsp] [definition] Support for jump to definition across workspace files. The location information is obtained from `.glob` files, so it is often not perfect. (@ejgallego, ejgallego/coq-lsp#762, fixes ejgallego/coq-lsp#317) - [lsp] [hover] Show full name and provenance of identifiers (@ejgallego, ejgallego/coq-lsp#762) - [lsp] [definition] Try also to resolve and locate module imports (@ejgallego, ejgallego/coq-lsp#764) - [code] Don't start server on extension activation, unless an editor we own is active. We also auto-start the server if a document that we own is opened later (@ejgallego, ejgallego/coq-lsp#758, fixes ejgallego/coq-lsp#750) - [petanque] Allow `init` to be called multiple times (@ejgallego, @gbdrt, ejgallego/coq-lsp#766) - [petanque] Faster query for goals status after `run_tac` (@ejgallego, ejgallego/coq-lsp#768) - [petanque] New parameter `pre_commands` to `start` which allows instrumenting the goal before starting the proof (@ejgallego, Alex Sanchez-Stern ejgallego/coq-lsp#769) - [petanque] New `http_headers={yes,no}` parameter for `pet` json shell, plus some improvements on protocol handling (@ejgallego, ejgallego/coq-lsp#770) - [petanque] Make agent agnostic of environment, allowing embedding inside LSP (@ejgallego, ejgallego/coq-lsp#771) - [diagnostics] Ensure extra diagnostics info is present in all errors, not only on those sentences that did parse successfully (@ejgallego, Diego Rivera, ejgallego/coq-lsp#772) - [hover] New option `show_universes_on_hover` that will display universe data on hover (@ejgallego, @SkySkimmer, ejgallego/coq-lsp#666) - [hover] New plugin `unidiff` that will elaborate a summary of universe data a file, in particular regarding universes added at `Qed` time (@ejgallego, ejgallego/coq-lsp#773) - [fleche] Support meta-command `Abort All` (@ejgallego, ejgallego/coq-lsp#774, fixes ejgallego/coq-lsp#550) - [petanque] Allow memoization control on `petanque/run` via a new parameter `memo` (@ejgallego, ejgallego/coq-lsp#780) - [lsp] [petanque] Allow acces to `petanque` protocol from the lsp server (@ejgallego, ejgallego/coq-lsp#778) - [petanque] Always initialize a workspace. This made `pet` crash if `--root` was not used and client didn't issue the optimal `setWorkspace` call (ejgallego/coq-lsp#782, @ejgallego, @gbdrt) - [lsp] [petanque] New methods `state/eq` and `state/hash`; this allows clients to implement a client-side hash; equality is configurable with different methods; moreover, `petanque/run` can compute some extra data like state hashing without a round-trip (@ejgallego @gbdrt, ejgallego/coq-lsp#779) - [petanque] New methods to hash proof states; use proof state hash by default in petanque agent (@ejgallego, @gbdrt, ejgallego/coq-lsp#808) - [petanque] New shell method `petanque/toc` that returns a document outline in LSP-style (@ejgallego, ejgallego/coq-lsp#794)
ejgallego
added a commit
to ejgallego/opam-repository
that referenced
this issue
Aug 29, 2024
CHANGES: ----------------------------------- - [deps] merge serlib into coq-lsp. This allow us to drop the SerAPI dependency, and will greatly easy the development of tools that require AST manipulation (@ejgallego, ejgallego/coq-lsp#698) - [fleche] Remove 8.16 compatibility layer (@ejgallego, ejgallego/coq-lsp#747) - [fleche] Preserve view hint across document changes. With this change, we get local continuous checking mode when the view-port heuristic is enabled (@ejgallego, ejgallego/coq-lsp#748) - [memo] More precise hashing for Coq states, this improves cache performance quite a bit (@ejgallego, ejgallego/coq-lsp#751) - [fleche] Enable sharing of `.vo` file parsing. This enables better sharing, achieving an almost 50% memory reduction for example when opening all of HoTT .v files (@ejgallego, @SkySkimmer, @bhaktishh, ejgallego/coq-lsp#744) - [memo] Provide API to query Hashtbl stats (@ejgallego, ejgallego/coq-lsp#753) - [nix] Add `pet-server` deps to flake.nix (Léo Stefanesco, ejgallego/coq-lsp#754) - [coq-lsp] Fix crash on `--help` option (Léo Stefanesco, @ejgallego, ejgallego/coq-lsp#754) - [vscode] Fix focus race when a Coq file is in column 2 (@ejgallego, ejgallego/coq-lsp#755, cc: ejgallego/coq-lsp#722, ejgallego/coq-lsp#725) - [hover] Show input howto for unicode characters on hover (@ejgallego, Léo Stefanesco, ejgallego/coq-lsp#756) - [lsp] [definition] Support for jump to definition across workspace files. The location information is obtained from `.glob` files, so it is often not perfect. (@ejgallego, ejgallego/coq-lsp#762, fixes ejgallego/coq-lsp#317) - [lsp] [hover] Show full name and provenance of identifiers (@ejgallego, ejgallego/coq-lsp#762) - [lsp] [definition] Try also to resolve and locate module imports (@ejgallego, ejgallego/coq-lsp#764) - [code] Don't start server on extension activation, unless an editor we own is active. We also auto-start the server if a document that we own is opened later (@ejgallego, ejgallego/coq-lsp#758, fixes ejgallego/coq-lsp#750) - [petanque] Allow `init` to be called multiple times (@ejgallego, @gbdrt, ejgallego/coq-lsp#766) - [petanque] Faster query for goals status after `run_tac` (@ejgallego, ejgallego/coq-lsp#768) - [petanque] New parameter `pre_commands` to `start` which allows instrumenting the goal before starting the proof (@ejgallego, Alex Sanchez-Stern ejgallego/coq-lsp#769) - [petanque] New `http_headers={yes,no}` parameter for `pet` json shell, plus some improvements on protocol handling (@ejgallego, ejgallego/coq-lsp#770) - [petanque] Make agent agnostic of environment, allowing embedding inside LSP (@ejgallego, ejgallego/coq-lsp#771) - [diagnostics] Ensure extra diagnostics info is present in all errors, not only on those sentences that did parse successfully (@ejgallego, Diego Rivera, ejgallego/coq-lsp#772) - [hover] New option `show_universes_on_hover` that will display universe data on hover (@ejgallego, @SkySkimmer, ejgallego/coq-lsp#666) - [hover] New plugin `unidiff` that will elaborate a summary of universe data a file, in particular regarding universes added at `Qed` time (@ejgallego, ejgallego/coq-lsp#773) - [fleche] Support meta-command `Abort All` (@ejgallego, ejgallego/coq-lsp#774, fixes ejgallego/coq-lsp#550) - [petanque] Allow memoization control on `petanque/run` via a new parameter `memo` (@ejgallego, ejgallego/coq-lsp#780) - [lsp] [petanque] Allow acces to `petanque` protocol from the lsp server (@ejgallego, ejgallego/coq-lsp#778) - [petanque] Always initialize a workspace. This made `pet` crash if `--root` was not used and client didn't issue the optimal `setWorkspace` call (ejgallego/coq-lsp#782, @ejgallego, @gbdrt) - [lsp] [petanque] New methods `state/eq` and `state/hash`; this allows clients to implement a client-side hash; equality is configurable with different methods; moreover, `petanque/run` can compute some extra data like state hashing without a round-trip (@ejgallego @gbdrt, ejgallego/coq-lsp#779) - [petanque] New methods to hash proof states; use proof state hash by default in petanque agent (@ejgallego, @gbdrt, ejgallego/coq-lsp#808) - [petanque] New shell method `petanque/toc` that returns a document outline in LSP-style (@ejgallego, ejgallego/coq-lsp#794)
ejgallego
added a commit
to ejgallego/opam-repository
that referenced
this issue
Aug 29, 2024
CHANGES: ----------------------------------- - [deps] merge serlib into coq-lsp. This allow us to drop the SerAPI dependency, and will greatly easy the development of tools that require AST manipulation (@ejgallego, ejgallego/coq-lsp#698) - [fleche] Remove 8.16 compatibility layer (@ejgallego, ejgallego/coq-lsp#747) - [fleche] Preserve view hint across document changes. With this change, we get local continuous checking mode when the view-port heuristic is enabled (@ejgallego, ejgallego/coq-lsp#748) - [memo] More precise hashing for Coq states, this improves cache performance quite a bit (@ejgallego, ejgallego/coq-lsp#751) - [fleche] Enable sharing of `.vo` file parsing. This enables better sharing, achieving an almost 50% memory reduction for example when opening all of HoTT .v files (@ejgallego, @SkySkimmer, @bhaktishh, ejgallego/coq-lsp#744) - [memo] Provide API to query Hashtbl stats (@ejgallego, ejgallego/coq-lsp#753) - [nix] Add `pet-server` deps to flake.nix (Léo Stefanesco, ejgallego/coq-lsp#754) - [coq-lsp] Fix crash on `--help` option (Léo Stefanesco, @ejgallego, ejgallego/coq-lsp#754) - [vscode] Fix focus race when a Coq file is in column 2 (@ejgallego, ejgallego/coq-lsp#755, cc: ejgallego/coq-lsp#722, ejgallego/coq-lsp#725) - [hover] Show input howto for unicode characters on hover (@ejgallego, Léo Stefanesco, ejgallego/coq-lsp#756) - [lsp] [definition] Support for jump to definition across workspace files. The location information is obtained from `.glob` files, so it is often not perfect. (@ejgallego, ejgallego/coq-lsp#762, fixes ejgallego/coq-lsp#317) - [lsp] [hover] Show full name and provenance of identifiers (@ejgallego, ejgallego/coq-lsp#762) - [lsp] [definition] Try also to resolve and locate module imports (@ejgallego, ejgallego/coq-lsp#764) - [code] Don't start server on extension activation, unless an editor we own is active. We also auto-start the server if a document that we own is opened later (@ejgallego, ejgallego/coq-lsp#758, fixes ejgallego/coq-lsp#750) - [petanque] Allow `init` to be called multiple times (@ejgallego, @gbdrt, ejgallego/coq-lsp#766) - [petanque] Faster query for goals status after `run_tac` (@ejgallego, ejgallego/coq-lsp#768) - [petanque] New parameter `pre_commands` to `start` which allows instrumenting the goal before starting the proof (@ejgallego, Alex Sanchez-Stern ejgallego/coq-lsp#769) - [petanque] New `http_headers={yes,no}` parameter for `pet` json shell, plus some improvements on protocol handling (@ejgallego, ejgallego/coq-lsp#770) - [petanque] Make agent agnostic of environment, allowing embedding inside LSP (@ejgallego, ejgallego/coq-lsp#771) - [diagnostics] Ensure extra diagnostics info is present in all errors, not only on those sentences that did parse successfully (@ejgallego, Diego Rivera, ejgallego/coq-lsp#772) - [hover] New option `show_universes_on_hover` that will display universe data on hover (@ejgallego, @SkySkimmer, ejgallego/coq-lsp#666) - [hover] New plugin `unidiff` that will elaborate a summary of universe data a file, in particular regarding universes added at `Qed` time (@ejgallego, ejgallego/coq-lsp#773) - [fleche] Support meta-command `Abort All` (@ejgallego, ejgallego/coq-lsp#774, fixes ejgallego/coq-lsp#550) - [petanque] Allow memoization control on `petanque/run` via a new parameter `memo` (@ejgallego, ejgallego/coq-lsp#780) - [lsp] [petanque] Allow acces to `petanque` protocol from the lsp server (@ejgallego, ejgallego/coq-lsp#778) - [petanque] Always initialize a workspace. This made `pet` crash if `--root` was not used and client didn't issue the optimal `setWorkspace` call (ejgallego/coq-lsp#782, @ejgallego, @gbdrt) - [lsp] [petanque] New methods `state/eq` and `state/hash`; this allows clients to implement a client-side hash; equality is configurable with different methods; moreover, `petanque/run` can compute some extra data like state hashing without a round-trip (@ejgallego @gbdrt, ejgallego/coq-lsp#779) - [petanque] New methods to hash proof states; use proof state hash by default in petanque agent (@ejgallego, @gbdrt, ejgallego/coq-lsp#808) - [petanque] New shell method `petanque/toc` that returns a document outline in LSP-style (@ejgallego, ejgallego/coq-lsp#794)
ejgallego
added a commit
to ejgallego/opam-repository
that referenced
this issue
Aug 29, 2024
CHANGES: ----------------------------------- - [deps] merge serlib into coq-lsp. This allow us to drop the SerAPI dependency, and will greatly easy the development of tools that require AST manipulation (@ejgallego, ejgallego/coq-lsp#698) - [fleche] Remove 8.16 compatibility layer (@ejgallego, ejgallego/coq-lsp#747) - [fleche] Preserve view hint across document changes. With this change, we get local continuous checking mode when the view-port heuristic is enabled (@ejgallego, ejgallego/coq-lsp#748) - [memo] More precise hashing for Coq states, this improves cache performance quite a bit (@ejgallego, ejgallego/coq-lsp#751) - [fleche] Enable sharing of `.vo` file parsing. This enables better sharing, achieving an almost 50% memory reduction for example when opening all of HoTT .v files (@ejgallego, @SkySkimmer, @bhaktishh, ejgallego/coq-lsp#744) - [memo] Provide API to query Hashtbl stats (@ejgallego, ejgallego/coq-lsp#753) - [nix] Add `pet-server` deps to flake.nix (Léo Stefanesco, ejgallego/coq-lsp#754) - [coq-lsp] Fix crash on `--help` option (Léo Stefanesco, @ejgallego, ejgallego/coq-lsp#754) - [vscode] Fix focus race when a Coq file is in column 2 (@ejgallego, ejgallego/coq-lsp#755, cc: ejgallego/coq-lsp#722, ejgallego/coq-lsp#725) - [hover] Show input howto for unicode characters on hover (@ejgallego, Léo Stefanesco, ejgallego/coq-lsp#756) - [lsp] [definition] Support for jump to definition across workspace files. The location information is obtained from `.glob` files, so it is often not perfect. (@ejgallego, ejgallego/coq-lsp#762, fixes ejgallego/coq-lsp#317) - [lsp] [hover] Show full name and provenance of identifiers (@ejgallego, ejgallego/coq-lsp#762) - [lsp] [definition] Try also to resolve and locate module imports (@ejgallego, ejgallego/coq-lsp#764) - [code] Don't start server on extension activation, unless an editor we own is active. We also auto-start the server if a document that we own is opened later (@ejgallego, ejgallego/coq-lsp#758, fixes ejgallego/coq-lsp#750) - [petanque] Allow `init` to be called multiple times (@ejgallego, @gbdrt, ejgallego/coq-lsp#766) - [petanque] Faster query for goals status after `run_tac` (@ejgallego, ejgallego/coq-lsp#768) - [petanque] New parameter `pre_commands` to `start` which allows instrumenting the goal before starting the proof (@ejgallego, Alex Sanchez-Stern ejgallego/coq-lsp#769) - [petanque] New `http_headers={yes,no}` parameter for `pet` json shell, plus some improvements on protocol handling (@ejgallego, ejgallego/coq-lsp#770) - [petanque] Make agent agnostic of environment, allowing embedding inside LSP (@ejgallego, ejgallego/coq-lsp#771) - [diagnostics] Ensure extra diagnostics info is present in all errors, not only on those sentences that did parse successfully (@ejgallego, Diego Rivera, ejgallego/coq-lsp#772) - [hover] New option `show_universes_on_hover` that will display universe data on hover (@ejgallego, @SkySkimmer, ejgallego/coq-lsp#666) - [hover] New plugin `unidiff` that will elaborate a summary of universe data a file, in particular regarding universes added at `Qed` time (@ejgallego, ejgallego/coq-lsp#773) - [fleche] Support meta-command `Abort All` (@ejgallego, ejgallego/coq-lsp#774, fixes ejgallego/coq-lsp#550) - [petanque] Allow memoization control on `petanque/run` via a new parameter `memo` (@ejgallego, ejgallego/coq-lsp#780) - [lsp] [petanque] Allow acces to `petanque` protocol from the lsp server (@ejgallego, ejgallego/coq-lsp#778) - [petanque] Always initialize a workspace. This made `pet` crash if `--root` was not used and client didn't issue the optimal `setWorkspace` call (ejgallego/coq-lsp#782, @ejgallego, @gbdrt) - [lsp] [petanque] New methods `state/eq` and `state/hash`; this allows clients to implement a client-side hash; equality is configurable with different methods; moreover, `petanque/run` can compute some extra data like state hashing without a round-trip (@ejgallego @gbdrt, ejgallego/coq-lsp#779) - [petanque] New methods to hash proof states; use proof state hash by default in petanque agent (@ejgallego, @gbdrt, ejgallego/coq-lsp#808) - [petanque] New shell method `petanque/toc` that returns a document outline in LSP-style (@ejgallego, ejgallego/coq-lsp#794)
ejgallego
added a commit
to ejgallego/opam-repository
that referenced
this issue
Aug 29, 2024
CHANGES: ----------------------------------- - [deps] merge serlib into coq-lsp. This allow us to drop the SerAPI dependency, and will greatly easy the development of tools that require AST manipulation (@ejgallego, ejgallego/coq-lsp#698) - [fleche] Remove 8.16 compatibility layer (@ejgallego, ejgallego/coq-lsp#747) - [fleche] Preserve view hint across document changes. With this change, we get local continuous checking mode when the view-port heuristic is enabled (@ejgallego, ejgallego/coq-lsp#748) - [memo] More precise hashing for Coq states, this improves cache performance quite a bit (@ejgallego, ejgallego/coq-lsp#751) - [fleche] Enable sharing of `.vo` file parsing. This enables better sharing, achieving an almost 50% memory reduction for example when opening all of HoTT .v files (@ejgallego, @SkySkimmer, @bhaktishh, ejgallego/coq-lsp#744) - [memo] Provide API to query Hashtbl stats (@ejgallego, ejgallego/coq-lsp#753) - [nix] Add `pet-server` deps to flake.nix (Léo Stefanesco, ejgallego/coq-lsp#754) - [coq-lsp] Fix crash on `--help` option (Léo Stefanesco, @ejgallego, ejgallego/coq-lsp#754) - [vscode] Fix focus race when a Coq file is in column 2 (@ejgallego, ejgallego/coq-lsp#755, cc: ejgallego/coq-lsp#722, ejgallego/coq-lsp#725) - [hover] Show input howto for unicode characters on hover (@ejgallego, Léo Stefanesco, ejgallego/coq-lsp#756) - [lsp] [definition] Support for jump to definition across workspace files. The location information is obtained from `.glob` files, so it is often not perfect. (@ejgallego, ejgallego/coq-lsp#762, fixes ejgallego/coq-lsp#317) - [lsp] [hover] Show full name and provenance of identifiers (@ejgallego, ejgallego/coq-lsp#762) - [lsp] [definition] Try also to resolve and locate module imports (@ejgallego, ejgallego/coq-lsp#764) - [code] Don't start server on extension activation, unless an editor we own is active. We also auto-start the server if a document that we own is opened later (@ejgallego, ejgallego/coq-lsp#758, fixes ejgallego/coq-lsp#750) - [petanque] Allow `init` to be called multiple times (@ejgallego, @gbdrt, ejgallego/coq-lsp#766) - [petanque] Faster query for goals status after `run_tac` (@ejgallego, ejgallego/coq-lsp#768) - [petanque] New parameter `pre_commands` to `start` which allows instrumenting the goal before starting the proof (@ejgallego, Alex Sanchez-Stern ejgallego/coq-lsp#769) - [petanque] New `http_headers={yes,no}` parameter for `pet` json shell, plus some improvements on protocol handling (@ejgallego, ejgallego/coq-lsp#770) - [petanque] Make agent agnostic of environment, allowing embedding inside LSP (@ejgallego, ejgallego/coq-lsp#771) - [diagnostics] Ensure extra diagnostics info is present in all errors, not only on those sentences that did parse successfully (@ejgallego, Diego Rivera, ejgallego/coq-lsp#772) - [hover] New option `show_universes_on_hover` that will display universe data on hover (@ejgallego, @SkySkimmer, ejgallego/coq-lsp#666) - [hover] New plugin `unidiff` that will elaborate a summary of universe data a file, in particular regarding universes added at `Qed` time (@ejgallego, ejgallego/coq-lsp#773) - [fleche] Support meta-command `Abort All` (@ejgallego, ejgallego/coq-lsp#774, fixes ejgallego/coq-lsp#550) - [petanque] Allow memoization control on `petanque/run` via a new parameter `memo` (@ejgallego, ejgallego/coq-lsp#780) - [lsp] [petanque] Allow acces to `petanque` protocol from the lsp server (@ejgallego, ejgallego/coq-lsp#778) - [petanque] Always initialize a workspace. This made `pet` crash if `--root` was not used and client didn't issue the optimal `setWorkspace` call (ejgallego/coq-lsp#782, @ejgallego, @gbdrt) - [lsp] [petanque] New methods `state/eq` and `state/hash`; this allows clients to implement a client-side hash; equality is configurable with different methods; moreover, `petanque/run` can compute some extra data like state hashing without a round-trip (@ejgallego @gbdrt, ejgallego/coq-lsp#779) - [petanque] New methods to hash proof states; use proof state hash by default in petanque agent (@ejgallego, @gbdrt, ejgallego/coq-lsp#808) - [petanque] New shell method `petanque/toc` that returns a document outline in LSP-style (@ejgallego, ejgallego/coq-lsp#794)
ejgallego
added a commit
to ejgallego/opam-repository
that referenced
this issue
Aug 29, 2024
CHANGES: ----------------------------------- - [deps] merge serlib into coq-lsp. This allow us to drop the SerAPI dependency, and will greatly easy the development of tools that require AST manipulation (@ejgallego, ejgallego/coq-lsp#698) - [fleche] Remove 8.16 compatibility layer (@ejgallego, ejgallego/coq-lsp#747) - [fleche] Preserve view hint across document changes. With this change, we get local continuous checking mode when the view-port heuristic is enabled (@ejgallego, ejgallego/coq-lsp#748) - [memo] More precise hashing for Coq states, this improves cache performance quite a bit (@ejgallego, ejgallego/coq-lsp#751) - [fleche] Enable sharing of `.vo` file parsing. This enables better sharing, achieving an almost 50% memory reduction for example when opening all of HoTT .v files (@ejgallego, @SkySkimmer, @bhaktishh, ejgallego/coq-lsp#744) - [memo] Provide API to query Hashtbl stats (@ejgallego, ejgallego/coq-lsp#753) - [nix] Add `pet-server` deps to flake.nix (Léo Stefanesco, ejgallego/coq-lsp#754) - [coq-lsp] Fix crash on `--help` option (Léo Stefanesco, @ejgallego, ejgallego/coq-lsp#754) - [vscode] Fix focus race when a Coq file is in column 2 (@ejgallego, ejgallego/coq-lsp#755, cc: ejgallego/coq-lsp#722, ejgallego/coq-lsp#725) - [hover] Show input howto for unicode characters on hover (@ejgallego, Léo Stefanesco, ejgallego/coq-lsp#756) - [lsp] [definition] Support for jump to definition across workspace files. The location information is obtained from `.glob` files, so it is often not perfect. (@ejgallego, ejgallego/coq-lsp#762, fixes ejgallego/coq-lsp#317) - [lsp] [hover] Show full name and provenance of identifiers (@ejgallego, ejgallego/coq-lsp#762) - [lsp] [definition] Try also to resolve and locate module imports (@ejgallego, ejgallego/coq-lsp#764) - [code] Don't start server on extension activation, unless an editor we own is active. We also auto-start the server if a document that we own is opened later (@ejgallego, ejgallego/coq-lsp#758, fixes ejgallego/coq-lsp#750) - [petanque] Allow `init` to be called multiple times (@ejgallego, @gbdrt, ejgallego/coq-lsp#766) - [petanque] Faster query for goals status after `run_tac` (@ejgallego, ejgallego/coq-lsp#768) - [petanque] New parameter `pre_commands` to `start` which allows instrumenting the goal before starting the proof (@ejgallego, Alex Sanchez-Stern ejgallego/coq-lsp#769) - [petanque] New `http_headers={yes,no}` parameter for `pet` json shell, plus some improvements on protocol handling (@ejgallego, ejgallego/coq-lsp#770) - [petanque] Make agent agnostic of environment, allowing embedding inside LSP (@ejgallego, ejgallego/coq-lsp#771) - [diagnostics] Ensure extra diagnostics info is present in all errors, not only on those sentences that did parse successfully (@ejgallego, Diego Rivera, ejgallego/coq-lsp#772) - [hover] New option `show_universes_on_hover` that will display universe data on hover (@ejgallego, @SkySkimmer, ejgallego/coq-lsp#666) - [hover] New plugin `unidiff` that will elaborate a summary of universe data a file, in particular regarding universes added at `Qed` time (@ejgallego, ejgallego/coq-lsp#773) - [fleche] Support meta-command `Abort All` (@ejgallego, ejgallego/coq-lsp#774, fixes ejgallego/coq-lsp#550) - [petanque] Allow memoization control on `petanque/run` via a new parameter `memo` (@ejgallego, ejgallego/coq-lsp#780) - [lsp] [petanque] Allow acces to `petanque` protocol from the lsp server (@ejgallego, ejgallego/coq-lsp#778) - [petanque] Always initialize a workspace. This made `pet` crash if `--root` was not used and client didn't issue the optimal `setWorkspace` call (ejgallego/coq-lsp#782, @ejgallego, @gbdrt) - [lsp] [petanque] New methods `state/eq` and `state/hash`; this allows clients to implement a client-side hash; equality is configurable with different methods; moreover, `petanque/run` can compute some extra data like state hashing without a round-trip (@ejgallego @gbdrt, ejgallego/coq-lsp#779) - [petanque] New methods to hash proof states; use proof state hash by default in petanque agent (@ejgallego, @gbdrt, ejgallego/coq-lsp#808) - [petanque] New shell method `petanque/toc` that returns a document outline in LSP-style (@ejgallego, ejgallego/coq-lsp#794)
ejgallego
added a commit
to ejgallego/opam-repository
that referenced
this issue
Aug 29, 2024
CHANGES: ----------------------------------- - [deps] merge serlib into coq-lsp. This allow us to drop the SerAPI dependency, and will greatly easy the development of tools that require AST manipulation (@ejgallego, ejgallego/coq-lsp#698) - [fleche] Remove 8.16 compatibility layer (@ejgallego, ejgallego/coq-lsp#747) - [fleche] Preserve view hint across document changes. With this change, we get local continuous checking mode when the view-port heuristic is enabled (@ejgallego, ejgallego/coq-lsp#748) - [memo] More precise hashing for Coq states, this improves cache performance quite a bit (@ejgallego, ejgallego/coq-lsp#751) - [fleche] Enable sharing of `.vo` file parsing. This enables better sharing, achieving an almost 50% memory reduction for example when opening all of HoTT .v files (@ejgallego, @SkySkimmer, @bhaktishh, ejgallego/coq-lsp#744) - [memo] Provide API to query Hashtbl stats (@ejgallego, ejgallego/coq-lsp#753) - [nix] Add `pet-server` deps to flake.nix (Léo Stefanesco, ejgallego/coq-lsp#754) - [coq-lsp] Fix crash on `--help` option (Léo Stefanesco, @ejgallego, ejgallego/coq-lsp#754) - [vscode] Fix focus race when a Coq file is in column 2 (@ejgallego, ejgallego/coq-lsp#755, cc: ejgallego/coq-lsp#722, ejgallego/coq-lsp#725) - [hover] Show input howto for unicode characters on hover (@ejgallego, Léo Stefanesco, ejgallego/coq-lsp#756) - [lsp] [definition] Support for jump to definition across workspace files. The location information is obtained from `.glob` files, so it is often not perfect. (@ejgallego, ejgallego/coq-lsp#762, fixes ejgallego/coq-lsp#317) - [lsp] [hover] Show full name and provenance of identifiers (@ejgallego, ejgallego/coq-lsp#762) - [lsp] [definition] Try also to resolve and locate module imports (@ejgallego, ejgallego/coq-lsp#764) - [code] Don't start server on extension activation, unless an editor we own is active. We also auto-start the server if a document that we own is opened later (@ejgallego, ejgallego/coq-lsp#758, fixes ejgallego/coq-lsp#750) - [petanque] Allow `init` to be called multiple times (@ejgallego, @gbdrt, ejgallego/coq-lsp#766) - [petanque] Faster query for goals status after `run_tac` (@ejgallego, ejgallego/coq-lsp#768) - [petanque] New parameter `pre_commands` to `start` which allows instrumenting the goal before starting the proof (@ejgallego, Alex Sanchez-Stern ejgallego/coq-lsp#769) - [petanque] New `http_headers={yes,no}` parameter for `pet` json shell, plus some improvements on protocol handling (@ejgallego, ejgallego/coq-lsp#770) - [petanque] Make agent agnostic of environment, allowing embedding inside LSP (@ejgallego, ejgallego/coq-lsp#771) - [diagnostics] Ensure extra diagnostics info is present in all errors, not only on those sentences that did parse successfully (@ejgallego, Diego Rivera, ejgallego/coq-lsp#772) - [hover] New option `show_universes_on_hover` that will display universe data on hover (@ejgallego, @SkySkimmer, ejgallego/coq-lsp#666) - [hover] New plugin `unidiff` that will elaborate a summary of universe data a file, in particular regarding universes added at `Qed` time (@ejgallego, ejgallego/coq-lsp#773) - [fleche] Support meta-command `Abort All` (@ejgallego, ejgallego/coq-lsp#774, fixes ejgallego/coq-lsp#550) - [petanque] Allow memoization control on `petanque/run` via a new parameter `memo` (@ejgallego, ejgallego/coq-lsp#780) - [lsp] [petanque] Allow acces to `petanque` protocol from the lsp server (@ejgallego, ejgallego/coq-lsp#778) - [petanque] Always initialize a workspace. This made `pet` crash if `--root` was not used and client didn't issue the optimal `setWorkspace` call (ejgallego/coq-lsp#782, @ejgallego, @gbdrt) - [lsp] [petanque] New methods `state/eq` and `state/hash`; this allows clients to implement a client-side hash; equality is configurable with different methods; moreover, `petanque/run` can compute some extra data like state hashing without a round-trip (@ejgallego @gbdrt, ejgallego/coq-lsp#779) - [petanque] New methods to hash proof states; use proof state hash by default in petanque agent (@ejgallego, @gbdrt, ejgallego/coq-lsp#808) - [petanque] New shell method `petanque/toc` that returns a document outline in LSP-style (@ejgallego, ejgallego/coq-lsp#794)
avsm
pushed a commit
to avsm/opam-repository
that referenced
this issue
Sep 5, 2024
CHANGES: ----------------------------------- - [deps] merge serlib into coq-lsp. This allow us to drop the SerAPI dependency, and will greatly easy the development of tools that require AST manipulation (@ejgallego, ejgallego/coq-lsp#698) - [fleche] Remove 8.16 compatibility layer (@ejgallego, ejgallego/coq-lsp#747) - [fleche] Preserve view hint across document changes. With this change, we get local continuous checking mode when the view-port heuristic is enabled (@ejgallego, ejgallego/coq-lsp#748) - [memo] More precise hashing for Coq states, this improves cache performance quite a bit (@ejgallego, ejgallego/coq-lsp#751) - [fleche] Enable sharing of `.vo` file parsing. This enables better sharing, achieving an almost 50% memory reduction for example when opening all of HoTT .v files (@ejgallego, @SkySkimmer, @bhaktishh, ejgallego/coq-lsp#744) - [memo] Provide API to query Hashtbl stats (@ejgallego, ejgallego/coq-lsp#753) - [nix] Add `pet-server` deps to flake.nix (Léo Stefanesco, ejgallego/coq-lsp#754) - [coq-lsp] Fix crash on `--help` option (Léo Stefanesco, @ejgallego, ejgallego/coq-lsp#754) - [vscode] Fix focus race when a Coq file is in column 2 (@ejgallego, ejgallego/coq-lsp#755, cc: ejgallego/coq-lsp#722, ejgallego/coq-lsp#725) - [hover] Show input howto for unicode characters on hover (@ejgallego, Léo Stefanesco, ejgallego/coq-lsp#756) - [lsp] [definition] Support for jump to definition across workspace files. The location information is obtained from `.glob` files, so it is often not perfect. (@ejgallego, ejgallego/coq-lsp#762, fixes ejgallego/coq-lsp#317) - [lsp] [hover] Show full name and provenance of identifiers (@ejgallego, ejgallego/coq-lsp#762) - [lsp] [definition] Try also to resolve and locate module imports (@ejgallego, ejgallego/coq-lsp#764) - [code] Don't start server on extension activation, unless an editor we own is active. We also auto-start the server if a document that we own is opened later (@ejgallego, ejgallego/coq-lsp#758, fixes ejgallego/coq-lsp#750) - [petanque] Allow `init` to be called multiple times (@ejgallego, @gbdrt, ejgallego/coq-lsp#766) - [petanque] Faster query for goals status after `run_tac` (@ejgallego, ejgallego/coq-lsp#768) - [petanque] New parameter `pre_commands` to `start` which allows instrumenting the goal before starting the proof (@ejgallego, Alex Sanchez-Stern ejgallego/coq-lsp#769) - [petanque] New `http_headers={yes,no}` parameter for `pet` json shell, plus some improvements on protocol handling (@ejgallego, ejgallego/coq-lsp#770) - [petanque] Make agent agnostic of environment, allowing embedding inside LSP (@ejgallego, ejgallego/coq-lsp#771) - [diagnostics] Ensure extra diagnostics info is present in all errors, not only on those sentences that did parse successfully (@ejgallego, Diego Rivera, ejgallego/coq-lsp#772) - [hover] New option `show_universes_on_hover` that will display universe data on hover (@ejgallego, @SkySkimmer, ejgallego/coq-lsp#666) - [hover] New plugin `unidiff` that will elaborate a summary of universe data a file, in particular regarding universes added at `Qed` time (@ejgallego, ejgallego/coq-lsp#773) - [fleche] Support meta-command `Abort All` (@ejgallego, ejgallego/coq-lsp#774, fixes ejgallego/coq-lsp#550) - [petanque] Allow memoization control on `petanque/run` via a new parameter `memo` (@ejgallego, ejgallego/coq-lsp#780) - [lsp] [petanque] Allow acces to `petanque` protocol from the lsp server (@ejgallego, ejgallego/coq-lsp#778) - [petanque] Always initialize a workspace. This made `pet` crash if `--root` was not used and client didn't issue the optimal `setWorkspace` call (ejgallego/coq-lsp#782, @ejgallego, @gbdrt) - [lsp] [petanque] New methods `state/eq` and `state/hash`; this allows clients to implement a client-side hash; equality is configurable with different methods; moreover, `petanque/run` can compute some extra data like state hashing without a round-trip (@ejgallego @gbdrt, ejgallego/coq-lsp#779) - [petanque] New methods to hash proof states; use proof state hash by default in petanque agent (@ejgallego, @gbdrt, ejgallego/coq-lsp#808) - [petanque] New shell method `petanque/toc` that returns a document outline in LSP-style (@ejgallego, ejgallego/coq-lsp#794)
avsm
pushed a commit
to avsm/opam-repository
that referenced
this issue
Sep 5, 2024
CHANGES: ----------------------------------- - [deps] merge serlib into coq-lsp. This allow us to drop the SerAPI dependency, and will greatly easy the development of tools that require AST manipulation (@ejgallego, ejgallego/coq-lsp#698) - [fleche] Remove 8.16 compatibility layer (@ejgallego, ejgallego/coq-lsp#747) - [fleche] Preserve view hint across document changes. With this change, we get local continuous checking mode when the view-port heuristic is enabled (@ejgallego, ejgallego/coq-lsp#748) - [memo] More precise hashing for Coq states, this improves cache performance quite a bit (@ejgallego, ejgallego/coq-lsp#751) - [fleche] Enable sharing of `.vo` file parsing. This enables better sharing, achieving an almost 50% memory reduction for example when opening all of HoTT .v files (@ejgallego, @SkySkimmer, @bhaktishh, ejgallego/coq-lsp#744) - [memo] Provide API to query Hashtbl stats (@ejgallego, ejgallego/coq-lsp#753) - [nix] Add `pet-server` deps to flake.nix (Léo Stefanesco, ejgallego/coq-lsp#754) - [coq-lsp] Fix crash on `--help` option (Léo Stefanesco, @ejgallego, ejgallego/coq-lsp#754) - [vscode] Fix focus race when a Coq file is in column 2 (@ejgallego, ejgallego/coq-lsp#755, cc: ejgallego/coq-lsp#722, ejgallego/coq-lsp#725) - [hover] Show input howto for unicode characters on hover (@ejgallego, Léo Stefanesco, ejgallego/coq-lsp#756) - [lsp] [definition] Support for jump to definition across workspace files. The location information is obtained from `.glob` files, so it is often not perfect. (@ejgallego, ejgallego/coq-lsp#762, fixes ejgallego/coq-lsp#317) - [lsp] [hover] Show full name and provenance of identifiers (@ejgallego, ejgallego/coq-lsp#762) - [lsp] [definition] Try also to resolve and locate module imports (@ejgallego, ejgallego/coq-lsp#764) - [code] Don't start server on extension activation, unless an editor we own is active. We also auto-start the server if a document that we own is opened later (@ejgallego, ejgallego/coq-lsp#758, fixes ejgallego/coq-lsp#750) - [petanque] Allow `init` to be called multiple times (@ejgallego, @gbdrt, ejgallego/coq-lsp#766) - [petanque] Faster query for goals status after `run_tac` (@ejgallego, ejgallego/coq-lsp#768) - [petanque] New parameter `pre_commands` to `start` which allows instrumenting the goal before starting the proof (@ejgallego, Alex Sanchez-Stern ejgallego/coq-lsp#769) - [petanque] New `http_headers={yes,no}` parameter for `pet` json shell, plus some improvements on protocol handling (@ejgallego, ejgallego/coq-lsp#770) - [petanque] Make agent agnostic of environment, allowing embedding inside LSP (@ejgallego, ejgallego/coq-lsp#771) - [diagnostics] Ensure extra diagnostics info is present in all errors, not only on those sentences that did parse successfully (@ejgallego, Diego Rivera, ejgallego/coq-lsp#772) - [hover] New option `show_universes_on_hover` that will display universe data on hover (@ejgallego, @SkySkimmer, ejgallego/coq-lsp#666) - [hover] New plugin `unidiff` that will elaborate a summary of universe data a file, in particular regarding universes added at `Qed` time (@ejgallego, ejgallego/coq-lsp#773) - [fleche] Support meta-command `Abort All` (@ejgallego, ejgallego/coq-lsp#774, fixes ejgallego/coq-lsp#550) - [petanque] Allow memoization control on `petanque/run` via a new parameter `memo` (@ejgallego, ejgallego/coq-lsp#780) - [lsp] [petanque] Allow acces to `petanque` protocol from the lsp server (@ejgallego, ejgallego/coq-lsp#778) - [petanque] Always initialize a workspace. This made `pet` crash if `--root` was not used and client didn't issue the optimal `setWorkspace` call (ejgallego/coq-lsp#782, @ejgallego, @gbdrt) - [lsp] [petanque] New methods `state/eq` and `state/hash`; this allows clients to implement a client-side hash; equality is configurable with different methods; moreover, `petanque/run` can compute some extra data like state hashing without a round-trip (@ejgallego @gbdrt, ejgallego/coq-lsp#779) - [petanque] New methods to hash proof states; use proof state hash by default in petanque agent (@ejgallego, @gbdrt, ejgallego/coq-lsp#808) - [petanque] New shell method `petanque/toc` that returns a document outline in LSP-style (@ejgallego, ejgallego/coq-lsp#794)
avsm
pushed a commit
to avsm/opam-repository
that referenced
this issue
Sep 5, 2024
CHANGES: ----------------------------------- - [deps] merge serlib into coq-lsp. This allow us to drop the SerAPI dependency, and will greatly easy the development of tools that require AST manipulation (@ejgallego, ejgallego/coq-lsp#698) - [fleche] Remove 8.16 compatibility layer (@ejgallego, ejgallego/coq-lsp#747) - [fleche] Preserve view hint across document changes. With this change, we get local continuous checking mode when the view-port heuristic is enabled (@ejgallego, ejgallego/coq-lsp#748) - [memo] More precise hashing for Coq states, this improves cache performance quite a bit (@ejgallego, ejgallego/coq-lsp#751) - [fleche] Enable sharing of `.vo` file parsing. This enables better sharing, achieving an almost 50% memory reduction for example when opening all of HoTT .v files (@ejgallego, @SkySkimmer, @bhaktishh, ejgallego/coq-lsp#744) - [memo] Provide API to query Hashtbl stats (@ejgallego, ejgallego/coq-lsp#753) - [nix] Add `pet-server` deps to flake.nix (Léo Stefanesco, ejgallego/coq-lsp#754) - [coq-lsp] Fix crash on `--help` option (Léo Stefanesco, @ejgallego, ejgallego/coq-lsp#754) - [vscode] Fix focus race when a Coq file is in column 2 (@ejgallego, ejgallego/coq-lsp#755, cc: ejgallego/coq-lsp#722, ejgallego/coq-lsp#725) - [hover] Show input howto for unicode characters on hover (@ejgallego, Léo Stefanesco, ejgallego/coq-lsp#756) - [lsp] [definition] Support for jump to definition across workspace files. The location information is obtained from `.glob` files, so it is often not perfect. (@ejgallego, ejgallego/coq-lsp#762, fixes ejgallego/coq-lsp#317) - [lsp] [hover] Show full name and provenance of identifiers (@ejgallego, ejgallego/coq-lsp#762) - [lsp] [definition] Try also to resolve and locate module imports (@ejgallego, ejgallego/coq-lsp#764) - [code] Don't start server on extension activation, unless an editor we own is active. We also auto-start the server if a document that we own is opened later (@ejgallego, ejgallego/coq-lsp#758, fixes ejgallego/coq-lsp#750) - [petanque] Allow `init` to be called multiple times (@ejgallego, @gbdrt, ejgallego/coq-lsp#766) - [petanque] Faster query for goals status after `run_tac` (@ejgallego, ejgallego/coq-lsp#768) - [petanque] New parameter `pre_commands` to `start` which allows instrumenting the goal before starting the proof (@ejgallego, Alex Sanchez-Stern ejgallego/coq-lsp#769) - [petanque] New `http_headers={yes,no}` parameter for `pet` json shell, plus some improvements on protocol handling (@ejgallego, ejgallego/coq-lsp#770) - [petanque] Make agent agnostic of environment, allowing embedding inside LSP (@ejgallego, ejgallego/coq-lsp#771) - [diagnostics] Ensure extra diagnostics info is present in all errors, not only on those sentences that did parse successfully (@ejgallego, Diego Rivera, ejgallego/coq-lsp#772) - [hover] New option `show_universes_on_hover` that will display universe data on hover (@ejgallego, @SkySkimmer, ejgallego/coq-lsp#666) - [hover] New plugin `unidiff` that will elaborate a summary of universe data a file, in particular regarding universes added at `Qed` time (@ejgallego, ejgallego/coq-lsp#773) - [fleche] Support meta-command `Abort All` (@ejgallego, ejgallego/coq-lsp#774, fixes ejgallego/coq-lsp#550) - [petanque] Allow memoization control on `petanque/run` via a new parameter `memo` (@ejgallego, ejgallego/coq-lsp#780) - [lsp] [petanque] Allow acces to `petanque` protocol from the lsp server (@ejgallego, ejgallego/coq-lsp#778) - [petanque] Always initialize a workspace. This made `pet` crash if `--root` was not used and client didn't issue the optimal `setWorkspace` call (ejgallego/coq-lsp#782, @ejgallego, @gbdrt) - [lsp] [petanque] New methods `state/eq` and `state/hash`; this allows clients to implement a client-side hash; equality is configurable with different methods; moreover, `petanque/run` can compute some extra data like state hashing without a round-trip (@ejgallego @gbdrt, ejgallego/coq-lsp#779) - [petanque] New methods to hash proof states; use proof state hash by default in petanque agent (@ejgallego, @gbdrt, ejgallego/coq-lsp#808) - [petanque] New shell method `petanque/toc` that returns a document outline in LSP-style (@ejgallego, ejgallego/coq-lsp#794)
ejgallego
added a commit
to ejgallego/opam-repository
that referenced
this issue
Sep 8, 2024
CHANGES: ----------------------------------- - [deps] merge serlib into coq-lsp. This allow us to drop the SerAPI dependency, and will greatly easy the development of tools that require AST manipulation (@ejgallego, ejgallego/coq-lsp#698) - [fleche] Remove 8.16 compatibility layer (@ejgallego, ejgallego/coq-lsp#747) - [fleche] Preserve view hint across document changes. With this change, we get local continuous checking mode when the view-port heuristic is enabled (@ejgallego, ejgallego/coq-lsp#748) - [memo] More precise hashing for Coq states, this improves cache performance quite a bit (@ejgallego, ejgallego/coq-lsp#751) - [fleche] Enable sharing of `.vo` file parsing. This enables better sharing, achieving an almost 50% memory reduction for example when opening all of HoTT .v files (@ejgallego, @SkySkimmer, @bhaktishh, ejgallego/coq-lsp#744) - [memo] Provide API to query Hashtbl stats (@ejgallego, ejgallego/coq-lsp#753) - [nix] Add `pet-server` deps to flake.nix (Léo Stefanesco, ejgallego/coq-lsp#754) - [coq-lsp] Fix crash on `--help` option (Léo Stefanesco, @ejgallego, ejgallego/coq-lsp#754) - [vscode] Fix focus race when a Coq file is in column 2 (@ejgallego, ejgallego/coq-lsp#755, cc: ejgallego/coq-lsp#722, ejgallego/coq-lsp#725) - [hover] Show input howto for unicode characters on hover (@ejgallego, Léo Stefanesco, ejgallego/coq-lsp#756) - [lsp] [definition] Support for jump to definition across workspace files. The location information is obtained from `.glob` files, so it is often not perfect. (@ejgallego, ejgallego/coq-lsp#762, fixes ejgallego/coq-lsp#317) - [lsp] [hover] Show full name and provenance of identifiers (@ejgallego, ejgallego/coq-lsp#762) - [lsp] [definition] Try also to resolve and locate module imports (@ejgallego, ejgallego/coq-lsp#764) - [code] Don't start server on extension activation, unless an editor we own is active. We also auto-start the server if a document that we own is opened later (@ejgallego, ejgallego/coq-lsp#758, fixes ejgallego/coq-lsp#750) - [petanque] Allow `init` to be called multiple times (@ejgallego, @gbdrt, ejgallego/coq-lsp#766) - [petanque] Faster query for goals status after `run_tac` (@ejgallego, ejgallego/coq-lsp#768) - [petanque] New parameter `pre_commands` to `start` which allows instrumenting the goal before starting the proof (@ejgallego, Alex Sanchez-Stern ejgallego/coq-lsp#769) - [petanque] New `http_headers={yes,no}` parameter for `pet` json shell, plus some improvements on protocol handling (@ejgallego, ejgallego/coq-lsp#770) - [petanque] Make agent agnostic of environment, allowing embedding inside LSP (@ejgallego, ejgallego/coq-lsp#771) - [diagnostics] Ensure extra diagnostics info is present in all errors, not only on those sentences that did parse successfully (@ejgallego, Diego Rivera, ejgallego/coq-lsp#772) - [hover] New option `show_universes_on_hover` that will display universe data on hover (@ejgallego, @SkySkimmer, ejgallego/coq-lsp#666) - [hover] New plugin `unidiff` that will elaborate a summary of universe data a file, in particular regarding universes added at `Qed` time (@ejgallego, ejgallego/coq-lsp#773) - [fleche] Support meta-command `Abort All` (@ejgallego, ejgallego/coq-lsp#774, fixes ejgallego/coq-lsp#550) - [petanque] Allow memoization control on `petanque/run` via a new parameter `memo` (@ejgallego, ejgallego/coq-lsp#780) - [lsp] [petanque] Allow acces to `petanque` protocol from the lsp server (@ejgallego, ejgallego/coq-lsp#778) - [petanque] Always initialize a workspace. This made `pet` crash if `--root` was not used and client didn't issue the optimal `setWorkspace` call (ejgallego/coq-lsp#782, @ejgallego, @gbdrt) - [lsp] [petanque] New methods `state/eq` and `state/hash`; this allows clients to implement a client-side hash; equality is configurable with different methods; moreover, `petanque/run` can compute some extra data like state hashing without a round-trip (@ejgallego @gbdrt, ejgallego/coq-lsp#779) - [petanque] New methods to hash proof states; use proof state hash by default in petanque agent (@ejgallego, @gbdrt, ejgallego/coq-lsp#808) - [petanque] New shell method `petanque/toc` that returns a document outline in LSP-style (@ejgallego, ejgallego/coq-lsp#794)
ejgallego
added a commit
to ejgallego/opam-repository
that referenced
this issue
Sep 8, 2024
CHANGES: ----------------------------------- - [deps] merge serlib into coq-lsp. This allow us to drop the SerAPI dependency, and will greatly easy the development of tools that require AST manipulation (@ejgallego, ejgallego/coq-lsp#698) - [fleche] Remove 8.16 compatibility layer (@ejgallego, ejgallego/coq-lsp#747) - [fleche] Preserve view hint across document changes. With this change, we get local continuous checking mode when the view-port heuristic is enabled (@ejgallego, ejgallego/coq-lsp#748) - [memo] More precise hashing for Coq states, this improves cache performance quite a bit (@ejgallego, ejgallego/coq-lsp#751) - [fleche] Enable sharing of `.vo` file parsing. This enables better sharing, achieving an almost 50% memory reduction for example when opening all of HoTT .v files (@ejgallego, @SkySkimmer, @bhaktishh, ejgallego/coq-lsp#744) - [memo] Provide API to query Hashtbl stats (@ejgallego, ejgallego/coq-lsp#753) - [nix] Add `pet-server` deps to flake.nix (Léo Stefanesco, ejgallego/coq-lsp#754) - [coq-lsp] Fix crash on `--help` option (Léo Stefanesco, @ejgallego, ejgallego/coq-lsp#754) - [vscode] Fix focus race when a Coq file is in column 2 (@ejgallego, ejgallego/coq-lsp#755, cc: ejgallego/coq-lsp#722, ejgallego/coq-lsp#725) - [hover] Show input howto for unicode characters on hover (@ejgallego, Léo Stefanesco, ejgallego/coq-lsp#756) - [lsp] [definition] Support for jump to definition across workspace files. The location information is obtained from `.glob` files, so it is often not perfect. (@ejgallego, ejgallego/coq-lsp#762, fixes ejgallego/coq-lsp#317) - [lsp] [hover] Show full name and provenance of identifiers (@ejgallego, ejgallego/coq-lsp#762) - [lsp] [definition] Try also to resolve and locate module imports (@ejgallego, ejgallego/coq-lsp#764) - [code] Don't start server on extension activation, unless an editor we own is active. We also auto-start the server if a document that we own is opened later (@ejgallego, ejgallego/coq-lsp#758, fixes ejgallego/coq-lsp#750) - [petanque] Allow `init` to be called multiple times (@ejgallego, @gbdrt, ejgallego/coq-lsp#766) - [petanque] Faster query for goals status after `run_tac` (@ejgallego, ejgallego/coq-lsp#768) - [petanque] New parameter `pre_commands` to `start` which allows instrumenting the goal before starting the proof (@ejgallego, Alex Sanchez-Stern ejgallego/coq-lsp#769) - [petanque] New `http_headers={yes,no}` parameter for `pet` json shell, plus some improvements on protocol handling (@ejgallego, ejgallego/coq-lsp#770) - [petanque] Make agent agnostic of environment, allowing embedding inside LSP (@ejgallego, ejgallego/coq-lsp#771) - [diagnostics] Ensure extra diagnostics info is present in all errors, not only on those sentences that did parse successfully (@ejgallego, Diego Rivera, ejgallego/coq-lsp#772) - [hover] New option `show_universes_on_hover` that will display universe data on hover (@ejgallego, @SkySkimmer, ejgallego/coq-lsp#666) - [hover] New plugin `unidiff` that will elaborate a summary of universe data a file, in particular regarding universes added at `Qed` time (@ejgallego, ejgallego/coq-lsp#773) - [fleche] Support meta-command `Abort All` (@ejgallego, ejgallego/coq-lsp#774, fixes ejgallego/coq-lsp#550) - [petanque] Allow memoization control on `petanque/run` via a new parameter `memo` (@ejgallego, ejgallego/coq-lsp#780) - [lsp] [petanque] Allow acces to `petanque` protocol from the lsp server (@ejgallego, ejgallego/coq-lsp#778) - [petanque] Always initialize a workspace. This made `pet` crash if `--root` was not used and client didn't issue the optimal `setWorkspace` call (ejgallego/coq-lsp#782, @ejgallego, @gbdrt) - [lsp] [petanque] New methods `state/eq` and `state/hash`; this allows clients to implement a client-side hash; equality is configurable with different methods; moreover, `petanque/run` can compute some extra data like state hashing without a round-trip (@ejgallego @gbdrt, ejgallego/coq-lsp#779) - [petanque] New methods to hash proof states; use proof state hash by default in petanque agent (@ejgallego, @gbdrt, ejgallego/coq-lsp#808) - [petanque] New shell method `petanque/toc` that returns a document outline in LSP-style (@ejgallego, ejgallego/coq-lsp#794)
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Thank you for developing coq-lsp!
I use many opam switches, most of which don't have coq-lsp installed.
With the new activation criteria (#737), when I open a project unrelated to Coq, e.g. containing only LaTeX and a Markdown readme, the extension activates and shows an error message about failing to connect to the LSP server, along with a rather obtrusive, persistent red section in the status bar.
Would it be possible to not activate the extension, or perhaps not show errors, if connecting to coq-lsp fails because it isn't installed?
The text was updated successfully, but these errors were encountered: