[fcc] Add --no_vo option, turn .vo file saving into a plugin.
#650
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
ejgallego
added
kind: enhancement
ejgallego
added a commit
to ejgallego/opam-repository
that referenced
this pull request
May 31, 2024
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)
ejgallego
added a commit
to ejgallego/opam-repository
that referenced
this pull request
May 31, 2024
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)
ejgallego
added a commit
to ejgallego/opam-repository
that referenced
this pull request
May 31, 2024
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)
ejgallego
added a commit
to ejgallego/opam-repository
that referenced
this pull request
May 31, 2024
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)
ejgallego
added a commit
to ejgallego/opam-repository
that referenced
this pull request
May 31, 2024
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)
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
No description provided.