-
Notifications
You must be signed in to change notification settings - Fork 35
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.
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
[vscode client] Export an API for ViZX integration #538
[vscode client] Export an API for ViZX integration #538
Comments
Let's start with some use cases? What kinds of extensions using the internals of this extension do you have in mind? |
For example, currently ViZX is hardwired into the coq-lsp code, which works for one extension but probably isn't scaleable or good practice if anyone wants to add more (which there seems to be interest in). Any kind of domain specific tool for Coq that doesn't necessarily make sense being integrated into the larger coq-lsp ecosystem because it's not general purpose enough, would probably want to interact with Coq, and sending requests to and from the server seems like a natural part of developing something like this. Something I'm working on currently needs to make a |
Are we talking about the coq-lsp server itself? Or specifically the VS Code extension? I understood the latter, but the former is completely agnostic to the client. |
I guess my idea is to make it easier to interact with the server too, via an extension API, instead of having to set up everything again with the server. |
Hi @bhaktishh , I think that what you propose makes total sense, I'll be happy to start experimenting with extension API. I think the only constraint I can see for now is that the extension hooks should be "pure" or "functional" as to work better with the server. For example I think the first API we could add is an API that allows the extension to insert a new collapsible tab for the goal view, and passing the context / goals info for that. |
I've taken the freedom to rename this issue to be about supporting |
This allows extensions to register without having to modify ours; it should subsume previous hooks for `VIXZ` and `VIZCAR` visualizers. There are many more improvements we can do to this API. Fixes #538
This allows extensions to register without having to modify ours; it should subsume previous hooks for `VIXZ` and `VIZCAR` visualizers. There are many more improvements we can do to this API. Fixes #538
This allows extensions to register without having to modify ours; it should subsume previous hooks for `VIXZ` and `VIZCAR` visualizers. There are many more improvements we can do to this API. Fixes #538
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)
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)
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)
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)
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)
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)
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)
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)
As documented here, it's possible for extensions to export an API for other extensions to use. I want to add an API for
coq-lsp
but I'm not sure what functions would make sense to include in the API. Are there thoughts on the same?The text was updated successfully, but these errors were encountered: