Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

[petanque] Hash proof states instead of system states #808

Merged
merged 1 commit into from
Jul 18, 2024
Merged

Conversation

ejgallego
Copy link
Owner

No description provided.

@ejgallego ejgallego added this to the 0.2.0 milestone Jul 18, 2024
@ejgallego ejgallego merged commit c417d1e into main Jul 18, 2024
13 checks passed
@ejgallego ejgallego deleted the hash_proof branch July 18, 2024 19:20
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
Labels
Projects
None yet
Development

Successfully merging this pull request may close these issues.

1 participant