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

[code] Preserve original focus when refocusing the panel. #725

Merged
merged 1 commit into from
May 27, 2024
Merged

[code] Preserve original focus when refocusing the panel. #725

merged 1 commit into from
May 27, 2024

Conversation

ejgallego
Copy link
Owner

This amends #722, as otherwise keyboard navigation becomes impossible.

We also amend the changelog entry (should be under main)

@ejgallego ejgallego added this to the 0.1.9 milestone May 27, 2024
@ejgallego
[code] Preserve original focus when refocusing the panel.
186cadd 
This amends #722, as otherwise keyboard navigation becomes impossible.

We also amend the changelog entry (should be under main)
@ejgallego ejgallego merged commit 1facd14 into main May 27, 2024
13 checks passed
@ejgallego ejgallego deleted the fix_focus branch May 27, 2024 10:45
ejgallego added a commit that referenced this pull request May 28, 2024
@ejgallego
[code] Amend #725
875ff90 
We indeed need to check `visible`, not `active`.
@ejgallego ejgallego mentioned this pull request May 31, 2024
Merged
ejgallego added a commit to ejgallego/opam-repository that referenced this pull request May 31, 2024
@ejgallego
[new release] coq-lsp (0.1.9+8.18)
feb250e 
CHANGES:

---------------------------------------

 - new option `show_loc_info_on_hover` that will display parsing debug
   information on hover; previous flag was fixed in code, which is way
   less flexible. This also fixes the option being on in 0.1.8 by
   mistake (@ejgallego, ejgallego/coq-lsp#588)
 - hover plugins can now access the full document, this is convenient
   for many use cases (@ejgallego, ejgallego/coq-lsp#591)
 - fix hover position computation on the presence of Utf characters
   (@ejgallego, ejgallego/coq-lsp#597, thanks to Pierre Courtieu for the report and
   example, closes ejgallego/coq-lsp#594)
 - fix activation bug that prevented extension activation for `.mv`
   files, see discussion in the issues about the upstream policy
   (@ejgallego @r3m0t, ejgallego/coq-lsp#598, cc ejgallego/coq-lsp#596, reported by Théo Zimmerman)
 - require VSCode >= 1.82 in package.json . Our VSCode extension uses
   `vscode-languageclient` 9 which imposes this. (@ejgallego, ejgallego/coq-lsp#599,
   thanks to Théo Zimmerman for the report)
 - `proof/goals` request: new `mode` parameter, to specify goals
   after/before sentence display; renamed `pretac` to `command`, as to
   provide official support for speculative execution (@ejgallego, ejgallego/coq-lsp#600)
 - fix some cases where interrupted computations where memoized
   (@ejgallego, ejgallego/coq-lsp#603)
 - [internal] Flèche [Doc.t] API will now absorb errors on document
   update and creation into the document itself. Thus, a document that
   failed to create or update is still valid, but in the right failed
   state. This is a much needed API change for a lot of use cases
   (@ejgallego, ejgallego/coq-lsp#604)
 - support OCaml 5.1.x (@ejgallego, ejgallego/coq-lsp#606)
 - update progress indicator correctly on End Of File (@ejgallego,
   ejgallego/coq-lsp#605, fixes ejgallego/coq-lsp#445)
 - [plugins] New `astdump` plugin to dump AST of files into JSON and
   SEXP (@ejgallego, ejgallego/coq-lsp#607)
 - errors on save where not properly caught (@ejgallego, ejgallego/coq-lsp#608)
 - switch default of `goal_after_tactic` to `true` (@Alizter,
   @ejgallego, cc: ejgallego/coq-lsp#614)
 - error recovery: Recognize `Defined` and `Admitted` in lex recovery
   (@ejgallego, ejgallego/coq-lsp#616)
 - completion: correctly understand UTF-16 code points on completion
   request (Léo Stefanesco, ejgallego/coq-lsp#613, fixes ejgallego/coq-lsp#531)
 - don't trigger the goals window in general markdown buffer
   (@ejgallego, ejgallego/coq-lsp#625, reported by Théo Zimmerman)
 - allow not to postpone full document requests (ejgallego/coq-lsp#626, @ejgallego)
 - new configuration value `check_only_on_request` which will delay
   checking the document until a request has been made (ejgallego/coq-lsp#629, cc: ejgallego/coq-lsp#24,
   @ejgallego)
 - fix typo on package.json configuration section (@ejgallego, ejgallego/coq-lsp#645)
 - be more resilient with invalid _CoqProject files (@ejgallego, ejgallego/coq-lsp#646)
 - support for Coq 8.16 has been abandoned due to lack of dev
   resources (@ejgallego, ejgallego/coq-lsp#649)
 - new option `--no_vo` for `fcc`, which will skip the `.vo` saving
   step. `.vo` saving is now an `fcc` plugins, but for now, it is
   enabled by default (@ejgallego, ejgallego/coq-lsp#650)
 - depend on `memprof-limits` on OCaml 4.x (@ejgallego, ejgallego/coq-lsp#660)
 - bump minimal OCaml version to 4.12 due to `memprof-limits`
   (@ejgallego, ejgallego/coq-lsp#660)
 - monitor all Coq-level calls under an interruption token
   (@ejgallego, ejgallego/coq-lsp#661)
 - interpret require thru our own custom execution env-aware path
   (@bhaktishh, @ejgallego, ejgallego/coq-lsp#642, ejgallego/coq-lsp#643, ejgallego/coq-lsp#644)
 - new `coq-lsp.plugin.goaldump` plugin, as an example on how to dump
   goals from a document (@ejgallego @gbdrt, ejgallego/coq-lsp#619)
 - new trim command (both in the server and in VSCode) to liberate
   space used in the cache (@ejgallego, ejgallego/coq-lsp#662, fixes ejgallego/coq-lsp#367 cc: ejgallego/coq-lsp#253 ejgallego/coq-lsp#236
   ejgallego/coq-lsp#348)
 - fix Coq performance view display (@ejgallego, ejgallego/coq-lsp#663, regression in
   ejgallego/coq-lsp#513)
 - Added new heatmap feature allowing timing data to be seen in the
   editor. Can be enabled with the `Coq LSP: Toggle heatmap`
   command. Can be configured to show memory usage. Colors and
   granularity are configurable. (@Alizter and @ejgallego, ejgallego/coq-lsp#686,
   grants ejgallego/coq-lsp#681).
 - allow more than one input position in `selectionRange` LSP call
   (@ejgallego, ejgallego/coq-lsp#667, fixes ejgallego/coq-lsp#663)
 - new VSCode commands to allow to move one sentence backwards /
   forward, this is particularly useful when combined with lazy
   checking mode (@ejgallego, ejgallego/coq-lsp#671, fixes ejgallego/coq-lsp#263, fixes ejgallego/coq-lsp#580)
 - VSCode commands `coq-lsp.sentenceNext` / `coq-lsp.sentencePrevious`
   are now bound by default to `Alt + N` / `Alt + P` keybindings
   (@ejgallego, ejgallego/coq-lsp#718)
 - change diagnostic `extra` field to `data`, so we now conform to the
   LSP spec, include the data only when the `send_diags_extra_data`
   server-side option is enabled (@ejgallego, ejgallego/coq-lsp#670)
 - include range of full sentence in error diagnostic extra data
   (@ejgallego, ejgallego/coq-lsp#670 , thanks to @driverag22 for the idea, cc: ejgallego/coq-lsp#663).
 - The `coq-lsp.pp_type` VSCode client option now takes effect
   immediately, no more need to restart the server to get different
   goal display formats (@ejgallego, ejgallego/coq-lsp#675)
 - new public VSCode extension API so other extensions can perform
   actions when the user request the goals (@ejgallego, @bhaktishh,
   ejgallego/coq-lsp#672, fixes ejgallego/coq-lsp#538)
 - Support Visual Studio Live Share URIs better (`vsls://`), in
   particular don't try to display goals if the URI is VSLS one
   (@ejgallego, ejgallego/coq-lsp#676)
 - New `InjectRequire` plugin API for plugins to be able to instrument
   the default import list of files (@ejgallego @corwin-of-amber,
   ejgallego/coq-lsp#679)
 - Add `--max_errors=n` option to `fcc`, this way users can set
   `--max_errors=0` to imitate `coqc` behavior (@ejgallego, ejgallego/coq-lsp#680)
 - Fix `fcc` exit status when checking terminates with fatal errors
   (@ejgallego, @Alizter, ejgallego/coq-lsp#680)
 - Fix install to OPAM switches from `main` branch (@ejgallego, ejgallego/coq-lsp#683,
   fixes ejgallego/coq-lsp#682, cc ejgallego/coq-lsp#479 ejgallego/coq-lsp#488, thanks to @HazardousPeach for the report)
 - New `--int_backend={Coq,Mp}` command line parameter to select the
   interruption method for Coq (@ejgallego, ejgallego/coq-lsp#684)
 - Update `package-lock.json` for latest bugfixes (@ejgallego, ejgallego/coq-lsp#687)
 - Update Nix flake enviroment (@Alizter, ejgallego/coq-lsp#684 ejgallego/coq-lsp#688)
 - Update `prettier` (@Alizter @ejgallego, ejgallego/coq-lsp#684 ejgallego/coq-lsp#688)
 - Store original performance data in the cache, so we now display the
   original timing and memory data even for cached commands (@ejgallego, ejgallego/coq-lsp#693)
 - Fix type errors in the Performance Data Notifications (@ejgallego,
   @Alizter, ejgallego/coq-lsp#689, ejgallego/coq-lsp#693)
 - Send performance performance data for the full document
   (@ejgallego, @Alizter, ejgallego/coq-lsp#689, ejgallego/coq-lsp#693)
 - Better types `coq/perfData` call (@ejgallego @Alizter, ejgallego/coq-lsp#689)
 - New server option to enable / disable `coq/perfData` (@ejgallego, ejgallego/coq-lsp#689)
 - New client option to enable / disable `coq/perfData` (@ejgallego, ejgallego/coq-lsp#717)
 - The `coq-lsp.document` VSCode command will now display the returned
   JSON data in a new editor (@ejgallego, ejgallego/coq-lsp#701)
 - Update server settings on the fly when tweaking them in VSCode.
   Implement `workspace/didChangeConfiguration` (@ejgallego, ejgallego/coq-lsp#702)
 - [Coq API] Add functions to retrieve list of declarations done in
   .vo files (@ejallego, @eytans, ejgallego/coq-lsp#704)
 - New `petanque` API to interact directly with Coq's proof
   engine. (@ejgallego, @gbdrt, Laetitia Teodorescu ejgallego/coq-lsp#703, thanks to
   Alex Sanchez-Stern for many insightful feedback and testing)
 - New `petanque` JSON-RPC `pet.exe`, which can be used à la SerAPI
   to perform proof search and more (@ejgallego, @gbdrt, ejgallego/coq-lsp#705)
 - New `pet-server.exe` TCP server for keep-alive sessions (@gbdrt,
   ejgallego/coq-lsp#697)
 - Always dispose UI elements. This should improve some strange
   behaviors on extension restart (@ejgallego, ejgallego/coq-lsp#708)
 - [code] Added new heatmap feature allowing timing data to be seen in
   the editor. Can be enabled with the `Coq LSP: Toggle heatmap`
   comamnd. Can be configured to show memory usage. Colors and
   granularity are configurable. (@Alizter and @ejgallego, ejgallego/coq-lsp#686,
   grants ejgallego/coq-lsp#681).
 - [server] Support Coq meta-commands (Reset, Reset Initial, Back)
   They are actually pretty useful to hint the incremental engine to
   ignore changes in some part of the document (@ejgallego, ejgallego/coq-lsp#709)
 - JSON-RPC library now supports all kind of incoming messages
   (@ejgallego, ejgallego/coq-lsp#713)
 - [code/server] New `coq/viewRange` notification, from client to
   server, than hints the scheduler for the visible area of the
   document; combined with the new lazy checking mode, this provides
   checking on scroll, a feature inspired from Isabelle IDE
   (@ejgallego, ejgallego/coq-lsp#717)
 - [code] Have VSCode wait for full LSP client shutdown on server
   restart. This fixes some bugs on extension restart (finally!)
   (@ejgallego, ejgallego/coq-lsp#719)
 - [code] Center the view if cursor goes out of scope in
   `sentenceNext/sentencePrevious` (@ejgallego, ejgallego/coq-lsp#718)
 - Switch Flèche range encoding to protocol native, this means UTF-16
   code points for now (Léo Stefanesco, @ejgallego, ejgallego/coq-lsp#624, fixes ejgallego/coq-lsp#620,
   ejgallego/coq-lsp#621)
 - Give `Goals` panel focus back if it has lost it (in case of
   multiple panels in the second viewColumn of Vscode) whenever
   user navigates proofs (@Alidra @ejgallego, ejgallego/coq-lsp#722, ejgallego/coq-lsp#725)
 - `fcc`: new option `--diags_level` to control whether Coq's notice
   and info messages appear as diagnostics
 - [code] Display the continous/on-request checking mode in the status bar,
   allow to change it by clicking on it (@ejgallego, ejgallego/coq-lsp#721)
 - Add an example of multiple workspaces (@ejgallego, @Blaisorblade,
   ejgallego/coq-lsp#611)
 - Don't show types of un-expanded goals. We should add an option for
   this, but we don't have the cycles (@ejgallego, ejgallego/coq-lsp#730, workarounds
   ejgallego/coq-lsp#525 ejgallego/coq-lsp#652)
 - Support for `.lv / .v.tex` TeX files with embedded Coq code
   (@ejgallego, ejgallego/coq-lsp#727)
 - Don't expand bullet goals at previous levels by default
   (@ejgallego, @Alizter, ejgallego/coq-lsp#731 cc ejgallego/coq-lsp#525)
 - [petanque] Return basic goal information after `run_tac`, so we
   avoid a `goals` round-trip for each tactic (@gbdrt, @ejgallego,
   ejgallego/coq-lsp#733)
 - [coq] Add support for reading glob files metadata (@ejgallego,
   ejgallego/coq-lsp#735)
 - [petanque] Return extra premise information: file name, position,
   raw_text, using the above support for reading .glob files
   (@ejgallego, ejgallego/coq-lsp#735)
 - [code] Display server status using the `LanguageStatusItem`
   facility, for now we display version and checking status
   information (moved from ejgallego/coq-lsp#721), and we also allow to toggle the
   checking mode from there (@ejgallego, ejgallego/coq-lsp#728)
@ejgallego ejgallego mentioned this pull request May 31, 2024
Merged
ejgallego added a commit to ejgallego/opam-repository that referenced this pull request May 31, 2024
@ejgallego
[new release] coq-lsp (0.1.9+8.17)
f7beab6 
CHANGES:

---------------------------------------

 - new option `show_loc_info_on_hover` that will display parsing debug
   information on hover; previous flag was fixed in code, which is way
   less flexible. This also fixes the option being on in 0.1.8 by
   mistake (@ejgallego, ejgallego/coq-lsp#588)
 - hover plugins can now access the full document, this is convenient
   for many use cases (@ejgallego, ejgallego/coq-lsp#591)
 - fix hover position computation on the presence of Utf characters
   (@ejgallego, ejgallego/coq-lsp#597, thanks to Pierre Courtieu for the report and
   example, closes ejgallego/coq-lsp#594)
 - fix activation bug that prevented extension activation for `.mv`
   files, see discussion in the issues about the upstream policy
   (@ejgallego @r3m0t, ejgallego/coq-lsp#598, cc ejgallego/coq-lsp#596, reported by Théo Zimmerman)
 - require VSCode >= 1.82 in package.json . Our VSCode extension uses
   `vscode-languageclient` 9 which imposes this. (@ejgallego, ejgallego/coq-lsp#599,
   thanks to Théo Zimmerman for the report)
 - `proof/goals` request: new `mode` parameter, to specify goals
   after/before sentence display; renamed `pretac` to `command`, as to
   provide official support for speculative execution (@ejgallego, ejgallego/coq-lsp#600)
 - fix some cases where interrupted computations where memoized
   (@ejgallego, ejgallego/coq-lsp#603)
 - [internal] Flèche [Doc.t] API will now absorb errors on document
   update and creation into the document itself. Thus, a document that
   failed to create or update is still valid, but in the right failed
   state. This is a much needed API change for a lot of use cases
   (@ejgallego, ejgallego/coq-lsp#604)
 - support OCaml 5.1.x (@ejgallego, ejgallego/coq-lsp#606)
 - update progress indicator correctly on End Of File (@ejgallego,
   ejgallego/coq-lsp#605, fixes ejgallego/coq-lsp#445)
 - [plugins] New `astdump` plugin to dump AST of files into JSON and
   SEXP (@ejgallego, ejgallego/coq-lsp#607)
 - errors on save where not properly caught (@ejgallego, ejgallego/coq-lsp#608)
 - switch default of `goal_after_tactic` to `true` (@Alizter,
   @ejgallego, cc: ejgallego/coq-lsp#614)
 - error recovery: Recognize `Defined` and `Admitted` in lex recovery
   (@ejgallego, ejgallego/coq-lsp#616)
 - completion: correctly understand UTF-16 code points on completion
   request (Léo Stefanesco, ejgallego/coq-lsp#613, fixes ejgallego/coq-lsp#531)
 - don't trigger the goals window in general markdown buffer
   (@ejgallego, ejgallego/coq-lsp#625, reported by Théo Zimmerman)
 - allow not to postpone full document requests (ejgallego/coq-lsp#626, @ejgallego)
 - new configuration value `check_only_on_request` which will delay
   checking the document until a request has been made (ejgallego/coq-lsp#629, cc: ejgallego/coq-lsp#24,
   @ejgallego)
 - fix typo on package.json configuration section (@ejgallego, ejgallego/coq-lsp#645)
 - be more resilient with invalid _CoqProject files (@ejgallego, ejgallego/coq-lsp#646)
 - support for Coq 8.16 has been abandoned due to lack of dev
   resources (@ejgallego, ejgallego/coq-lsp#649)
 - new option `--no_vo` for `fcc`, which will skip the `.vo` saving
   step. `.vo` saving is now an `fcc` plugins, but for now, it is
   enabled by default (@ejgallego, ejgallego/coq-lsp#650)
 - depend on `memprof-limits` on OCaml 4.x (@ejgallego, ejgallego/coq-lsp#660)
 - bump minimal OCaml version to 4.12 due to `memprof-limits`
   (@ejgallego, ejgallego/coq-lsp#660)
 - monitor all Coq-level calls under an interruption token
   (@ejgallego, ejgallego/coq-lsp#661)
 - interpret require thru our own custom execution env-aware path
   (@bhaktishh, @ejgallego, ejgallego/coq-lsp#642, ejgallego/coq-lsp#643, ejgallego/coq-lsp#644)
 - new `coq-lsp.plugin.goaldump` plugin, as an example on how to dump
   goals from a document (@ejgallego @gbdrt, ejgallego/coq-lsp#619)
 - new trim command (both in the server and in VSCode) to liberate
   space used in the cache (@ejgallego, ejgallego/coq-lsp#662, fixes ejgallego/coq-lsp#367 cc: ejgallego/coq-lsp#253 ejgallego/coq-lsp#236
   ejgallego/coq-lsp#348)
 - fix Coq performance view display (@ejgallego, ejgallego/coq-lsp#663, regression in
   ejgallego/coq-lsp#513)
 - Added new heatmap feature allowing timing data to be seen in the
   editor. Can be enabled with the `Coq LSP: Toggle heatmap`
   command. Can be configured to show memory usage. Colors and
   granularity are configurable. (@Alizter and @ejgallego, ejgallego/coq-lsp#686,
   grants ejgallego/coq-lsp#681).
 - allow more than one input position in `selectionRange` LSP call
   (@ejgallego, ejgallego/coq-lsp#667, fixes ejgallego/coq-lsp#663)
 - new VSCode commands to allow to move one sentence backwards /
   forward, this is particularly useful when combined with lazy
   checking mode (@ejgallego, ejgallego/coq-lsp#671, fixes ejgallego/coq-lsp#263, fixes ejgallego/coq-lsp#580)
 - VSCode commands `coq-lsp.sentenceNext` / `coq-lsp.sentencePrevious`
   are now bound by default to `Alt + N` / `Alt + P` keybindings
   (@ejgallego, ejgallego/coq-lsp#718)
 - change diagnostic `extra` field to `data`, so we now conform to the
   LSP spec, include the data only when the `send_diags_extra_data`
   server-side option is enabled (@ejgallego, ejgallego/coq-lsp#670)
 - include range of full sentence in error diagnostic extra data
   (@ejgallego, ejgallego/coq-lsp#670 , thanks to @driverag22 for the idea, cc: ejgallego/coq-lsp#663).
 - The `coq-lsp.pp_type` VSCode client option now takes effect
   immediately, no more need to restart the server to get different
   goal display formats (@ejgallego, ejgallego/coq-lsp#675)
 - new public VSCode extension API so other extensions can perform
   actions when the user request the goals (@ejgallego, @bhaktishh,
   ejgallego/coq-lsp#672, fixes ejgallego/coq-lsp#538)
 - Support Visual Studio Live Share URIs better (`vsls://`), in
   particular don't try to display goals if the URI is VSLS one
   (@ejgallego, ejgallego/coq-lsp#676)
 - New `InjectRequire` plugin API for plugins to be able to instrument
   the default import list of files (@ejgallego @corwin-of-amber,
   ejgallego/coq-lsp#679)
 - Add `--max_errors=n` option to `fcc`, this way users can set
   `--max_errors=0` to imitate `coqc` behavior (@ejgallego, ejgallego/coq-lsp#680)
 - Fix `fcc` exit status when checking terminates with fatal errors
   (@ejgallego, @Alizter, ejgallego/coq-lsp#680)
 - Fix install to OPAM switches from `main` branch (@ejgallego, ejgallego/coq-lsp#683,
   fixes ejgallego/coq-lsp#682, cc ejgallego/coq-lsp#479 ejgallego/coq-lsp#488, thanks to @HazardousPeach for the report)
 - New `--int_backend={Coq,Mp}` command line parameter to select the
   interruption method for Coq (@ejgallego, ejgallego/coq-lsp#684)
 - Update `package-lock.json` for latest bugfixes (@ejgallego, ejgallego/coq-lsp#687)
 - Update Nix flake enviroment (@Alizter, ejgallego/coq-lsp#684 ejgallego/coq-lsp#688)
 - Update `prettier` (@Alizter @ejgallego, ejgallego/coq-lsp#684 ejgallego/coq-lsp#688)
 - Store original performance data in the cache, so we now display the
   original timing and memory data even for cached commands (@ejgallego, ejgallego/coq-lsp#693)
 - Fix type errors in the Performance Data Notifications (@ejgallego,
   @Alizter, ejgallego/coq-lsp#689, ejgallego/coq-lsp#693)
 - Send performance performance data for the full document
   (@ejgallego, @Alizter, ejgallego/coq-lsp#689, ejgallego/coq-lsp#693)
 - Better types `coq/perfData` call (@ejgallego @Alizter, ejgallego/coq-lsp#689)
 - New server option to enable / disable `coq/perfData` (@ejgallego, ejgallego/coq-lsp#689)
 - New client option to enable / disable `coq/perfData` (@ejgallego, ejgallego/coq-lsp#717)
 - The `coq-lsp.document` VSCode command will now display the returned
   JSON data in a new editor (@ejgallego, ejgallego/coq-lsp#701)
 - Update server settings on the fly when tweaking them in VSCode.
   Implement `workspace/didChangeConfiguration` (@ejgallego, ejgallego/coq-lsp#702)
 - [Coq API] Add functions to retrieve list of declarations done in
   .vo files (@ejallego, @eytans, ejgallego/coq-lsp#704)
 - New `petanque` API to interact directly with Coq's proof
   engine. (@ejgallego, @gbdrt, Laetitia Teodorescu ejgallego/coq-lsp#703, thanks to
   Alex Sanchez-Stern for many insightful feedback and testing)
 - New `petanque` JSON-RPC `pet.exe`, which can be used à la SerAPI
   to perform proof search and more (@ejgallego, @gbdrt, ejgallego/coq-lsp#705)
 - New `pet-server.exe` TCP server for keep-alive sessions (@gbdrt,
   ejgallego/coq-lsp#697)
 - Always dispose UI elements. This should improve some strange
   behaviors on extension restart (@ejgallego, ejgallego/coq-lsp#708)
 - [code] Added new heatmap feature allowing timing data to be seen in
   the editor. Can be enabled with the `Coq LSP: Toggle heatmap`
   comamnd. Can be configured to show memory usage. Colors and
   granularity are configurable. (@Alizter and @ejgallego, ejgallego/coq-lsp#686,
   grants ejgallego/coq-lsp#681).
 - [server] Support Coq meta-commands (Reset, Reset Initial, Back)
   They are actually pretty useful to hint the incremental engine to
   ignore changes in some part of the document (@ejgallego, ejgallego/coq-lsp#709)
 - JSON-RPC library now supports all kind of incoming messages
   (@ejgallego, ejgallego/coq-lsp#713)
 - [code/server] New `coq/viewRange` notification, from client to
   server, than hints the scheduler for the visible area of the
   document; combined with the new lazy checking mode, this provides
   checking on scroll, a feature inspired from Isabelle IDE
   (@ejgallego, ejgallego/coq-lsp#717)
 - [code] Have VSCode wait for full LSP client shutdown on server
   restart. This fixes some bugs on extension restart (finally!)
   (@ejgallego, ejgallego/coq-lsp#719)
 - [code] Center the view if cursor goes out of scope in
   `sentenceNext/sentencePrevious` (@ejgallego, ejgallego/coq-lsp#718)
 - Switch Flèche range encoding to protocol native, this means UTF-16
   code points for now (Léo Stefanesco, @ejgallego, ejgallego/coq-lsp#624, fixes ejgallego/coq-lsp#620,
   ejgallego/coq-lsp#621)
 - Give `Goals` panel focus back if it has lost it (in case of
   multiple panels in the second viewColumn of Vscode) whenever
   user navigates proofs (@Alidra @ejgallego, ejgallego/coq-lsp#722, ejgallego/coq-lsp#725)
 - `fcc`: new option `--diags_level` to control whether Coq's notice
   and info messages appear as diagnostics
 - [code] Display the continous/on-request checking mode in the status bar,
   allow to change it by clicking on it (@ejgallego, ejgallego/coq-lsp#721)
 - Add an example of multiple workspaces (@ejgallego, @Blaisorblade,
   ejgallego/coq-lsp#611)
 - Don't show types of un-expanded goals. We should add an option for
   this, but we don't have the cycles (@ejgallego, ejgallego/coq-lsp#730, workarounds
   ejgallego/coq-lsp#525 ejgallego/coq-lsp#652)
 - Support for `.lv / .v.tex` TeX files with embedded Coq code
   (@ejgallego, ejgallego/coq-lsp#727)
 - Don't expand bullet goals at previous levels by default
   (@ejgallego, @Alizter, ejgallego/coq-lsp#731 cc ejgallego/coq-lsp#525)
 - [petanque] Return basic goal information after `run_tac`, so we
   avoid a `goals` round-trip for each tactic (@gbdrt, @ejgallego,
   ejgallego/coq-lsp#733)
 - [coq] Add support for reading glob files metadata (@ejgallego,
   ejgallego/coq-lsp#735)
 - [petanque] Return extra premise information: file name, position,
   raw_text, using the above support for reading .glob files
   (@ejgallego, ejgallego/coq-lsp#735)
 - [code] Display server status using the `LanguageStatusItem`
   facility, for now we display version and checking status
   information (moved from ejgallego/coq-lsp#721), and we also allow to toggle the
   checking mode from there (@ejgallego, ejgallego/coq-lsp#728)
@ejgallego ejgallego mentioned this pull request May 31, 2024
Merged
ejgallego added a commit to ejgallego/opam-repository that referenced this pull request May 31, 2024
@ejgallego
[new release] coq-lsp (0.1.9+8.17)
ac0ffb0 
CHANGES:

---------------------------------------

 - new option `show_loc_info_on_hover` that will display parsing debug
   information on hover; previous flag was fixed in code, which is way
   less flexible. This also fixes the option being on in 0.1.8 by
   mistake (@ejgallego, ejgallego/coq-lsp#588)
 - hover plugins can now access the full document, this is convenient
   for many use cases (@ejgallego, ejgallego/coq-lsp#591)
 - fix hover position computation on the presence of Utf characters
   (@ejgallego, ejgallego/coq-lsp#597, thanks to Pierre Courtieu for the report and
   example, closes ejgallego/coq-lsp#594)
 - fix activation bug that prevented extension activation for `.mv`
   files, see discussion in the issues about the upstream policy
   (@ejgallego @r3m0t, ejgallego/coq-lsp#598, cc ejgallego/coq-lsp#596, reported by Théo Zimmerman)
 - require VSCode >= 1.82 in package.json . Our VSCode extension uses
   `vscode-languageclient` 9 which imposes this. (@ejgallego, ejgallego/coq-lsp#599,
   thanks to Théo Zimmerman for the report)
 - `proof/goals` request: new `mode` parameter, to specify goals
   after/before sentence display; renamed `pretac` to `command`, as to
   provide official support for speculative execution (@ejgallego, ejgallego/coq-lsp#600)
 - fix some cases where interrupted computations where memoized
   (@ejgallego, ejgallego/coq-lsp#603)
 - [internal] Flèche [Doc.t] API will now absorb errors on document
   update and creation into the document itself. Thus, a document that
   failed to create or update is still valid, but in the right failed
   state. This is a much needed API change for a lot of use cases
   (@ejgallego, ejgallego/coq-lsp#604)
 - support OCaml 5.1.x (@ejgallego, ejgallego/coq-lsp#606)
 - update progress indicator correctly on End Of File (@ejgallego,
   ejgallego/coq-lsp#605, fixes ejgallego/coq-lsp#445)
 - [plugins] New `astdump` plugin to dump AST of files into JSON and
   SEXP (@ejgallego, ejgallego/coq-lsp#607)
 - errors on save where not properly caught (@ejgallego, ejgallego/coq-lsp#608)
 - switch default of `goal_after_tactic` to `true` (@Alizter,
   @ejgallego, cc: ejgallego/coq-lsp#614)
 - error recovery: Recognize `Defined` and `Admitted` in lex recovery
   (@ejgallego, ejgallego/coq-lsp#616)
 - completion: correctly understand UTF-16 code points on completion
   request (Léo Stefanesco, ejgallego/coq-lsp#613, fixes ejgallego/coq-lsp#531)
 - don't trigger the goals window in general markdown buffer
   (@ejgallego, ejgallego/coq-lsp#625, reported by Théo Zimmerman)
 - allow not to postpone full document requests (ejgallego/coq-lsp#626, @ejgallego)
 - new configuration value `check_only_on_request` which will delay
   checking the document until a request has been made (ejgallego/coq-lsp#629, cc: ejgallego/coq-lsp#24,
   @ejgallego)
 - fix typo on package.json configuration section (@ejgallego, ejgallego/coq-lsp#645)
 - be more resilient with invalid _CoqProject files (@ejgallego, ejgallego/coq-lsp#646)
 - support for Coq 8.16 has been abandoned due to lack of dev
   resources (@ejgallego, ejgallego/coq-lsp#649)
 - new option `--no_vo` for `fcc`, which will skip the `.vo` saving
   step. `.vo` saving is now an `fcc` plugins, but for now, it is
   enabled by default (@ejgallego, ejgallego/coq-lsp#650)
 - depend on `memprof-limits` on OCaml 4.x (@ejgallego, ejgallego/coq-lsp#660)
 - bump minimal OCaml version to 4.12 due to `memprof-limits`
   (@ejgallego, ejgallego/coq-lsp#660)
 - monitor all Coq-level calls under an interruption token
   (@ejgallego, ejgallego/coq-lsp#661)
 - interpret require thru our own custom execution env-aware path
   (@bhaktishh, @ejgallego, ejgallego/coq-lsp#642, ejgallego/coq-lsp#643, ejgallego/coq-lsp#644)
 - new `coq-lsp.plugin.goaldump` plugin, as an example on how to dump
   goals from a document (@ejgallego @gbdrt, ejgallego/coq-lsp#619)
 - new trim command (both in the server and in VSCode) to liberate
   space used in the cache (@ejgallego, ejgallego/coq-lsp#662, fixes ejgallego/coq-lsp#367 cc: ejgallego/coq-lsp#253 ejgallego/coq-lsp#236
   ejgallego/coq-lsp#348)
 - fix Coq performance view display (@ejgallego, ejgallego/coq-lsp#663, regression in
   ejgallego/coq-lsp#513)
 - Added new heatmap feature allowing timing data to be seen in the
   editor. Can be enabled with the `Coq LSP: Toggle heatmap`
   command. Can be configured to show memory usage. Colors and
   granularity are configurable. (@Alizter and @ejgallego, ejgallego/coq-lsp#686,
   grants ejgallego/coq-lsp#681).
 - allow more than one input position in `selectionRange` LSP call
   (@ejgallego, ejgallego/coq-lsp#667, fixes ejgallego/coq-lsp#663)
 - new VSCode commands to allow to move one sentence backwards /
   forward, this is particularly useful when combined with lazy
   checking mode (@ejgallego, ejgallego/coq-lsp#671, fixes ejgallego/coq-lsp#263, fixes ejgallego/coq-lsp#580)
 - VSCode commands `coq-lsp.sentenceNext` / `coq-lsp.sentencePrevious`
   are now bound by default to `Alt + N` / `Alt + P` keybindings
   (@ejgallego, ejgallego/coq-lsp#718)
 - change diagnostic `extra` field to `data`, so we now conform to the
   LSP spec, include the data only when the `send_diags_extra_data`
   server-side option is enabled (@ejgallego, ejgallego/coq-lsp#670)
 - include range of full sentence in error diagnostic extra data
   (@ejgallego, ejgallego/coq-lsp#670 , thanks to @driverag22 for the idea, cc: ejgallego/coq-lsp#663).
 - The `coq-lsp.pp_type` VSCode client option now takes effect
   immediately, no more need to restart the server to get different
   goal display formats (@ejgallego, ejgallego/coq-lsp#675)
 - new public VSCode extension API so other extensions can perform
   actions when the user request the goals (@ejgallego, @bhaktishh,
   ejgallego/coq-lsp#672, fixes ejgallego/coq-lsp#538)
 - Support Visual Studio Live Share URIs better (`vsls://`), in
   particular don't try to display goals if the URI is VSLS one
   (@ejgallego, ejgallego/coq-lsp#676)
 - New `InjectRequire` plugin API for plugins to be able to instrument
   the default import list of files (@ejgallego @corwin-of-amber,
   ejgallego/coq-lsp#679)
 - Add `--max_errors=n` option to `fcc`, this way users can set
   `--max_errors=0` to imitate `coqc` behavior (@ejgallego, ejgallego/coq-lsp#680)
 - Fix `fcc` exit status when checking terminates with fatal errors
   (@ejgallego, @Alizter, ejgallego/coq-lsp#680)
 - Fix install to OPAM switches from `main` branch (@ejgallego, ejgallego/coq-lsp#683,
   fixes ejgallego/coq-lsp#682, cc ejgallego/coq-lsp#479 ejgallego/coq-lsp#488, thanks to @HazardousPeach for the report)
 - New `--int_backend={Coq,Mp}` command line parameter to select the
   interruption method for Coq (@ejgallego, ejgallego/coq-lsp#684)
 - Update `package-lock.json` for latest bugfixes (@ejgallego, ejgallego/coq-lsp#687)
 - Update Nix flake enviroment (@Alizter, ejgallego/coq-lsp#684 ejgallego/coq-lsp#688)
 - Update `prettier` (@Alizter @ejgallego, ejgallego/coq-lsp#684 ejgallego/coq-lsp#688)
 - Store original performance data in the cache, so we now display the
   original timing and memory data even for cached commands (@ejgallego, ejgallego/coq-lsp#693)
 - Fix type errors in the Performance Data Notifications (@ejgallego,
   @Alizter, ejgallego/coq-lsp#689, ejgallego/coq-lsp#693)
 - Send performance performance data for the full document
   (@ejgallego, @Alizter, ejgallego/coq-lsp#689, ejgallego/coq-lsp#693)
 - Better types `coq/perfData` call (@ejgallego @Alizter, ejgallego/coq-lsp#689)
 - New server option to enable / disable `coq/perfData` (@ejgallego, ejgallego/coq-lsp#689)
 - New client option to enable / disable `coq/perfData` (@ejgallego, ejgallego/coq-lsp#717)
 - The `coq-lsp.document` VSCode command will now display the returned
   JSON data in a new editor (@ejgallego, ejgallego/coq-lsp#701)
 - Update server settings on the fly when tweaking them in VSCode.
   Implement `workspace/didChangeConfiguration` (@ejgallego, ejgallego/coq-lsp#702)
 - [Coq API] Add functions to retrieve list of declarations done in
   .vo files (@ejallego, @eytans, ejgallego/coq-lsp#704)
 - New `petanque` API to interact directly with Coq's proof
   engine. (@ejgallego, @gbdrt, Laetitia Teodorescu ejgallego/coq-lsp#703, thanks to
   Alex Sanchez-Stern for many insightful feedback and testing)
 - New `petanque` JSON-RPC `pet.exe`, which can be used à la SerAPI
   to perform proof search and more (@ejgallego, @gbdrt, ejgallego/coq-lsp#705)
 - New `pet-server.exe` TCP server for keep-alive sessions (@gbdrt,
   ejgallego/coq-lsp#697)
 - Always dispose UI elements. This should improve some strange
   behaviors on extension restart (@ejgallego, ejgallego/coq-lsp#708)
 - [code] Added new heatmap feature allowing timing data to be seen in
   the editor. Can be enabled with the `Coq LSP: Toggle heatmap`
   comamnd. Can be configured to show memory usage. Colors and
   granularity are configurable. (@Alizter and @ejgallego, ejgallego/coq-lsp#686,
   grants ejgallego/coq-lsp#681).
 - [server] Support Coq meta-commands (Reset, Reset Initial, Back)
   They are actually pretty useful to hint the incremental engine to
   ignore changes in some part of the document (@ejgallego, ejgallego/coq-lsp#709)
 - JSON-RPC library now supports all kind of incoming messages
   (@ejgallego, ejgallego/coq-lsp#713)
 - [code/server] New `coq/viewRange` notification, from client to
   server, than hints the scheduler for the visible area of the
   document; combined with the new lazy checking mode, this provides
   checking on scroll, a feature inspired from Isabelle IDE
   (@ejgallego, ejgallego/coq-lsp#717)
 - [code] Have VSCode wait for full LSP client shutdown on server
   restart. This fixes some bugs on extension restart (finally!)
   (@ejgallego, ejgallego/coq-lsp#719)
 - [code] Center the view if cursor goes out of scope in
   `sentenceNext/sentencePrevious` (@ejgallego, ejgallego/coq-lsp#718)
 - Switch Flèche range encoding to protocol native, this means UTF-16
   code points for now (Léo Stefanesco, @ejgallego, ejgallego/coq-lsp#624, fixes ejgallego/coq-lsp#620,
   ejgallego/coq-lsp#621)
 - Give `Goals` panel focus back if it has lost it (in case of
   multiple panels in the second viewColumn of Vscode) whenever
   user navigates proofs (@Alidra @ejgallego, ejgallego/coq-lsp#722, ejgallego/coq-lsp#725)
 - `fcc`: new option `--diags_level` to control whether Coq's notice
   and info messages appear as diagnostics
 - [code] Display the continous/on-request checking mode in the status bar,
   allow to change it by clicking on it (@ejgallego, ejgallego/coq-lsp#721)
 - Add an example of multiple workspaces (@ejgallego, @Blaisorblade,
   ejgallego/coq-lsp#611)
 - Don't show types of un-expanded goals. We should add an option for
   this, but we don't have the cycles (@ejgallego, ejgallego/coq-lsp#730, workarounds
   ejgallego/coq-lsp#525 ejgallego/coq-lsp#652)
 - Support for `.lv / .v.tex` TeX files with embedded Coq code
   (@ejgallego, ejgallego/coq-lsp#727)
 - Don't expand bullet goals at previous levels by default
   (@ejgallego, @Alizter, ejgallego/coq-lsp#731 cc ejgallego/coq-lsp#525)
 - [petanque] Return basic goal information after `run_tac`, so we
   avoid a `goals` round-trip for each tactic (@gbdrt, @ejgallego,
   ejgallego/coq-lsp#733)
 - [coq] Add support for reading glob files metadata (@ejgallego,
   ejgallego/coq-lsp#735)
 - [petanque] Return extra premise information: file name, position,
   raw_text, using the above support for reading .glob files
   (@ejgallego, ejgallego/coq-lsp#735)
 - [code] Display server status using the `LanguageStatusItem`
   facility, for now we display version and checking status
   information (moved from ejgallego/coq-lsp#721), and we also allow to toggle the
   checking mode from there (@ejgallego, ejgallego/coq-lsp#728)
ejgallego added a commit to ejgallego/opam-repository that referenced this pull request May 31, 2024
@ejgallego
[new release] coq-lsp (0.1.9+8.18)
aec15a8 
CHANGES:

---------------------------------------

 - new option `show_loc_info_on_hover` that will display parsing debug
   information on hover; previous flag was fixed in code, which is way
   less flexible. This also fixes the option being on in 0.1.8 by
   mistake (@ejgallego, ejgallego/coq-lsp#588)
 - hover plugins can now access the full document, this is convenient
   for many use cases (@ejgallego, ejgallego/coq-lsp#591)
 - fix hover position computation on the presence of Utf characters
   (@ejgallego, ejgallego/coq-lsp#597, thanks to Pierre Courtieu for the report and
   example, closes ejgallego/coq-lsp#594)
 - fix activation bug that prevented extension activation for `.mv`
   files, see discussion in the issues about the upstream policy
   (@ejgallego @r3m0t, ejgallego/coq-lsp#598, cc ejgallego/coq-lsp#596, reported by Théo Zimmerman)
 - require VSCode >= 1.82 in package.json . Our VSCode extension uses
   `vscode-languageclient` 9 which imposes this. (@ejgallego, ejgallego/coq-lsp#599,
   thanks to Théo Zimmerman for the report)
 - `proof/goals` request: new `mode` parameter, to specify goals
   after/before sentence display; renamed `pretac` to `command`, as to
   provide official support for speculative execution (@ejgallego, ejgallego/coq-lsp#600)
 - fix some cases where interrupted computations where memoized
   (@ejgallego, ejgallego/coq-lsp#603)
 - [internal] Flèche [Doc.t] API will now absorb errors on document
   update and creation into the document itself. Thus, a document that
   failed to create or update is still valid, but in the right failed
   state. This is a much needed API change for a lot of use cases
   (@ejgallego, ejgallego/coq-lsp#604)
 - support OCaml 5.1.x (@ejgallego, ejgallego/coq-lsp#606)
 - update progress indicator correctly on End Of File (@ejgallego,
   ejgallego/coq-lsp#605, fixes ejgallego/coq-lsp#445)
 - [plugins] New `astdump` plugin to dump AST of files into JSON and
   SEXP (@ejgallego, ejgallego/coq-lsp#607)
 - errors on save where not properly caught (@ejgallego, ejgallego/coq-lsp#608)
 - switch default of `goal_after_tactic` to `true` (@Alizter,
   @ejgallego, cc: ejgallego/coq-lsp#614)
 - error recovery: Recognize `Defined` and `Admitted` in lex recovery
   (@ejgallego, ejgallego/coq-lsp#616)
 - completion: correctly understand UTF-16 code points on completion
   request (Léo Stefanesco, ejgallego/coq-lsp#613, fixes ejgallego/coq-lsp#531)
 - don't trigger the goals window in general markdown buffer
   (@ejgallego, ejgallego/coq-lsp#625, reported by Théo Zimmerman)
 - allow not to postpone full document requests (ejgallego/coq-lsp#626, @ejgallego)
 - new configuration value `check_only_on_request` which will delay
   checking the document until a request has been made (ejgallego/coq-lsp#629, cc: ejgallego/coq-lsp#24,
   @ejgallego)
 - fix typo on package.json configuration section (@ejgallego, ejgallego/coq-lsp#645)
 - be more resilient with invalid _CoqProject files (@ejgallego, ejgallego/coq-lsp#646)
 - support for Coq 8.16 has been abandoned due to lack of dev
   resources (@ejgallego, ejgallego/coq-lsp#649)
 - new option `--no_vo` for `fcc`, which will skip the `.vo` saving
   step. `.vo` saving is now an `fcc` plugins, but for now, it is
   enabled by default (@ejgallego, ejgallego/coq-lsp#650)
 - depend on `memprof-limits` on OCaml 4.x (@ejgallego, ejgallego/coq-lsp#660)
 - bump minimal OCaml version to 4.12 due to `memprof-limits`
   (@ejgallego, ejgallego/coq-lsp#660)
 - monitor all Coq-level calls under an interruption token
   (@ejgallego, ejgallego/coq-lsp#661)
 - interpret require thru our own custom execution env-aware path
   (@bhaktishh, @ejgallego, ejgallego/coq-lsp#642, ejgallego/coq-lsp#643, ejgallego/coq-lsp#644)
 - new `coq-lsp.plugin.goaldump` plugin, as an example on how to dump
   goals from a document (@ejgallego @gbdrt, ejgallego/coq-lsp#619)
 - new trim command (both in the server and in VSCode) to liberate
   space used in the cache (@ejgallego, ejgallego/coq-lsp#662, fixes ejgallego/coq-lsp#367 cc: ejgallego/coq-lsp#253 ejgallego/coq-lsp#236
   ejgallego/coq-lsp#348)
 - fix Coq performance view display (@ejgallego, ejgallego/coq-lsp#663, regression in
   ejgallego/coq-lsp#513)
 - Added new heatmap feature allowing timing data to be seen in the
   editor. Can be enabled with the `Coq LSP: Toggle heatmap`
   command. Can be configured to show memory usage. Colors and
   granularity are configurable. (@Alizter and @ejgallego, ejgallego/coq-lsp#686,
   grants ejgallego/coq-lsp#681).
 - allow more than one input position in `selectionRange` LSP call
   (@ejgallego, ejgallego/coq-lsp#667, fixes ejgallego/coq-lsp#663)
 - new VSCode commands to allow to move one sentence backwards /
   forward, this is particularly useful when combined with lazy
   checking mode (@ejgallego, ejgallego/coq-lsp#671, fixes ejgallego/coq-lsp#263, fixes ejgallego/coq-lsp#580)
 - VSCode commands `coq-lsp.sentenceNext` / `coq-lsp.sentencePrevious`
   are now bound by default to `Alt + N` / `Alt + P` keybindings
   (@ejgallego, ejgallego/coq-lsp#718)
 - change diagnostic `extra` field to `data`, so we now conform to the
   LSP spec, include the data only when the `send_diags_extra_data`
   server-side option is enabled (@ejgallego, ejgallego/coq-lsp#670)
 - include range of full sentence in error diagnostic extra data
   (@ejgallego, ejgallego/coq-lsp#670 , thanks to @driverag22 for the idea, cc: ejgallego/coq-lsp#663).
 - The `coq-lsp.pp_type` VSCode client option now takes effect
   immediately, no more need to restart the server to get different
   goal display formats (@ejgallego, ejgallego/coq-lsp#675)
 - new public VSCode extension API so other extensions can perform
   actions when the user request the goals (@ejgallego, @bhaktishh,
   ejgallego/coq-lsp#672, fixes ejgallego/coq-lsp#538)
 - Support Visual Studio Live Share URIs better (`vsls://`), in
   particular don't try to display goals if the URI is VSLS one
   (@ejgallego, ejgallego/coq-lsp#676)
 - New `InjectRequire` plugin API for plugins to be able to instrument
   the default import list of files (@ejgallego @corwin-of-amber,
   ejgallego/coq-lsp#679)
 - Add `--max_errors=n` option to `fcc`, this way users can set
   `--max_errors=0` to imitate `coqc` behavior (@ejgallego, ejgallego/coq-lsp#680)
 - Fix `fcc` exit status when checking terminates with fatal errors
   (@ejgallego, @Alizter, ejgallego/coq-lsp#680)
 - Fix install to OPAM switches from `main` branch (@ejgallego, ejgallego/coq-lsp#683,
   fixes ejgallego/coq-lsp#682, cc ejgallego/coq-lsp#479 ejgallego/coq-lsp#488, thanks to @HazardousPeach for the report)
 - New `--int_backend={Coq,Mp}` command line parameter to select the
   interruption method for Coq (@ejgallego, ejgallego/coq-lsp#684)
 - Update `package-lock.json` for latest bugfixes (@ejgallego, ejgallego/coq-lsp#687)
 - Update Nix flake enviroment (@Alizter, ejgallego/coq-lsp#684 ejgallego/coq-lsp#688)
 - Update `prettier` (@Alizter @ejgallego, ejgallego/coq-lsp#684 ejgallego/coq-lsp#688)
 - Store original performance data in the cache, so we now display the
   original timing and memory data even for cached commands (@ejgallego, ejgallego/coq-lsp#693)
 - Fix type errors in the Performance Data Notifications (@ejgallego,
   @Alizter, ejgallego/coq-lsp#689, ejgallego/coq-lsp#693)
 - Send performance performance data for the full document
   (@ejgallego, @Alizter, ejgallego/coq-lsp#689, ejgallego/coq-lsp#693)
 - Better types `coq/perfData` call (@ejgallego @Alizter, ejgallego/coq-lsp#689)
 - New server option to enable / disable `coq/perfData` (@ejgallego, ejgallego/coq-lsp#689)
 - New client option to enable / disable `coq/perfData` (@ejgallego, ejgallego/coq-lsp#717)
 - The `coq-lsp.document` VSCode command will now display the returned
   JSON data in a new editor (@ejgallego, ejgallego/coq-lsp#701)
 - Update server settings on the fly when tweaking them in VSCode.
   Implement `workspace/didChangeConfiguration` (@ejgallego, ejgallego/coq-lsp#702)
 - [Coq API] Add functions to retrieve list of declarations done in
   .vo files (@ejallego, @eytans, ejgallego/coq-lsp#704)
 - New `petanque` API to interact directly with Coq's proof
   engine. (@ejgallego, @gbdrt, Laetitia Teodorescu ejgallego/coq-lsp#703, thanks to
   Alex Sanchez-Stern for many insightful feedback and testing)
 - New `petanque` JSON-RPC `pet.exe`, which can be used à la SerAPI
   to perform proof search and more (@ejgallego, @gbdrt, ejgallego/coq-lsp#705)
 - New `pet-server.exe` TCP server for keep-alive sessions (@gbdrt,
   ejgallego/coq-lsp#697)
 - Always dispose UI elements. This should improve some strange
   behaviors on extension restart (@ejgallego, ejgallego/coq-lsp#708)
 - [code] Added new heatmap feature allowing timing data to be seen in
   the editor. Can be enabled with the `Coq LSP: Toggle heatmap`
   comamnd. Can be configured to show memory usage. Colors and
   granularity are configurable. (@Alizter and @ejgallego, ejgallego/coq-lsp#686,
   grants ejgallego/coq-lsp#681).
 - [server] Support Coq meta-commands (Reset, Reset Initial, Back)
   They are actually pretty useful to hint the incremental engine to
   ignore changes in some part of the document (@ejgallego, ejgallego/coq-lsp#709)
 - JSON-RPC library now supports all kind of incoming messages
   (@ejgallego, ejgallego/coq-lsp#713)
 - [code/server] New `coq/viewRange` notification, from client to
   server, than hints the scheduler for the visible area of the
   document; combined with the new lazy checking mode, this provides
   checking on scroll, a feature inspired from Isabelle IDE
   (@ejgallego, ejgallego/coq-lsp#717)
 - [code] Have VSCode wait for full LSP client shutdown on server
   restart. This fixes some bugs on extension restart (finally!)
   (@ejgallego, ejgallego/coq-lsp#719)
 - [code] Center the view if cursor goes out of scope in
   `sentenceNext/sentencePrevious` (@ejgallego, ejgallego/coq-lsp#718)
 - Switch Flèche range encoding to protocol native, this means UTF-16
   code points for now (Léo Stefanesco, @ejgallego, ejgallego/coq-lsp#624, fixes ejgallego/coq-lsp#620,
   ejgallego/coq-lsp#621)
 - Give `Goals` panel focus back if it has lost it (in case of
   multiple panels in the second viewColumn of Vscode) whenever
   user navigates proofs (@Alidra @ejgallego, ejgallego/coq-lsp#722, ejgallego/coq-lsp#725)
 - `fcc`: new option `--diags_level` to control whether Coq's notice
   and info messages appear as diagnostics
 - [code] Display the continous/on-request checking mode in the status bar,
   allow to change it by clicking on it (@ejgallego, ejgallego/coq-lsp#721)
 - Add an example of multiple workspaces (@ejgallego, @Blaisorblade,
   ejgallego/coq-lsp#611)
 - Don't show types of un-expanded goals. We should add an option for
   this, but we don't have the cycles (@ejgallego, ejgallego/coq-lsp#730, workarounds
   ejgallego/coq-lsp#525 ejgallego/coq-lsp#652)
 - Support for `.lv / .v.tex` TeX files with embedded Coq code
   (@ejgallego, ejgallego/coq-lsp#727)
 - Don't expand bullet goals at previous levels by default
   (@ejgallego, @Alizter, ejgallego/coq-lsp#731 cc ejgallego/coq-lsp#525)
 - [petanque] Return basic goal information after `run_tac`, so we
   avoid a `goals` round-trip for each tactic (@gbdrt, @ejgallego,
   ejgallego/coq-lsp#733)
 - [coq] Add support for reading glob files metadata (@ejgallego,
   ejgallego/coq-lsp#735)
 - [petanque] Return extra premise information: file name, position,
   raw_text, using the above support for reading .glob files
   (@ejgallego, ejgallego/coq-lsp#735)
 - [code] Display server status using the `LanguageStatusItem`
   facility, for now we display version and checking status
   information (moved from ejgallego/coq-lsp#721), and we also allow to toggle the
   checking mode from there (@ejgallego, ejgallego/coq-lsp#728)
ejgallego added a commit to ejgallego/opam-repository that referenced this pull request May 31, 2024
@ejgallego
[new release] coq-lsp (0.1.9+8.19)
140cf0a 
CHANGES:

---------------------------------------

 - new option `show_loc_info_on_hover` that will display parsing debug
   information on hover; previous flag was fixed in code, which is way
   less flexible. This also fixes the option being on in 0.1.8 by
   mistake (@ejgallego, ejgallego/coq-lsp#588)
 - hover plugins can now access the full document, this is convenient
   for many use cases (@ejgallego, ejgallego/coq-lsp#591)
 - fix hover position computation on the presence of Utf characters
   (@ejgallego, ejgallego/coq-lsp#597, thanks to Pierre Courtieu for the report and
   example, closes ejgallego/coq-lsp#594)
 - fix activation bug that prevented extension activation for `.mv`
   files, see discussion in the issues about the upstream policy
   (@ejgallego @r3m0t, ejgallego/coq-lsp#598, cc ejgallego/coq-lsp#596, reported by Théo Zimmerman)
 - require VSCode >= 1.82 in package.json . Our VSCode extension uses
   `vscode-languageclient` 9 which imposes this. (@ejgallego, ejgallego/coq-lsp#599,
   thanks to Théo Zimmerman for the report)
 - `proof/goals` request: new `mode` parameter, to specify goals
   after/before sentence display; renamed `pretac` to `command`, as to
   provide official support for speculative execution (@ejgallego, ejgallego/coq-lsp#600)
 - fix some cases where interrupted computations where memoized
   (@ejgallego, ejgallego/coq-lsp#603)
 - [internal] Flèche [Doc.t] API will now absorb errors on document
   update and creation into the document itself. Thus, a document that
   failed to create or update is still valid, but in the right failed
   state. This is a much needed API change for a lot of use cases
   (@ejgallego, ejgallego/coq-lsp#604)
 - support OCaml 5.1.x (@ejgallego, ejgallego/coq-lsp#606)
 - update progress indicator correctly on End Of File (@ejgallego,
   ejgallego/coq-lsp#605, fixes ejgallego/coq-lsp#445)
 - [plugins] New `astdump` plugin to dump AST of files into JSON and
   SEXP (@ejgallego, ejgallego/coq-lsp#607)
 - errors on save where not properly caught (@ejgallego, ejgallego/coq-lsp#608)
 - switch default of `goal_after_tactic` to `true` (@Alizter,
   @ejgallego, cc: ejgallego/coq-lsp#614)
 - error recovery: Recognize `Defined` and `Admitted` in lex recovery
   (@ejgallego, ejgallego/coq-lsp#616)
 - completion: correctly understand UTF-16 code points on completion
   request (Léo Stefanesco, ejgallego/coq-lsp#613, fixes ejgallego/coq-lsp#531)
 - don't trigger the goals window in general markdown buffer
   (@ejgallego, ejgallego/coq-lsp#625, reported by Théo Zimmerman)
 - allow not to postpone full document requests (ejgallego/coq-lsp#626, @ejgallego)
 - new configuration value `check_only_on_request` which will delay
   checking the document until a request has been made (ejgallego/coq-lsp#629, cc: ejgallego/coq-lsp#24,
   @ejgallego)
 - fix typo on package.json configuration section (@ejgallego, ejgallego/coq-lsp#645)
 - be more resilient with invalid _CoqProject files (@ejgallego, ejgallego/coq-lsp#646)
 - support for Coq 8.16 has been abandoned due to lack of dev
   resources (@ejgallego, ejgallego/coq-lsp#649)
 - new option `--no_vo` for `fcc`, which will skip the `.vo` saving
   step. `.vo` saving is now an `fcc` plugins, but for now, it is
   enabled by default (@ejgallego, ejgallego/coq-lsp#650)
 - depend on `memprof-limits` on OCaml 4.x (@ejgallego, ejgallego/coq-lsp#660)
 - bump minimal OCaml version to 4.12 due to `memprof-limits`
   (@ejgallego, ejgallego/coq-lsp#660)
 - monitor all Coq-level calls under an interruption token
   (@ejgallego, ejgallego/coq-lsp#661)
 - interpret require thru our own custom execution env-aware path
   (@bhaktishh, @ejgallego, ejgallego/coq-lsp#642, ejgallego/coq-lsp#643, ejgallego/coq-lsp#644)
 - new `coq-lsp.plugin.goaldump` plugin, as an example on how to dump
   goals from a document (@ejgallego @gbdrt, ejgallego/coq-lsp#619)
 - new trim command (both in the server and in VSCode) to liberate
   space used in the cache (@ejgallego, ejgallego/coq-lsp#662, fixes ejgallego/coq-lsp#367 cc: ejgallego/coq-lsp#253 ejgallego/coq-lsp#236
   ejgallego/coq-lsp#348)
 - fix Coq performance view display (@ejgallego, ejgallego/coq-lsp#663, regression in
   ejgallego/coq-lsp#513)
 - Added new heatmap feature allowing timing data to be seen in the
   editor. Can be enabled with the `Coq LSP: Toggle heatmap`
   command. Can be configured to show memory usage. Colors and
   granularity are configurable. (@Alizter and @ejgallego, ejgallego/coq-lsp#686,
   grants ejgallego/coq-lsp#681).
 - allow more than one input position in `selectionRange` LSP call
   (@ejgallego, ejgallego/coq-lsp#667, fixes ejgallego/coq-lsp#663)
 - new VSCode commands to allow to move one sentence backwards /
   forward, this is particularly useful when combined with lazy
   checking mode (@ejgallego, ejgallego/coq-lsp#671, fixes ejgallego/coq-lsp#263, fixes ejgallego/coq-lsp#580)
 - VSCode commands `coq-lsp.sentenceNext` / `coq-lsp.sentencePrevious`
   are now bound by default to `Alt + N` / `Alt + P` keybindings
   (@ejgallego, ejgallego/coq-lsp#718)
 - change diagnostic `extra` field to `data`, so we now conform to the
   LSP spec, include the data only when the `send_diags_extra_data`
   server-side option is enabled (@ejgallego, ejgallego/coq-lsp#670)
 - include range of full sentence in error diagnostic extra data
   (@ejgallego, ejgallego/coq-lsp#670 , thanks to @driverag22 for the idea, cc: ejgallego/coq-lsp#663).
 - The `coq-lsp.pp_type` VSCode client option now takes effect
   immediately, no more need to restart the server to get different
   goal display formats (@ejgallego, ejgallego/coq-lsp#675)
 - new public VSCode extension API so other extensions can perform
   actions when the user request the goals (@ejgallego, @bhaktishh,
   ejgallego/coq-lsp#672, fixes ejgallego/coq-lsp#538)
 - Support Visual Studio Live Share URIs better (`vsls://`), in
   particular don't try to display goals if the URI is VSLS one
   (@ejgallego, ejgallego/coq-lsp#676)
 - New `InjectRequire` plugin API for plugins to be able to instrument
   the default import list of files (@ejgallego @corwin-of-amber,
   ejgallego/coq-lsp#679)
 - Add `--max_errors=n` option to `fcc`, this way users can set
   `--max_errors=0` to imitate `coqc` behavior (@ejgallego, ejgallego/coq-lsp#680)
 - Fix `fcc` exit status when checking terminates with fatal errors
   (@ejgallego, @Alizter, ejgallego/coq-lsp#680)
 - Fix install to OPAM switches from `main` branch (@ejgallego, ejgallego/coq-lsp#683,
   fixes ejgallego/coq-lsp#682, cc ejgallego/coq-lsp#479 ejgallego/coq-lsp#488, thanks to @HazardousPeach for the report)
 - New `--int_backend={Coq,Mp}` command line parameter to select the
   interruption method for Coq (@ejgallego, ejgallego/coq-lsp#684)
 - Update `package-lock.json` for latest bugfixes (@ejgallego, ejgallego/coq-lsp#687)
 - Update Nix flake enviroment (@Alizter, ejgallego/coq-lsp#684 ejgallego/coq-lsp#688)
 - Update `prettier` (@Alizter @ejgallego, ejgallego/coq-lsp#684 ejgallego/coq-lsp#688)
 - Store original performance data in the cache, so we now display the
   original timing and memory data even for cached commands (@ejgallego, ejgallego/coq-lsp#693)
 - Fix type errors in the Performance Data Notifications (@ejgallego,
   @Alizter, ejgallego/coq-lsp#689, ejgallego/coq-lsp#693)
 - Send performance performance data for the full document
   (@ejgallego, @Alizter, ejgallego/coq-lsp#689, ejgallego/coq-lsp#693)
 - Better types `coq/perfData` call (@ejgallego @Alizter, ejgallego/coq-lsp#689)
 - New server option to enable / disable `coq/perfData` (@ejgallego, ejgallego/coq-lsp#689)
 - New client option to enable / disable `coq/perfData` (@ejgallego, ejgallego/coq-lsp#717)
 - The `coq-lsp.document` VSCode command will now display the returned
   JSON data in a new editor (@ejgallego, ejgallego/coq-lsp#701)
 - Update server settings on the fly when tweaking them in VSCode.
   Implement `workspace/didChangeConfiguration` (@ejgallego, ejgallego/coq-lsp#702)
 - [Coq API] Add functions to retrieve list of declarations done in
   .vo files (@ejallego, @eytans, ejgallego/coq-lsp#704)
 - New `petanque` API to interact directly with Coq's proof
   engine. (@ejgallego, @gbdrt, Laetitia Teodorescu ejgallego/coq-lsp#703, thanks to
   Alex Sanchez-Stern for many insightful feedback and testing)
 - New `petanque` JSON-RPC `pet.exe`, which can be used à la SerAPI
   to perform proof search and more (@ejgallego, @gbdrt, ejgallego/coq-lsp#705)
 - New `pet-server.exe` TCP server for keep-alive sessions (@gbdrt,
   ejgallego/coq-lsp#697)
 - Always dispose UI elements. This should improve some strange
   behaviors on extension restart (@ejgallego, ejgallego/coq-lsp#708)
 - [code] Added new heatmap feature allowing timing data to be seen in
   the editor. Can be enabled with the `Coq LSP: Toggle heatmap`
   comamnd. Can be configured to show memory usage. Colors and
   granularity are configurable. (@Alizter and @ejgallego, ejgallego/coq-lsp#686,
   grants ejgallego/coq-lsp#681).
 - [server] Support Coq meta-commands (Reset, Reset Initial, Back)
   They are actually pretty useful to hint the incremental engine to
   ignore changes in some part of the document (@ejgallego, ejgallego/coq-lsp#709)
 - JSON-RPC library now supports all kind of incoming messages
   (@ejgallego, ejgallego/coq-lsp#713)
 - [code/server] New `coq/viewRange` notification, from client to
   server, than hints the scheduler for the visible area of the
   document; combined with the new lazy checking mode, this provides
   checking on scroll, a feature inspired from Isabelle IDE
   (@ejgallego, ejgallego/coq-lsp#717)
 - [code] Have VSCode wait for full LSP client shutdown on server
   restart. This fixes some bugs on extension restart (finally!)
   (@ejgallego, ejgallego/coq-lsp#719)
 - [code] Center the view if cursor goes out of scope in
   `sentenceNext/sentencePrevious` (@ejgallego, ejgallego/coq-lsp#718)
 - Switch Flèche range encoding to protocol native, this means UTF-16
   code points for now (Léo Stefanesco, @ejgallego, ejgallego/coq-lsp#624, fixes ejgallego/coq-lsp#620,
   ejgallego/coq-lsp#621)
 - Give `Goals` panel focus back if it has lost it (in case of
   multiple panels in the second viewColumn of Vscode) whenever
   user navigates proofs (@Alidra @ejgallego, ejgallego/coq-lsp#722, ejgallego/coq-lsp#725)
 - `fcc`: new option `--diags_level` to control whether Coq's notice
   and info messages appear as diagnostics
 - [code] Display the continous/on-request checking mode in the status bar,
   allow to change it by clicking on it (@ejgallego, ejgallego/coq-lsp#721)
 - Add an example of multiple workspaces (@ejgallego, @Blaisorblade,
   ejgallego/coq-lsp#611)
 - Don't show types of un-expanded goals. We should add an option for
   this, but we don't have the cycles (@ejgallego, ejgallego/coq-lsp#730, workarounds
   ejgallego/coq-lsp#525 ejgallego/coq-lsp#652)
 - Support for `.lv / .v.tex` TeX files with embedded Coq code
   (@ejgallego, ejgallego/coq-lsp#727)
 - Don't expand bullet goals at previous levels by default
   (@ejgallego, @Alizter, ejgallego/coq-lsp#731 cc ejgallego/coq-lsp#525)
 - [petanque] Return basic goal information after `run_tac`, so we
   avoid a `goals` round-trip for each tactic (@gbdrt, @ejgallego,
   ejgallego/coq-lsp#733)
 - [coq] Add support for reading glob files metadata (@ejgallego,
   ejgallego/coq-lsp#735)
 - [petanque] Return extra premise information: file name, position,
   raw_text, using the above support for reading .glob files
   (@ejgallego, ejgallego/coq-lsp#735)
 - [code] Display server status using the `LanguageStatusItem`
   facility, for now we display version and checking status
   information (moved from ejgallego/coq-lsp#721), and we also allow to toggle the
   checking mode from there (@ejgallego, ejgallego/coq-lsp#728)
ejgallego added a commit that referenced this pull request Jun 5, 2024
@ejgallego
[code] Fix focus race when a Coq file is in column 2
9a654ee 
Continuation / fix of #722, #725
@ejgallego ejgallego mentioned this pull request Jun 5, 2024
Merged
@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 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)
avsm pushed a commit to avsm/opam-repository that referenced this pull request Sep 5, 2024
@ejgallego @avsm
[new release] coq-lsp (0.1.9+8.17)
a4a48f3 
CHANGES:

---------------------------------------

 - new option `show_loc_info_on_hover` that will display parsing debug
   information on hover; previous flag was fixed in code, which is way
   less flexible. This also fixes the option being on in 0.1.8 by
   mistake (@ejgallego, ejgallego/coq-lsp#588)
 - hover plugins can now access the full document, this is convenient
   for many use cases (@ejgallego, ejgallego/coq-lsp#591)
 - fix hover position computation on the presence of Utf characters
   (@ejgallego, ejgallego/coq-lsp#597, thanks to Pierre Courtieu for the report and
   example, closes ejgallego/coq-lsp#594)
 - fix activation bug that prevented extension activation for `.mv`
   files, see discussion in the issues about the upstream policy
   (@ejgallego @r3m0t, ejgallego/coq-lsp#598, cc ejgallego/coq-lsp#596, reported by Théo Zimmerman)
 - require VSCode >= 1.82 in package.json . Our VSCode extension uses
   `vscode-languageclient` 9 which imposes this. (@ejgallego, ejgallego/coq-lsp#599,
   thanks to Théo Zimmerman for the report)
 - `proof/goals` request: new `mode` parameter, to specify goals
   after/before sentence display; renamed `pretac` to `command`, as to
   provide official support for speculative execution (@ejgallego, ejgallego/coq-lsp#600)
 - fix some cases where interrupted computations where memoized
   (@ejgallego, ejgallego/coq-lsp#603)
 - [internal] Flèche [Doc.t] API will now absorb errors on document
   update and creation into the document itself. Thus, a document that
   failed to create or update is still valid, but in the right failed
   state. This is a much needed API change for a lot of use cases
   (@ejgallego, ejgallego/coq-lsp#604)
 - support OCaml 5.1.x (@ejgallego, ejgallego/coq-lsp#606)
 - update progress indicator correctly on End Of File (@ejgallego,
   ejgallego/coq-lsp#605, fixes ejgallego/coq-lsp#445)
 - [plugins] New `astdump` plugin to dump AST of files into JSON and
   SEXP (@ejgallego, ejgallego/coq-lsp#607)
 - errors on save where not properly caught (@ejgallego, ejgallego/coq-lsp#608)
 - switch default of `goal_after_tactic` to `true` (@Alizter,
   @ejgallego, cc: ejgallego/coq-lsp#614)
 - error recovery: Recognize `Defined` and `Admitted` in lex recovery
   (@ejgallego, ejgallego/coq-lsp#616)
 - completion: correctly understand UTF-16 code points on completion
   request (Léo Stefanesco, ejgallego/coq-lsp#613, fixes ejgallego/coq-lsp#531)
 - don't trigger the goals window in general markdown buffer
   (@ejgallego, ejgallego/coq-lsp#625, reported by Théo Zimmerman)
 - allow not to postpone full document requests (ejgallego/coq-lsp#626, @ejgallego)
 - new configuration value `check_only_on_request` which will delay
   checking the document until a request has been made (ejgallego/coq-lsp#629, cc: ejgallego/coq-lsp#24,
   @ejgallego)
 - fix typo on package.json configuration section (@ejgallego, ejgallego/coq-lsp#645)
 - be more resilient with invalid _CoqProject files (@ejgallego, ejgallego/coq-lsp#646)
 - support for Coq 8.16 has been abandoned due to lack of dev
   resources (@ejgallego, ejgallego/coq-lsp#649)
 - new option `--no_vo` for `fcc`, which will skip the `.vo` saving
   step. `.vo` saving is now an `fcc` plugins, but for now, it is
   enabled by default (@ejgallego, ejgallego/coq-lsp#650)
 - depend on `memprof-limits` on OCaml 4.x (@ejgallego, ejgallego/coq-lsp#660)
 - bump minimal OCaml version to 4.12 due to `memprof-limits`
   (@ejgallego, ejgallego/coq-lsp#660)
 - monitor all Coq-level calls under an interruption token
   (@ejgallego, ejgallego/coq-lsp#661)
 - interpret require thru our own custom execution env-aware path
   (@bhaktishh, @ejgallego, ejgallego/coq-lsp#642, ejgallego/coq-lsp#643, ejgallego/coq-lsp#644)
 - new `coq-lsp.plugin.goaldump` plugin, as an example on how to dump
   goals from a document (@ejgallego @gbdrt, ejgallego/coq-lsp#619)
 - new trim command (both in the server and in VSCode) to liberate
   space used in the cache (@ejgallego, ejgallego/coq-lsp#662, fixes ejgallego/coq-lsp#367 cc: ejgallego/coq-lsp#253 ejgallego/coq-lsp#236
   ejgallego/coq-lsp#348)
 - fix Coq performance view display (@ejgallego, ejgallego/coq-lsp#663, regression in
   ejgallego/coq-lsp#513)
 - Added new heatmap feature allowing timing data to be seen in the
   editor. Can be enabled with the `Coq LSP: Toggle heatmap`
   command. Can be configured to show memory usage. Colors and
   granularity are configurable. (@Alizter and @ejgallego, ejgallego/coq-lsp#686,
   grants ejgallego/coq-lsp#681).
 - allow more than one input position in `selectionRange` LSP call
   (@ejgallego, ejgallego/coq-lsp#667, fixes ejgallego/coq-lsp#663)
 - new VSCode commands to allow to move one sentence backwards /
   forward, this is particularly useful when combined with lazy
   checking mode (@ejgallego, ejgallego/coq-lsp#671, fixes ejgallego/coq-lsp#263, fixes ejgallego/coq-lsp#580)
 - VSCode commands `coq-lsp.sentenceNext` / `coq-lsp.sentencePrevious`
   are now bound by default to `Alt + N` / `Alt + P` keybindings
   (@ejgallego, ejgallego/coq-lsp#718)
 - change diagnostic `extra` field to `data`, so we now conform to the
   LSP spec, include the data only when the `send_diags_extra_data`
   server-side option is enabled (@ejgallego, ejgallego/coq-lsp#670)
 - include range of full sentence in error diagnostic extra data
   (@ejgallego, ejgallego/coq-lsp#670 , thanks to @driverag22 for the idea, cc: ejgallego/coq-lsp#663).
 - The `coq-lsp.pp_type` VSCode client option now takes effect
   immediately, no more need to restart the server to get different
   goal display formats (@ejgallego, ejgallego/coq-lsp#675)
 - new public VSCode extension API so other extensions can perform
   actions when the user request the goals (@ejgallego, @bhaktishh,
   ejgallego/coq-lsp#672, fixes ejgallego/coq-lsp#538)
 - Support Visual Studio Live Share URIs better (`vsls://`), in
   particular don't try to display goals if the URI is VSLS one
   (@ejgallego, ejgallego/coq-lsp#676)
 - New `InjectRequire` plugin API for plugins to be able to instrument
   the default import list of files (@ejgallego @corwin-of-amber,
   ejgallego/coq-lsp#679)
 - Add `--max_errors=n` option to `fcc`, this way users can set
   `--max_errors=0` to imitate `coqc` behavior (@ejgallego, ejgallego/coq-lsp#680)
 - Fix `fcc` exit status when checking terminates with fatal errors
   (@ejgallego, @Alizter, ejgallego/coq-lsp#680)
 - Fix install to OPAM switches from `main` branch (@ejgallego, ejgallego/coq-lsp#683,
   fixes ejgallego/coq-lsp#682, cc ejgallego/coq-lsp#479 ejgallego/coq-lsp#488, thanks to @HazardousPeach for the report)
 - New `--int_backend={Coq,Mp}` command line parameter to select the
   interruption method for Coq (@ejgallego, ejgallego/coq-lsp#684)
 - Update `package-lock.json` for latest bugfixes (@ejgallego, ejgallego/coq-lsp#687)
 - Update Nix flake enviroment (@Alizter, ejgallego/coq-lsp#684 ejgallego/coq-lsp#688)
 - Update `prettier` (@Alizter @ejgallego, ejgallego/coq-lsp#684 ejgallego/coq-lsp#688)
 - Store original performance data in the cache, so we now display the
   original timing and memory data even for cached commands (@ejgallego, ejgallego/coq-lsp#693)
 - Fix type errors in the Performance Data Notifications (@ejgallego,
   @Alizter, ejgallego/coq-lsp#689, ejgallego/coq-lsp#693)
 - Send performance performance data for the full document
   (@ejgallego, @Alizter, ejgallego/coq-lsp#689, ejgallego/coq-lsp#693)
 - Better types `coq/perfData` call (@ejgallego @Alizter, ejgallego/coq-lsp#689)
 - New server option to enable / disable `coq/perfData` (@ejgallego, ejgallego/coq-lsp#689)
 - New client option to enable / disable `coq/perfData` (@ejgallego, ejgallego/coq-lsp#717)
 - The `coq-lsp.document` VSCode command will now display the returned
   JSON data in a new editor (@ejgallego, ejgallego/coq-lsp#701)
 - Update server settings on the fly when tweaking them in VSCode.
   Implement `workspace/didChangeConfiguration` (@ejgallego, ejgallego/coq-lsp#702)
 - [Coq API] Add functions to retrieve list of declarations done in
   .vo files (@ejallego, @eytans, ejgallego/coq-lsp#704)
 - New `petanque` API to interact directly with Coq's proof
   engine. (@ejgallego, @gbdrt, Laetitia Teodorescu ejgallego/coq-lsp#703, thanks to
   Alex Sanchez-Stern for many insightful feedback and testing)
 - New `petanque` JSON-RPC `pet.exe`, which can be used à la SerAPI
   to perform proof search and more (@ejgallego, @gbdrt, ejgallego/coq-lsp#705)
 - New `pet-server.exe` TCP server for keep-alive sessions (@gbdrt,
   ejgallego/coq-lsp#697)
 - Always dispose UI elements. This should improve some strange
   behaviors on extension restart (@ejgallego, ejgallego/coq-lsp#708)
 - [code] Added new heatmap feature allowing timing data to be seen in
   the editor. Can be enabled with the `Coq LSP: Toggle heatmap`
   comamnd. Can be configured to show memory usage. Colors and
   granularity are configurable. (@Alizter and @ejgallego, ejgallego/coq-lsp#686,
   grants ejgallego/coq-lsp#681).
 - [server] Support Coq meta-commands (Reset, Reset Initial, Back)
   They are actually pretty useful to hint the incremental engine to
   ignore changes in some part of the document (@ejgallego, ejgallego/coq-lsp#709)
 - JSON-RPC library now supports all kind of incoming messages
   (@ejgallego, ejgallego/coq-lsp#713)
 - [code/server] New `coq/viewRange` notification, from client to
   server, than hints the scheduler for the visible area of the
   document; combined with the new lazy checking mode, this provides
   checking on scroll, a feature inspired from Isabelle IDE
   (@ejgallego, ejgallego/coq-lsp#717)
 - [code] Have VSCode wait for full LSP client shutdown on server
   restart. This fixes some bugs on extension restart (finally!)
   (@ejgallego, ejgallego/coq-lsp#719)
 - [code] Center the view if cursor goes out of scope in
   `sentenceNext/sentencePrevious` (@ejgallego, ejgallego/coq-lsp#718)
 - Switch Flèche range encoding to protocol native, this means UTF-16
   code points for now (Léo Stefanesco, @ejgallego, ejgallego/coq-lsp#624, fixes ejgallego/coq-lsp#620,
   ejgallego/coq-lsp#621)
 - Give `Goals` panel focus back if it has lost it (in case of
   multiple panels in the second viewColumn of Vscode) whenever
   user navigates proofs (@Alidra @ejgallego, ejgallego/coq-lsp#722, ejgallego/coq-lsp#725)
 - `fcc`: new option `--diags_level` to control whether Coq's notice
   and info messages appear as diagnostics
 - [code] Display the continous/on-request checking mode in the status bar,
   allow to change it by clicking on it (@ejgallego, ejgallego/coq-lsp#721)
 - Add an example of multiple workspaces (@ejgallego, @Blaisorblade,
   ejgallego/coq-lsp#611)
 - Don't show types of un-expanded goals. We should add an option for
   this, but we don't have the cycles (@ejgallego, ejgallego/coq-lsp#730, workarounds
   ejgallego/coq-lsp#525 ejgallego/coq-lsp#652)
 - Support for `.lv / .v.tex` TeX files with embedded Coq code
   (@ejgallego, ejgallego/coq-lsp#727)
 - Don't expand bullet goals at previous levels by default
   (@ejgallego, @Alizter, ejgallego/coq-lsp#731 cc ejgallego/coq-lsp#525)
 - [petanque] Return basic goal information after `run_tac`, so we
   avoid a `goals` round-trip for each tactic (@gbdrt, @ejgallego,
   ejgallego/coq-lsp#733)
 - [coq] Add support for reading glob files metadata (@ejgallego,
   ejgallego/coq-lsp#735)
 - [petanque] Return extra premise information: file name, position,
   raw_text, using the above support for reading .glob files
   (@ejgallego, ejgallego/coq-lsp#735)
 - [code] Display server status using the `LanguageStatusItem`
   facility, for now we display version and checking status
   information (moved from ejgallego/coq-lsp#721), and we also allow to toggle the
   checking mode from there (@ejgallego, ejgallego/coq-lsp#728)
avsm pushed a commit to avsm/opam-repository that referenced this pull request Sep 5, 2024
@ejgallego @avsm
[new release] coq-lsp (0.1.9+8.18)
de5b102 
CHANGES:

---------------------------------------

 - new option `show_loc_info_on_hover` that will display parsing debug
   information on hover; previous flag was fixed in code, which is way
   less flexible. This also fixes the option being on in 0.1.8 by
   mistake (@ejgallego, ejgallego/coq-lsp#588)
 - hover plugins can now access the full document, this is convenient
   for many use cases (@ejgallego, ejgallego/coq-lsp#591)
 - fix hover position computation on the presence of Utf characters
   (@ejgallego, ejgallego/coq-lsp#597, thanks to Pierre Courtieu for the report and
   example, closes ejgallego/coq-lsp#594)
 - fix activation bug that prevented extension activation for `.mv`
   files, see discussion in the issues about the upstream policy
   (@ejgallego @r3m0t, ejgallego/coq-lsp#598, cc ejgallego/coq-lsp#596, reported by Théo Zimmerman)
 - require VSCode >= 1.82 in package.json . Our VSCode extension uses
   `vscode-languageclient` 9 which imposes this. (@ejgallego, ejgallego/coq-lsp#599,
   thanks to Théo Zimmerman for the report)
 - `proof/goals` request: new `mode` parameter, to specify goals
   after/before sentence display; renamed `pretac` to `command`, as to
   provide official support for speculative execution (@ejgallego, ejgallego/coq-lsp#600)
 - fix some cases where interrupted computations where memoized
   (@ejgallego, ejgallego/coq-lsp#603)
 - [internal] Flèche [Doc.t] API will now absorb errors on document
   update and creation into the document itself. Thus, a document that
   failed to create or update is still valid, but in the right failed
   state. This is a much needed API change for a lot of use cases
   (@ejgallego, ejgallego/coq-lsp#604)
 - support OCaml 5.1.x (@ejgallego, ejgallego/coq-lsp#606)
 - update progress indicator correctly on End Of File (@ejgallego,
   ejgallego/coq-lsp#605, fixes ejgallego/coq-lsp#445)
 - [plugins] New `astdump` plugin to dump AST of files into JSON and
   SEXP (@ejgallego, ejgallego/coq-lsp#607)
 - errors on save where not properly caught (@ejgallego, ejgallego/coq-lsp#608)
 - switch default of `goal_after_tactic` to `true` (@Alizter,
   @ejgallego, cc: ejgallego/coq-lsp#614)
 - error recovery: Recognize `Defined` and `Admitted` in lex recovery
   (@ejgallego, ejgallego/coq-lsp#616)
 - completion: correctly understand UTF-16 code points on completion
   request (Léo Stefanesco, ejgallego/coq-lsp#613, fixes ejgallego/coq-lsp#531)
 - don't trigger the goals window in general markdown buffer
   (@ejgallego, ejgallego/coq-lsp#625, reported by Théo Zimmerman)
 - allow not to postpone full document requests (ejgallego/coq-lsp#626, @ejgallego)
 - new configuration value `check_only_on_request` which will delay
   checking the document until a request has been made (ejgallego/coq-lsp#629, cc: ejgallego/coq-lsp#24,
   @ejgallego)
 - fix typo on package.json configuration section (@ejgallego, ejgallego/coq-lsp#645)
 - be more resilient with invalid _CoqProject files (@ejgallego, ejgallego/coq-lsp#646)
 - support for Coq 8.16 has been abandoned due to lack of dev
   resources (@ejgallego, ejgallego/coq-lsp#649)
 - new option `--no_vo` for `fcc`, which will skip the `.vo` saving
   step. `.vo` saving is now an `fcc` plugins, but for now, it is
   enabled by default (@ejgallego, ejgallego/coq-lsp#650)
 - depend on `memprof-limits` on OCaml 4.x (@ejgallego, ejgallego/coq-lsp#660)
 - bump minimal OCaml version to 4.12 due to `memprof-limits`
   (@ejgallego, ejgallego/coq-lsp#660)
 - monitor all Coq-level calls under an interruption token
   (@ejgallego, ejgallego/coq-lsp#661)
 - interpret require thru our own custom execution env-aware path
   (@bhaktishh, @ejgallego, ejgallego/coq-lsp#642, ejgallego/coq-lsp#643, ejgallego/coq-lsp#644)
 - new `coq-lsp.plugin.goaldump` plugin, as an example on how to dump
   goals from a document (@ejgallego @gbdrt, ejgallego/coq-lsp#619)
 - new trim command (both in the server and in VSCode) to liberate
   space used in the cache (@ejgallego, ejgallego/coq-lsp#662, fixes ejgallego/coq-lsp#367 cc: ejgallego/coq-lsp#253 ejgallego/coq-lsp#236
   ejgallego/coq-lsp#348)
 - fix Coq performance view display (@ejgallego, ejgallego/coq-lsp#663, regression in
   ejgallego/coq-lsp#513)
 - Added new heatmap feature allowing timing data to be seen in the
   editor. Can be enabled with the `Coq LSP: Toggle heatmap`
   command. Can be configured to show memory usage. Colors and
   granularity are configurable. (@Alizter and @ejgallego, ejgallego/coq-lsp#686,
   grants ejgallego/coq-lsp#681).
 - allow more than one input position in `selectionRange` LSP call
   (@ejgallego, ejgallego/coq-lsp#667, fixes ejgallego/coq-lsp#663)
 - new VSCode commands to allow to move one sentence backwards /
   forward, this is particularly useful when combined with lazy
   checking mode (@ejgallego, ejgallego/coq-lsp#671, fixes ejgallego/coq-lsp#263, fixes ejgallego/coq-lsp#580)
 - VSCode commands `coq-lsp.sentenceNext` / `coq-lsp.sentencePrevious`
   are now bound by default to `Alt + N` / `Alt + P` keybindings
   (@ejgallego, ejgallego/coq-lsp#718)
 - change diagnostic `extra` field to `data`, so we now conform to the
   LSP spec, include the data only when the `send_diags_extra_data`
   server-side option is enabled (@ejgallego, ejgallego/coq-lsp#670)
 - include range of full sentence in error diagnostic extra data
   (@ejgallego, ejgallego/coq-lsp#670 , thanks to @driverag22 for the idea, cc: ejgallego/coq-lsp#663).
 - The `coq-lsp.pp_type` VSCode client option now takes effect
   immediately, no more need to restart the server to get different
   goal display formats (@ejgallego, ejgallego/coq-lsp#675)
 - new public VSCode extension API so other extensions can perform
   actions when the user request the goals (@ejgallego, @bhaktishh,
   ejgallego/coq-lsp#672, fixes ejgallego/coq-lsp#538)
 - Support Visual Studio Live Share URIs better (`vsls://`), in
   particular don't try to display goals if the URI is VSLS one
   (@ejgallego, ejgallego/coq-lsp#676)
 - New `InjectRequire` plugin API for plugins to be able to instrument
   the default import list of files (@ejgallego @corwin-of-amber,
   ejgallego/coq-lsp#679)
 - Add `--max_errors=n` option to `fcc`, this way users can set
   `--max_errors=0` to imitate `coqc` behavior (@ejgallego, ejgallego/coq-lsp#680)
 - Fix `fcc` exit status when checking terminates with fatal errors
   (@ejgallego, @Alizter, ejgallego/coq-lsp#680)
 - Fix install to OPAM switches from `main` branch (@ejgallego, ejgallego/coq-lsp#683,
   fixes ejgallego/coq-lsp#682, cc ejgallego/coq-lsp#479 ejgallego/coq-lsp#488, thanks to @HazardousPeach for the report)
 - New `--int_backend={Coq,Mp}` command line parameter to select the
   interruption method for Coq (@ejgallego, ejgallego/coq-lsp#684)
 - Update `package-lock.json` for latest bugfixes (@ejgallego, ejgallego/coq-lsp#687)
 - Update Nix flake enviroment (@Alizter, ejgallego/coq-lsp#684 ejgallego/coq-lsp#688)
 - Update `prettier` (@Alizter @ejgallego, ejgallego/coq-lsp#684 ejgallego/coq-lsp#688)
 - Store original performance data in the cache, so we now display the
   original timing and memory data even for cached commands (@ejgallego, ejgallego/coq-lsp#693)
 - Fix type errors in the Performance Data Notifications (@ejgallego,
   @Alizter, ejgallego/coq-lsp#689, ejgallego/coq-lsp#693)
 - Send performance performance data for the full document
   (@ejgallego, @Alizter, ejgallego/coq-lsp#689, ejgallego/coq-lsp#693)
 - Better types `coq/perfData` call (@ejgallego @Alizter, ejgallego/coq-lsp#689)
 - New server option to enable / disable `coq/perfData` (@ejgallego, ejgallego/coq-lsp#689)
 - New client option to enable / disable `coq/perfData` (@ejgallego, ejgallego/coq-lsp#717)
 - The `coq-lsp.document` VSCode command will now display the returned
   JSON data in a new editor (@ejgallego, ejgallego/coq-lsp#701)
 - Update server settings on the fly when tweaking them in VSCode.
   Implement `workspace/didChangeConfiguration` (@ejgallego, ejgallego/coq-lsp#702)
 - [Coq API] Add functions to retrieve list of declarations done in
   .vo files (@ejallego, @eytans, ejgallego/coq-lsp#704)
 - New `petanque` API to interact directly with Coq's proof
   engine. (@ejgallego, @gbdrt, Laetitia Teodorescu ejgallego/coq-lsp#703, thanks to
   Alex Sanchez-Stern for many insightful feedback and testing)
 - New `petanque` JSON-RPC `pet.exe`, which can be used à la SerAPI
   to perform proof search and more (@ejgallego, @gbdrt, ejgallego/coq-lsp#705)
 - New `pet-server.exe` TCP server for keep-alive sessions (@gbdrt,
   ejgallego/coq-lsp#697)
 - Always dispose UI elements. This should improve some strange
   behaviors on extension restart (@ejgallego, ejgallego/coq-lsp#708)
 - [code] Added new heatmap feature allowing timing data to be seen in
   the editor. Can be enabled with the `Coq LSP: Toggle heatmap`
   comamnd. Can be configured to show memory usage. Colors and
   granularity are configurable. (@Alizter and @ejgallego, ejgallego/coq-lsp#686,
   grants ejgallego/coq-lsp#681).
 - [server] Support Coq meta-commands (Reset, Reset Initial, Back)
   They are actually pretty useful to hint the incremental engine to
   ignore changes in some part of the document (@ejgallego, ejgallego/coq-lsp#709)
 - JSON-RPC library now supports all kind of incoming messages
   (@ejgallego, ejgallego/coq-lsp#713)
 - [code/server] New `coq/viewRange` notification, from client to
   server, than hints the scheduler for the visible area of the
   document; combined with the new lazy checking mode, this provides
   checking on scroll, a feature inspired from Isabelle IDE
   (@ejgallego, ejgallego/coq-lsp#717)
 - [code] Have VSCode wait for full LSP client shutdown on server
   restart. This fixes some bugs on extension restart (finally!)
   (@ejgallego, ejgallego/coq-lsp#719)
 - [code] Center the view if cursor goes out of scope in
   `sentenceNext/sentencePrevious` (@ejgallego, ejgallego/coq-lsp#718)
 - Switch Flèche range encoding to protocol native, this means UTF-16
   code points for now (Léo Stefanesco, @ejgallego, ejgallego/coq-lsp#624, fixes ejgallego/coq-lsp#620,
   ejgallego/coq-lsp#621)
 - Give `Goals` panel focus back if it has lost it (in case of
   multiple panels in the second viewColumn of Vscode) whenever
   user navigates proofs (@Alidra @ejgallego, ejgallego/coq-lsp#722, ejgallego/coq-lsp#725)
 - `fcc`: new option `--diags_level` to control whether Coq's notice
   and info messages appear as diagnostics
 - [code] Display the continous/on-request checking mode in the status bar,
   allow to change it by clicking on it (@ejgallego, ejgallego/coq-lsp#721)
 - Add an example of multiple workspaces (@ejgallego, @Blaisorblade,
   ejgallego/coq-lsp#611)
 - Don't show types of un-expanded goals. We should add an option for
   this, but we don't have the cycles (@ejgallego, ejgallego/coq-lsp#730, workarounds
   ejgallego/coq-lsp#525 ejgallego/coq-lsp#652)
 - Support for `.lv / .v.tex` TeX files with embedded Coq code
   (@ejgallego, ejgallego/coq-lsp#727)
 - Don't expand bullet goals at previous levels by default
   (@ejgallego, @Alizter, ejgallego/coq-lsp#731 cc ejgallego/coq-lsp#525)
 - [petanque] Return basic goal information after `run_tac`, so we
   avoid a `goals` round-trip for each tactic (@gbdrt, @ejgallego,
   ejgallego/coq-lsp#733)
 - [coq] Add support for reading glob files metadata (@ejgallego,
   ejgallego/coq-lsp#735)
 - [petanque] Return extra premise information: file name, position,
   raw_text, using the above support for reading .glob files
   (@ejgallego, ejgallego/coq-lsp#735)
 - [code] Display server status using the `LanguageStatusItem`
   facility, for now we display version and checking status
   information (moved from ejgallego/coq-lsp#721), and we also allow to toggle the
   checking mode from there (@ejgallego, ejgallego/coq-lsp#728)
avsm pushed a commit to avsm/opam-repository that referenced this pull request Sep 5, 2024
@ejgallego @avsm
[new release] coq-lsp (0.1.9+8.19)
2c18e54 
CHANGES:

---------------------------------------

 - new option `show_loc_info_on_hover` that will display parsing debug
   information on hover; previous flag was fixed in code, which is way
   less flexible. This also fixes the option being on in 0.1.8 by
   mistake (@ejgallego, ejgallego/coq-lsp#588)
 - hover plugins can now access the full document, this is convenient
   for many use cases (@ejgallego, ejgallego/coq-lsp#591)
 - fix hover position computation on the presence of Utf characters
   (@ejgallego, ejgallego/coq-lsp#597, thanks to Pierre Courtieu for the report and
   example, closes ejgallego/coq-lsp#594)
 - fix activation bug that prevented extension activation for `.mv`
   files, see discussion in the issues about the upstream policy
   (@ejgallego @r3m0t, ejgallego/coq-lsp#598, cc ejgallego/coq-lsp#596, reported by Théo Zimmerman)
 - require VSCode >= 1.82 in package.json . Our VSCode extension uses
   `vscode-languageclient` 9 which imposes this. (@ejgallego, ejgallego/coq-lsp#599,
   thanks to Théo Zimmerman for the report)
 - `proof/goals` request: new `mode` parameter, to specify goals
   after/before sentence display; renamed `pretac` to `command`, as to
   provide official support for speculative execution (@ejgallego, ejgallego/coq-lsp#600)
 - fix some cases where interrupted computations where memoized
   (@ejgallego, ejgallego/coq-lsp#603)
 - [internal] Flèche [Doc.t] API will now absorb errors on document
   update and creation into the document itself. Thus, a document that
   failed to create or update is still valid, but in the right failed
   state. This is a much needed API change for a lot of use cases
   (@ejgallego, ejgallego/coq-lsp#604)
 - support OCaml 5.1.x (@ejgallego, ejgallego/coq-lsp#606)
 - update progress indicator correctly on End Of File (@ejgallego,
   ejgallego/coq-lsp#605, fixes ejgallego/coq-lsp#445)
 - [plugins] New `astdump` plugin to dump AST of files into JSON and
   SEXP (@ejgallego, ejgallego/coq-lsp#607)
 - errors on save where not properly caught (@ejgallego, ejgallego/coq-lsp#608)
 - switch default of `goal_after_tactic` to `true` (@Alizter,
   @ejgallego, cc: ejgallego/coq-lsp#614)
 - error recovery: Recognize `Defined` and `Admitted` in lex recovery
   (@ejgallego, ejgallego/coq-lsp#616)
 - completion: correctly understand UTF-16 code points on completion
   request (Léo Stefanesco, ejgallego/coq-lsp#613, fixes ejgallego/coq-lsp#531)
 - don't trigger the goals window in general markdown buffer
   (@ejgallego, ejgallego/coq-lsp#625, reported by Théo Zimmerman)
 - allow not to postpone full document requests (ejgallego/coq-lsp#626, @ejgallego)
 - new configuration value `check_only_on_request` which will delay
   checking the document until a request has been made (ejgallego/coq-lsp#629, cc: ejgallego/coq-lsp#24,
   @ejgallego)
 - fix typo on package.json configuration section (@ejgallego, ejgallego/coq-lsp#645)
 - be more resilient with invalid _CoqProject files (@ejgallego, ejgallego/coq-lsp#646)
 - support for Coq 8.16 has been abandoned due to lack of dev
   resources (@ejgallego, ejgallego/coq-lsp#649)
 - new option `--no_vo` for `fcc`, which will skip the `.vo` saving
   step. `.vo` saving is now an `fcc` plugins, but for now, it is
   enabled by default (@ejgallego, ejgallego/coq-lsp#650)
 - depend on `memprof-limits` on OCaml 4.x (@ejgallego, ejgallego/coq-lsp#660)
 - bump minimal OCaml version to 4.12 due to `memprof-limits`
   (@ejgallego, ejgallego/coq-lsp#660)
 - monitor all Coq-level calls under an interruption token
   (@ejgallego, ejgallego/coq-lsp#661)
 - interpret require thru our own custom execution env-aware path
   (@bhaktishh, @ejgallego, ejgallego/coq-lsp#642, ejgallego/coq-lsp#643, ejgallego/coq-lsp#644)
 - new `coq-lsp.plugin.goaldump` plugin, as an example on how to dump
   goals from a document (@ejgallego @gbdrt, ejgallego/coq-lsp#619)
 - new trim command (both in the server and in VSCode) to liberate
   space used in the cache (@ejgallego, ejgallego/coq-lsp#662, fixes ejgallego/coq-lsp#367 cc: ejgallego/coq-lsp#253 ejgallego/coq-lsp#236
   ejgallego/coq-lsp#348)
 - fix Coq performance view display (@ejgallego, ejgallego/coq-lsp#663, regression in
   ejgallego/coq-lsp#513)
 - Added new heatmap feature allowing timing data to be seen in the
   editor. Can be enabled with the `Coq LSP: Toggle heatmap`
   command. Can be configured to show memory usage. Colors and
   granularity are configurable. (@Alizter and @ejgallego, ejgallego/coq-lsp#686,
   grants ejgallego/coq-lsp#681).
 - allow more than one input position in `selectionRange` LSP call
   (@ejgallego, ejgallego/coq-lsp#667, fixes ejgallego/coq-lsp#663)
 - new VSCode commands to allow to move one sentence backwards /
   forward, this is particularly useful when combined with lazy
   checking mode (@ejgallego, ejgallego/coq-lsp#671, fixes ejgallego/coq-lsp#263, fixes ejgallego/coq-lsp#580)
 - VSCode commands `coq-lsp.sentenceNext` / `coq-lsp.sentencePrevious`
   are now bound by default to `Alt + N` / `Alt + P` keybindings
   (@ejgallego, ejgallego/coq-lsp#718)
 - change diagnostic `extra` field to `data`, so we now conform to the
   LSP spec, include the data only when the `send_diags_extra_data`
   server-side option is enabled (@ejgallego, ejgallego/coq-lsp#670)
 - include range of full sentence in error diagnostic extra data
   (@ejgallego, ejgallego/coq-lsp#670 , thanks to @driverag22 for the idea, cc: ejgallego/coq-lsp#663).
 - The `coq-lsp.pp_type` VSCode client option now takes effect
   immediately, no more need to restart the server to get different
   goal display formats (@ejgallego, ejgallego/coq-lsp#675)
 - new public VSCode extension API so other extensions can perform
   actions when the user request the goals (@ejgallego, @bhaktishh,
   ejgallego/coq-lsp#672, fixes ejgallego/coq-lsp#538)
 - Support Visual Studio Live Share URIs better (`vsls://`), in
   particular don't try to display goals if the URI is VSLS one
   (@ejgallego, ejgallego/coq-lsp#676)
 - New `InjectRequire` plugin API for plugins to be able to instrument
   the default import list of files (@ejgallego @corwin-of-amber,
   ejgallego/coq-lsp#679)
 - Add `--max_errors=n` option to `fcc`, this way users can set
   `--max_errors=0` to imitate `coqc` behavior (@ejgallego, ejgallego/coq-lsp#680)
 - Fix `fcc` exit status when checking terminates with fatal errors
   (@ejgallego, @Alizter, ejgallego/coq-lsp#680)
 - Fix install to OPAM switches from `main` branch (@ejgallego, ejgallego/coq-lsp#683,
   fixes ejgallego/coq-lsp#682, cc ejgallego/coq-lsp#479 ejgallego/coq-lsp#488, thanks to @HazardousPeach for the report)
 - New `--int_backend={Coq,Mp}` command line parameter to select the
   interruption method for Coq (@ejgallego, ejgallego/coq-lsp#684)
 - Update `package-lock.json` for latest bugfixes (@ejgallego, ejgallego/coq-lsp#687)
 - Update Nix flake enviroment (@Alizter, ejgallego/coq-lsp#684 ejgallego/coq-lsp#688)
 - Update `prettier` (@Alizter @ejgallego, ejgallego/coq-lsp#684 ejgallego/coq-lsp#688)
 - Store original performance data in the cache, so we now display the
   original timing and memory data even for cached commands (@ejgallego, ejgallego/coq-lsp#693)
 - Fix type errors in the Performance Data Notifications (@ejgallego,
   @Alizter, ejgallego/coq-lsp#689, ejgallego/coq-lsp#693)
 - Send performance performance data for the full document
   (@ejgallego, @Alizter, ejgallego/coq-lsp#689, ejgallego/coq-lsp#693)
 - Better types `coq/perfData` call (@ejgallego @Alizter, ejgallego/coq-lsp#689)
 - New server option to enable / disable `coq/perfData` (@ejgallego, ejgallego/coq-lsp#689)
 - New client option to enable / disable `coq/perfData` (@ejgallego, ejgallego/coq-lsp#717)
 - The `coq-lsp.document` VSCode command will now display the returned
   JSON data in a new editor (@ejgallego, ejgallego/coq-lsp#701)
 - Update server settings on the fly when tweaking them in VSCode.
   Implement `workspace/didChangeConfiguration` (@ejgallego, ejgallego/coq-lsp#702)
 - [Coq API] Add functions to retrieve list of declarations done in
   .vo files (@ejallego, @eytans, ejgallego/coq-lsp#704)
 - New `petanque` API to interact directly with Coq's proof
   engine. (@ejgallego, @gbdrt, Laetitia Teodorescu ejgallego/coq-lsp#703, thanks to
   Alex Sanchez-Stern for many insightful feedback and testing)
 - New `petanque` JSON-RPC `pet.exe`, which can be used à la SerAPI
   to perform proof search and more (@ejgallego, @gbdrt, ejgallego/coq-lsp#705)
 - New `pet-server.exe` TCP server for keep-alive sessions (@gbdrt,
   ejgallego/coq-lsp#697)
 - Always dispose UI elements. This should improve some strange
   behaviors on extension restart (@ejgallego, ejgallego/coq-lsp#708)
 - [code] Added new heatmap feature allowing timing data to be seen in
   the editor. Can be enabled with the `Coq LSP: Toggle heatmap`
   comamnd. Can be configured to show memory usage. Colors and
   granularity are configurable. (@Alizter and @ejgallego, ejgallego/coq-lsp#686,
   grants ejgallego/coq-lsp#681).
 - [server] Support Coq meta-commands (Reset, Reset Initial, Back)
   They are actually pretty useful to hint the incremental engine to
   ignore changes in some part of the document (@ejgallego, ejgallego/coq-lsp#709)
 - JSON-RPC library now supports all kind of incoming messages
   (@ejgallego, ejgallego/coq-lsp#713)
 - [code/server] New `coq/viewRange` notification, from client to
   server, than hints the scheduler for the visible area of the
   document; combined with the new lazy checking mode, this provides
   checking on scroll, a feature inspired from Isabelle IDE
   (@ejgallego, ejgallego/coq-lsp#717)
 - [code] Have VSCode wait for full LSP client shutdown on server
   restart. This fixes some bugs on extension restart (finally!)
   (@ejgallego, ejgallego/coq-lsp#719)
 - [code] Center the view if cursor goes out of scope in
   `sentenceNext/sentencePrevious` (@ejgallego, ejgallego/coq-lsp#718)
 - Switch Flèche range encoding to protocol native, this means UTF-16
   code points for now (Léo Stefanesco, @ejgallego, ejgallego/coq-lsp#624, fixes ejgallego/coq-lsp#620,
   ejgallego/coq-lsp#621)
 - Give `Goals` panel focus back if it has lost it (in case of
   multiple panels in the second viewColumn of Vscode) whenever
   user navigates proofs (@Alidra @ejgallego, ejgallego/coq-lsp#722, ejgallego/coq-lsp#725)
 - `fcc`: new option `--diags_level` to control whether Coq's notice
   and info messages appear as diagnostics
 - [code] Display the continous/on-request checking mode in the status bar,
   allow to change it by clicking on it (@ejgallego, ejgallego/coq-lsp#721)
 - Add an example of multiple workspaces (@ejgallego, @Blaisorblade,
   ejgallego/coq-lsp#611)
 - Don't show types of un-expanded goals. We should add an option for
   this, but we don't have the cycles (@ejgallego, ejgallego/coq-lsp#730, workarounds
   ejgallego/coq-lsp#525 ejgallego/coq-lsp#652)
 - Support for `.lv / .v.tex` TeX files with embedded Coq code
   (@ejgallego, ejgallego/coq-lsp#727)
 - Don't expand bullet goals at previous levels by default
   (@ejgallego, @Alizter, ejgallego/coq-lsp#731 cc ejgallego/coq-lsp#525)
 - [petanque] Return basic goal information after `run_tac`, so we
   avoid a `goals` round-trip for each tactic (@gbdrt, @ejgallego,
   ejgallego/coq-lsp#733)
 - [coq] Add support for reading glob files metadata (@ejgallego,
   ejgallego/coq-lsp#735)
 - [petanque] Return extra premise information: file name, position,
   raw_text, using the above support for reading .glob files
   (@ejgallego, ejgallego/coq-lsp#735)
 - [code] Display server status using the `LanguageStatusItem`
   facility, for now we display version and checking status
   information (moved from ejgallego/coq-lsp#721), and we also allow to toggle the
   checking mode from there (@ejgallego, ejgallego/coq-lsp#728)
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)
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: fix part: client (VSCode) part: goals and info panel
Projects
None yet
Milestone
0.1.9
Development

Successfully merging this pull request may close these issues.
1 participant
@ejgallego