[fleche] Caching / sharing of .vo contents #744
Merged
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
|
@Alizter memory use (approx) with patch, opening a lot of files in HoTT:
So while not the panacea, the reduction in memory use seems quite useful, in particular for devs with large .vo size. I'm very interested in seeing your numbers. |
|
cc: @SkySkimmer @ppedrot in case you are curious about the kind of improvements we see by sharing .vo files (in stdlib that amounts to 8% faster compilation) |
|
Loading all of HoTT in the same server: 1169 Mw to 668 Mw , quite a considerable saving @Alizter |
ejgallego
changed the title
For now we just update the types to get ready for coq/coq#17393 , we will add the cache in the next commit. Based on work from #641
This seems to achieve significant memory reduction when opening multiple .v files in the same server process.
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.
We add a basic .vo parsing cache; this often results in large memory savings when working simultaneously with several files.
Based on work from #641 and coq/coq#17393