From 550a4a48d22d00c6173a1d991b4dc45e1fcf929f Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Wed, 25 Oct 2023 17:59:43 +0200 Subject: [PATCH] [code] Update client changelog. --- editor/code/CHANGELOG.md | 61 ++++++++++++++++++++++++++++++++++++++++ 1 file changed, 61 insertions(+) diff --git a/editor/code/CHANGELOG.md b/editor/code/CHANGELOG.md index a199fe16..b5eee4a5 100644 --- a/editor/code/CHANGELOG.md +++ b/editor/code/CHANGELOG.md @@ -1,3 +1,64 @@ +# coq-lsp 0.1.8: Trick-or-treat +------------------------------- + + - Update VSCode client dependencies, should bring some performance + improvements to goal pretty printing (@ejgallego, #530) + - Update goal display colors for light mode so they are actually + readable now. (@bhaktishh, #539, fixes #532) + - Added link to Python coq-lsp client by Pedro Carrot and Nuno + Saavedra (@Nfsaavedra, #536) + - Properly concatenate warnings from _CoqProject (@ejgallego, + reported by @mituharu, #541, fixes #540) + - Fix broken `coq/saveVo` and `coq/getDocument` requests due to a + parsing problem with extra fields in their requests (@ejgallego, + #547, reported by @Zimmi48) + - `fcc` now understands the `--coqlib`, `--coqcorelib`, + `--ocamlpath`, `-Q` and `-R` arguments (@ejgallego, #555) + - Describe findlib status in `Workspace.describe`, which is printed + in the output windows (@ejgallego, #556) + - `coq-lsp` plugin loader will now be strict in case of a plugin + failure, the previous loose behavior was more convenient for the + early releases, but it doesn't make sense now and made things + pretty hard to debug on the Windows installer (@ejgallego, #557) + - Add pointers to Windows installers (@ejgallego, #559) + - Recognize `Goal` and `Definition $id : ... .` as proof starters + (@ejgallego, #561, reported by @Zimmi48, fixes #548) + - Provide basic notation information on hover. This is intended for + people to build their own more refined notation feedback systems + (@ejgallego, #562) + - Hover request can now be extended by plugins (@ejgallego, #562) + - Updated LSP and JS client libs, notably to vscode-languageclient 9 + (@ejgallego, #565) + - Implement a LIFO document scheduler, this is heavier in the + background as more documents will be checked, but provides a few + usability improvements (@ejgallego, #566, fixes #563, reported by + Ali Caglayan) + - New lexical qed detection error recovery rule; this makes a very + large usability difference in practice when editing inside proofs. + (@ejgallego, #567, fixes #33) + - `coq-lsp` is now supported by the `coq-nix-toolbox` (@Zimmi48, + @CohenCyril, #572, via + https://github.com/coq-community/coq-nix-toolbox/pull/164 ) + - Support for `-rifrom` in `_CoqProject` and in command line + (`--rifrom`). Thanks to Lasse Blaauwbroek for the report. + (@ejgallego, #581, fixes #579) + - Export Query Goals API in VSCode client; this way other extensions + can implement their own commands that query Coq goals (@amblafont, + @ejgallego, #576, closes #558) + - New `pretac` field for preprocessing of goals with a tactic using + speculative execution, this is experimental for now (@amblafont, + @ejgallego, #573, helps with #558) + - Implement `textDocument/selectionRange` request, that will return + the range of the Coq sentence underlying the cursor. In VSCode, + this is triggered by the "Expand Selection" command. The + implementation is partial: we only take into account the first + position, and we only return a single range (Coq sentence) without + parents. (@ejgallego, #582) + - Be more robust to mixed-separator windows paths in workspace + detection (@ejgallego, #583, fixes #569) + - Adjust printing breaks in error and message panels (@ejgallego, + @Alizter, #586, fixes #457 , fixes #458 , fixes #571) + # coq-lsp 0.1.7: Just-in-time -----------------------------