The Coq mailing list

[Emilio Jesús Gallego Arias <e AT x80.org>]

Dear all,

We are happy to announce the 0.1.9 release of `coq-lsp`.

This release brings many new features and fixes, in particular:

- New on-demand checking mode: `coq-lsp` can now check files on
  demand, either by following the goals requested, or by following the
  current viewport of your editor. Combined with the new keybinding
  `M-n/M-p` for moving between Coq sentences, this provides a mode
  similar to the usual one in Proof General. Additionally, we now show
  real-time server status and checking information in the VSCode
  language status area.

- New interruption support using `memprofs-limits` (only in OCaml
  4). This solves all known cases of the server hanging.
  (By E. J. Gallego Arias, thanks to Guillaume Munch-Maccagnoni and
  Alex Sanchez-Stern).

- `petanque`: a new server built on top of Flèche specifically
  targeted at high-throughput low-latency reinforcement learning
  applications. A subset of `petanque` has been experimentally
  embedded into LSP for profit of extensions. (By E. J. Gallego
  Arias, Guillaume Baudart, and Laetitia Teodorescu; thanks to Alex
  Sanchez-Stern).

- New heatmap feature to detect execution time hotspots in your Coq
  documents, by Ali Caglayan; plus many more improvements and fixes
  w.r.t. performance monitoring.

- Coq meta commands `Reset` / `Reset Inital` and `Back` are supported,
  together with the incremental checking engine they do provide some
  interesting document splitting and isolation features.

- New user manual with some information on how to start with `coq-lsp`

- `coq-lsp` will now recognize literate LaTeX Coq files that end in
  `.v.tex` or `.lv` and allow interacting with the Coq code inside
  `\begin{coq}/\end{coq}` blocks.

- Improved support for VSCode Live Share; full support requires
  approval from Microsoft, please see below if you are interested in
  helping with this.

- New `Free Memory` server command.

- Server settings are now updated on the fly when edited in VSCode.

- Locations are now stored in the server in protocol format, this
  should solve some Unicode issues present in previous versions
  (by E. J. Gallego Arias and Leo Stefanesco).

- Many improvements to both client and server plugin API, including a
  new client extension API by E. J. Gallego Arias and Bhakti Shah.

This version should be quite usable for a large majority of users, we
encourage you to test it!

Please see the detailed Changelog below. We have added to the README a
list of tools using `coq-lsp` that may be of your interest.

We'd like to thank to all the contributors and bug reporters for their
work. Contributions, bug reports, and feedback over `coq-lsp` are much
welcome, get in touch with us at GitHub or Zulip if you have questions
or comments.

`coq-lsp` is compatible with Coq 8.17-8.20. The `fcc` compiler has
been ported back to 8.11, for the benefit of some SerAPI users.

## Live Share support

If you are interesting in seeing VSCode Live Share support, please go
to this issue and click the "Thumbs Up" icon at end of the first
comment:

https://github.com/microsoft/live-share/issues/5046

This will help MS developers prioritizing support based on number of
demands. Please, _don't comment_ on the issue as this would create
load for MS developers, unless you have some feedback about the
technical implementation points

