[lsp] [petanque] Allow access to petanque protocol from the lsp server
#778
Conversation
This file contains 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
ejgallego
force-pushed
the
petanque_lsp
branch
3 times, most recently
from
0016c2b to
1561f86
Compare
ejgallego
added
part: petanque
part: lsp server
kind: enhancement
ejgallego
force-pushed
the
petanque_lsp
branch
2 times, most recently
from
11cf979 to
5c5aa8b
Compare
…ver. This will be very useful for quite a few users, in particular those willing to interact with Coq from an editor context. Things integrate pretty well, and `petanque` can demand `Flèche` to build documents, etc... Note that we can still improve the codebase a bit, in particular: - we should share the generic handling code between `controller` and `petanque`. - note also the lack of uniformity w.r.t. the cancellation token and Rq.serve, in particular `Rq.Immediate` and `Rq.query` with result `Now` should do the same.
ejgallego
added a commit
to ejgallego/opam-repository
that referenced
this pull request
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 pull request
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 pull request
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 pull request
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 pull request
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 pull request
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 pull request
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 pull request
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 pull request
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 pull request
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 pull request
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 pull request
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 pull request
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 pull request
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 pull request
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 pull request
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
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 will be very useful for quite a few users, in particular those
willing to interact with Coq from an editor context.
Things integrate pretty well, and
petanquecan demandFlèchetobuild documents, etc...
Note that we can still improve the codebase a bit, in particular:
we should share the generic handling code between
controllerandpetanque.note also the lack of uniformity w.r.t. the cancellation token and
Rq.serve, in particular
Rq.ImmediateandRq.querywith resultNowshould do the same.