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

[petanque] Initial commit, as an OCaml library #703

Merged
merged 1 commit into from
May 13, 2024
Merged

[petanque] Initial commit, as an OCaml library #703

merged 1 commit into from
May 13, 2024

Conversation

ejgallego
Copy link
Owner

@ejgallego ejgallego commented May 13, 2024 •
edited
Loading

This is the first version of petanque, suitable for merging.

TODO before merging:

  • basic test suite (API)
  • complete premises API
  • update README.md

@ejgallego ejgallego added this to the 0.1.9 milestone May 13, 2024
@Alizter
Copy link
Collaborator

Alizter commented May 13, 2024

What exactly is it? I read the README but I didn't understand anything.

@ejgallego ejgallego force-pushed the petanque branch 2 times, most recently from 7b6b9ce to d26914f Compare May 13, 2024 14:30
Alizter
Alizter reviewed May 13, 2024
View reviewed changes
README.md Outdated Show resolved Hide resolved
@ejgallego
Copy link
Owner Author

What exactly is it? I read the README but I didn't understand anything.

This is a start of a RL agent for Coq, on top of Flèche, indeed, we need to improve the docs a lot, but for now this is just the first step.

Thanks for checking the README, should be better now and contain a link to Gym in python

Alizter
Alizter reviewed May 13, 2024
View reviewed changes
CONTRIBUTING.md Outdated Show resolved Hide resolved
@ejgallego ejgallego added the kind: enhancement New feature or request label May 13, 2024
@ejgallego ejgallego force-pushed the petanque branch 3 times, most recently from 0dd2aa8 to 7c251cc Compare May 13, 2024 16:46
@ejgallego ejgallego merged commit c822d1e into main May 13, 2024
12 checks passed
@ejgallego ejgallego deleted the petanque branch May 13, 2024 17:15
@ejgallego ejgallego restored the petanque branch May 13, 2024 17:18
@ejgallego ejgallego deleted the petanque branch May 13, 2024 17:20
This was referenced May 31, 2024
Merged
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 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)
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)
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@Alizter Alizter Alizter left review comments

Assignees
No one assigned
Labels
kind: enhancement New feature or request part: petanque
Projects
None yet
Milestone
0.1.9
Development

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