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

Add a Petanque TCP server #697

Merged
merged 2 commits into from
May 30, 2024
Merged

Add a Petanque TCP server #697

merged 2 commits into from
May 30, 2024

Conversation

gbdrt
Copy link
Collaborator

@gbdrt gbdrt commented May 7, 2024

Add a Petanque TCP server to communicate with Coq.

Bug fixes:

  • Run_error: unbound (ocaml 5.1.1)
  • Second starts with same args raise ThmNotFound

@Alizter
Copy link
Collaborator

Alizter commented May 7, 2024

This PR is aimed at the petanque branch, is that intentional?

@ejgallego
Copy link
Owner

This PR is aimed at the petanque branch, is that intentional?

Yes, we will put things in main soonish, once we get the first working prototype.

In an ideal world we could have developed petanque in its own repos, but actually it makes more sense to have a single repos for now due to API coupling and the bad state of multi-repos tooling.

@ejgallego ejgallego force-pushed the petanque branch 10 times, most recently from 7c251cc to a9f2d2d Compare May 13, 2024 16:48
@ejgallego ejgallego deleted the branch ejgallego:main May 13, 2024 17:15
@ejgallego ejgallego closed this May 13, 2024
@ejgallego
Copy link
Owner

Ouch, this was closed because I merged the petanque branch! Let me fix the mess.

@ejgallego ejgallego reopened this May 13, 2024
@ejgallego ejgallego changed the base branch from petanque to petanque-json May 13, 2024 17:19
@ejgallego
Copy link
Owner

ejgallego commented May 13, 2024 •
edited
Loading

Ok, I've rebased this on top of #705 , once #705 goes in we can merge this, but I think we may want to tweak #705 a little bit before.

@ejgallego ejgallego added this to the 0.1.9 milestone May 13, 2024
@ejgallego ejgallego marked this pull request as draft May 13, 2024 19:37
@ejgallego ejgallego force-pushed the petanque-json branch 2 times, most recently from 8ce955f to 2a915d1 Compare May 13, 2024 20:47
@ejgallego ejgallego force-pushed the petanque-json branch 4 times, most recently from 138d732 to 07d8c8c Compare May 14, 2024 16:32
@ejgallego ejgallego deleted the branch ejgallego:main May 16, 2024 19:04
@ejgallego ejgallego closed this May 16, 2024
@ejgallego
Copy link
Owner

That was closed because I deleted the branch this depended upon (again).

Sorry for all the noise, will fix ASAP.

@ejgallego ejgallego reopened this May 17, 2024
@ejgallego ejgallego changed the base branch from petanque-json to main May 17, 2024 09:30
@ejgallego ejgallego force-pushed the pytanque branch 6 times, most recently from 54aa403 to 46fdee0 Compare May 29, 2024 20:44
@ejgallego ejgallego marked this pull request as ready for review May 30, 2024 09:06
@ejgallego ejgallego added the kind: enhancement New feature or request label May 30, 2024
@ejgallego ejgallego merged commit 3ed39a0 into ejgallego:main May 30, 2024
13 checks passed
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
No reviews
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.
3 participants
@gbdrt @Alizter @ejgallego