[ANN] coq-lsp 0.1.9

[ejgallego]

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:

Extension support: coq-lsp

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)