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

Minor issue with vim and cursor tracking #614

Closed
qcfu-bu opened this issue Nov 20, 2023 · 7 comments
Closed

Minor issue with vim and cursor tracking #614

qcfu-bu opened this issue Nov 20, 2023 · 7 comments
Labels
kind: question Further information is requested lsp: goals part: protocol (custom)

Comments

@qcfu-bu
Copy link

qcfu-bu commented Nov 20, 2023

I have a minor issue when it comes to using coq-lsp together VscodeVim.

In vim normal-mode, when the cursor is placed on the period at the end of a tactic, the Goals do not update to reflect the application of the tactic.

rewrite H1.
          ^

Only when the cursor is moved after the period does the goal update.

rewrite H1.
           ^

This behavior is a little annoying when browsing through source files in normal-mode as the tactics at the end of each line do not get applied until the start of the next line.

When trying this with Lean4's extension, they seem to register cursor's position across the entire tactic.

rewrite H1.
^^^^^^^^^^^
@qcfu-bu
Copy link
Author

qcfu-bu commented Nov 21, 2023

Nvm, turning on 'Goal_after_tactic' gives me the exact functionality I wanted.

@qcfu-bu qcfu-bu closed this as completed Nov 21, 2023
@Alizter
Copy link
Collaborator

Alizter commented Nov 21, 2023

@ejgallego how do you feel about making this setting the default?

@ejgallego
Copy link
Owner

Happy to do so! Indeed seems like the most reasonable default.

Note that in main the proof/goals request does indeed take the parameter, so different goals requests can use a different setting; this is IMHO better, as it allows the client to be more flexible.

This setting is a bit weird in the sense that for example, it doesn't affect errors or messages, that we currently relay on the proof/goals call.

@ejgallego
Copy link
Owner

@qcfu-bu sorry for the trouble, indeed I think we should change the default of this option.

@qcfu-bu
Copy link
Author

qcfu-bu commented Nov 21, 2023 •
edited
Loading

@qcfu-bu sorry for the trouble, indeed I think we should change the default of this option.

No worries! The experience after turning it on so much more enjoyable imo!

@Alizter
Copy link
Collaborator

Alizter commented Nov 21, 2023

We also all have it turned on which is why it probably makes sense to be the default now. :)

@ejgallego
Copy link
Owner

@qcfu-bu sorry for the trouble, indeed I think we should change the default of this option.

No worries! The experience after turning it on so much more enjoyable imo!

Thanks; let us know of any further improvement we can do!

ejgallego added a commit that referenced this issue Nov 21, 2023
@ejgallego
[config] set goal_after_tactic default to true
a0f8951 
cc: #614
@ejgallego ejgallego mentioned this issue Nov 21, 2023
Merged
@ejgallego ejgallego mentioned this issue May 31, 2024
Merged
ejgallego added a commit to ejgallego/opam-repository that referenced this issue May 31, 2024
@ejgallego
[new release] coq-lsp (0.1.9+8.18)
feb250e 
CHANGES:

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

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

No branches or pull requests
3 participants
@ejgallego @Alizter @qcfu-bu