Full Changelog
==============

 - 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, #686,
   grants #681).
 - 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, #588)
 - hover plugins can now access the full document, this is convenient
   for many use cases (@ejgallego, #591)
 - fix hover position computation on the presence of Utf characters
   (@ejgallego, #597, thanks to Pierre Courtieu for the report and
   example, closes #594)
 - fix activation bug that prevented extension activation for `.mv`
   files, see discussion in the issues about the upstream policy
   (@ejgallego @r3m0t, #598, cc #596, reported by Théo Zimmerman)
 - require VSCode >= 1.82 in package.json . Our VSCode extension uses
   `vscode-languageclient` 9 which imposes this. (@ejgallego, #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, #600)
 - fix some cases where interrupted computations where memoized
   (@ejgallego, #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, #604)
 - support OCaml 5.1.x (@ejgallego, #606)
 - update progress indicator correctly on End Of File (@ejgallego,
   #605, fixes #445)
 - [plugins] New `astdump` plugin to dump AST of files into JSON and
   SEXP (@ejgallego, #607)
 - errors on save where not properly caught (@ejgallego, #608)
 - switch default of `goal_after_tactic` to `true` (@Alizter,
   @ejgallego, cc: #614)
 - error recovery: Recognize `Defined` and `Admitted` in lex recovery
   (@ejgallego, #616)
 - completion: correctly understand UTF-16 code points on completion
   request (Léo Stefanesco, #613, fixes #531)
 - don't trigger the goals window in general markdown buffer
   (@ejgallego, #625, reported by Théo Zimmerman)
 - allow not to postpone full document requests (#626, @ejgallego)
 - new configuration value `check_only_on_request` which will delay
   checking the document until a request has been made (#629, cc: #24,
   @ejgallego)
 - fix typo on package.json configuration section (@ejgallego, #645)
 - be more resilient with invalid _CoqProject files (@ejgallego, #646)
 - support for Coq 8.16 has been abandoned due to lack of dev
   resources (@ejgallego, #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, #650)
 - depend on `memprof-limits` on OCaml 4.x (@ejgallego, #660)
 - bump minimal OCaml version to 4.12 due to `memprof-limits`
   (@ejgallego, #660)
 - monitor all Coq-level calls under an interruption token
   (@ejgallego, #661)
 - interpret require thru our own custom execution env-aware path
   (@bhaktishh, @ejgallego, #642, #643, #644)
 - new `coq-lsp.plugin.goaldump` plugin, as an example on how to dump
   goals from a document (@ejgallego @gbdrt, #619)
 - new trim command (both in the server and in VSCode) to liberate
   space used in the cache (@ejgallego, #662, fixes #367 cc: #253 #236
   #348)
 - fix Coq performance view display (@ejgallego, #663, regression in
   #513)
 - allow more than one input position in `selectionRange` LSP call
   (@ejgallego, #667, fixes #663)
 - new VSCode commands to allow to move one sentence backwards /
   forward, this is particularly useful when combined with lazy
   checking mode (@ejgallego, #671, fixes #263, fixes #580)
 - VSCode commands `coq-lsp.sentenceNext` / `coq-lsp.sentencePrevious`
   are now bound by default to `Alt + N` / `Alt + P` keybindings
   (@ejgallego, #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, #670)
 - include range of full sentence in error diagnostic extra data
   (@ejgallego, #670 , thanks to @driverag22 for the idea, cc: #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, #675)
 - new public VSCode extension API so other extensions can perform
   actions when the user request the goals (@ejgallego, @bhaktishh,
   #672, fixes #538)
 - Support Visual Studio Live Share URIs better (`vsls://`), in
   particular don't try to display goals if the URI is VSLS one
   (@ejgallego, #676)
 - New `InjectRequire` plugin API for plugins to be able to instrument
   the default import list of files (@ejgallego @corwin-of-amber,
   #679)
 - Add `--max_errors=n` option to `fcc`, this way users can set
   `--max_errors=0` to imitate `coqc` behavior (@ejgallego, #680)
 - Fix `fcc` exit status when checking terminates with fatal errors
   (@ejgallego, @Alizter, #680)
 - Fix install to OPAM switches from `main` branch (@ejgallego, #683,
   fixes #682, cc #479 #488, thanks to @Hazardouspeach for the report)
 - New `--int_backend={Coq,Mp}` command line parameter to select the
   interruption method for Coq (@ejgallego, #684)
 - Update `package-lock.json` for latest bugfixes (@ejgallego, #687)
 - Update Nix flake enviroment (@Alizter, #684 #688)
 - Update `prettier` (@Alizter @ejgallego, #684 #688)
 - Store original performance data in the cache, so we now display the
   original timing and memory data even for cached commands (@ejgallego, #693)
 - Fix type errors in the Performance Data Notifications (@ejgallego,
   @Alizter, #689, #693)
 - Send performance performance data for the full document
   (@ejgallego, @Alizter, #689, #693)
 - Better types `coq/perfData` call (@ejgallego @Alizter, #689)
 - New server option to enable / disable `coq/perfData` (@ejgallego, #689)
 - New client option to enable / disable `coq/perfData` (@ejgallego, #717)
 - The `coq-lsp.document` VSCode command will now display the returned
   JSON data in a new editor (@ejgallego, #701)
 - Update server settings on the fly when tweaking them in VSCode.
   Implement `workspace/didChangeConfiguration` (@ejgallego, #702)
 - [Coq API] Add functions to retrieve list of declarations done in
   .vo files (@ejgallego, @eytans, #704)
 - New `petanque` API to interact directly with Coq's proof
   engine. (@ejgallego, @gbdrt, Laetitia Teodorescu #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, #705)
 - New `pet-server.exe` TCP server for keep-alive sessions (@gbdrt,
   #697)
 - Always dispose UI elements. This should improve some strange
   behaviors on extension restart (@ejgallego, #708)
 - 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, #709)
 - JSON-RPC library now supports all kind of incoming messages
   (@ejgallego, #713)
 - 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, #717)
 - Have VSCode wait for full LSP client shutdown on server
   restart. This fixes some bugs on extension restart (finally!)
   (@ejgallego, #719)
 - Center the view if cursor goes out of scope in
   `sentenceNext/sentencePrevious` (@ejgallego, #718)
 - Switch Flèche range encoding to protocol native, this means UTF-16
   code points for now (Léo Stefanesco, @ejgallego, #624, fixes #620,
   #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, #722, #725)
 - `fcc`: new option `--diags_level` to control whether Coq's notice
   and info messages appear as diagnostics
 - Display the continous/on-request checking mode in the status bar,
   allow to change it by clicking on it (@ejgallego, #721)
 - Add an example of multiple workspaces (@ejgallego, @Blaisorblade,
   #611)
 - Don't show types of un-expanded goals. We should add an option for
   this, but we don't have the cycles (@ejgallego, #730, workarounds
   #525 #652)
 - Support for `.lv / .v.tex` TeX files with embedded Coq code
   (@ejgallego, #727)
 - Don't expand bullet goals at previous levels by default
   (@ejgallego, @Alizter, #731 cc #525)
 - [petanque] Return basic goal information after `run_tac`, so we
   avoid a `goals` round-trip for each tactic (@gbdrt, @ejgallego,
   #733)
 - [coq] Add support for reading glob files metadata (@ejgallego,
   #735)
 - [petanque] Return extra premise information: file name, position,
   raw_text, using the above support for reading .glob files
   (@ejgallego, #735)