Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
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)
- Loading branch information
