[ANN] coq-lsp 0.1.9

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:

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)
1 Like