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.

Sign up for GitHub

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

Jump to bottom

[build] [deps] Merge serlib into coq-lsp #698

Merged
merged 5 commits into from
May 31, 2024
Merged

[build] [deps] Merge serlib into coq-lsp #698

merged 5 commits into from
May 31, 2024

Conversation

ejgallego
Copy link
Owner

@ejgallego ejgallego commented May 9, 2024 •
edited
Loading

It makes a lot more sense for us to develop serlib natively here, as we need new exclusive functionalities and the submodules are not bringing us a lot.

I guess we will reverse the dependency and have sertop depend on coq-lsp serlib's, if that's still needed.

TODO:

@ejgallego ejgallego mentioned this pull request May 9, 2024
Merged
@ejgallego ejgallego force-pushed the serlib_merge branch 5 times, most recently from 7cffef1 to bd4545e Compare May 9, 2024 14:07
@Alizter
Copy link
Collaborator

Alizter commented May 9, 2024

What happens to the opam package? Do you just switch the source?

@ejgallego ejgallego force-pushed the serlib_merge branch 2 times, most recently from 260f585 to 2ea69ce Compare May 9, 2024 14:50
@ejgallego
Copy link
Owner Author

What happens to the opam package? Do you just switch the source?

coq-lsp wont' depend anymore on coq-serapi

Newer coq-serapi will depend on coq-lsp, if there is a new release tho, likely the last.

@ejgallego ejgallego force-pushed the serlib_merge branch 5 times, most recently from a0ea620 to 7ed2cea Compare May 10, 2024 08:28
@ejgallego ejgallego added this to the 0.1.10 milestone May 10, 2024
@ejgallego ejgallego modified the milestones: 0.1.9.1, 0.2.0 May 31, 2024
@ejgallego ejgallego force-pushed the serlib_merge branch 2 times, most recently from 3a59113 to 55b7d5d Compare May 31, 2024 14:45
@ejgallego ejgallego deleted the serlib_merge branch May 31, 2024 15:49
@ejgallego ejgallego mentioned this pull request Jul 2, 2024
Closed
@ejgallego ejgallego mentioned this pull request Aug 29, 2024
Merged
ejgallego added a commit to ejgallego/opam-repository that referenced this pull request Aug 29, 2024
@ejgallego
[new release] coq-lsp (0.2.0+8.19)
3285281 
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 ejgallego mentioned this pull request Aug 29, 2024
Merged
ejgallego added a commit to ejgallego/opam-repository that referenced this pull request Aug 29, 2024
@ejgallego
[new release] coq-lsp (0.2.0+8.18)
41af8af 
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 ejgallego mentioned this pull request Aug 29, 2024
Merged
ejgallego added a commit to ejgallego/opam-repository that referenced this pull request Aug 29, 2024
@ejgallego
[new release] coq-lsp (0.2.0+8.19)
ab06019 
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
@ejgallego
[new release] coq-lsp (0.2.0+8.17)
d27a0da 
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 ejgallego mentioned this pull request Aug 29, 2024
Merged
ejgallego added a commit to ejgallego/opam-repository that referenced this pull request Aug 29, 2024
@ejgallego
[new release] coq-lsp (0.2.0+8.17)
e532eb8 
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
@ejgallego
[new release] coq-lsp (0.2.0+8.18)
b019fab 
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
@ejgallego
[new release] coq-lsp (0.2.0+8.19)
14dc9f8 
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
@ejgallego
[new release] coq-lsp (0.2.0+8.19)
2c116c7 
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
@ejgallego
[new release] coq-lsp (0.2.0+8.19)
cba99d7 
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 that referenced this pull request Aug 29, 2024
@ejgallego
[build] [deps] Bump ppxlib toolchain to 0.26.0.
86fc9bb 
It is time to clean up this old compat setup once that #698 has been
completed; old `ppx_import` is giving us too much trouble with
`petanque`.
@ejgallego ejgallego mentioned this pull request Aug 29, 2024
Merged
ejgallego added a commit that referenced this pull request Aug 29, 2024
@ejgallego
[build] [deps] Bump ppxlib toolchain to 0.26.0.
0669ca6 
It is time to clean up this old compat setup once that #698 has been
completed; old `ppx_import` is giving us too much trouble with
`petanque`.
ejgallego added a commit that referenced this pull request Aug 29, 2024
@ejgallego
[build] [deps] Bump ppxlib toolchain to 0.26.0.
5d64905 
It is time to clean up this old compat setup once that #698 has been
completed; old `ppx_import` is giving us too much trouble with
`petanque`.
ejgallego added a commit to ejgallego/opam-repository that referenced this pull request Aug 29, 2024
@ejgallego
[new release] coq-lsp (0.2.0+8.17)
b30a0df 
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
@ejgallego
[new release] coq-lsp (0.2.0+8.18)
7c5386a 
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 that referenced this pull request Aug 30, 2024
@ejgallego
[build] [deps] Bump ppxlib toolchain to 0.26.0.
ffadc3b 
It is time to clean up this old compat setup once that #698 has been
completed; old `ppx_import` is giving us too much trouble with
`petanque`.
ejgallego added a commit that referenced this pull request Aug 30, 2024
@ejgallego
[build] [deps] Bump ppxlib toolchain to 0.26.0.
6219d34 
It is time to clean up this old compat setup once that #698 has been
completed; old `ppx_import` is giving us too much trouble with
`petanque`.
avsm pushed a commit to avsm/opam-repository that referenced this pull request Sep 5, 2024
@ejgallego @avsm
[new release] coq-lsp (0.2.0+8.18)
efc6055 
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
@ejgallego @avsm
[new release] coq-lsp (0.2.0+8.17)
25ea7ed 
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
@ejgallego @avsm
[new release] coq-lsp (0.2.0+8.19)
27471d2 
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
@ejgallego
[new release] coq-lsp (0.2.0+8.20)
bbb4aa6 
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
@ejgallego
[new release] coq-lsp (0.2.0+8.20)
9917434 
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 ejgallego mentioned this pull request Sep 16, 2024
Closed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers
No reviews
Assignees
No one assigned
Labels
kind: cleanup kind: enhancement New feature or request kind: internal kind: redesign part: build part: deps part: external tools part: ocaml part: plugins part: serlib part: upstream
Projects
None yet
Milestone
0.2.0
Development

Successfully merging this pull request may close these issues.
2 participants
@ejgallego @Alizter