From df88b71923761b902d3ef71e8426e2263338309a Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Wed, 25 Oct 2023 21:17:12 +0200 Subject: [PATCH] [doc] Release notes for 0.1.8 --- etc/release_notes/v0.1.8.md | 116 ++++++++++++++++++++++++++++++++++++ 1 file changed, 116 insertions(+) create mode 100644 etc/release_notes/v0.1.8.md diff --git a/etc/release_notes/v0.1.8.md b/etc/release_notes/v0.1.8.md new file mode 100644 index 00000000..7d17d2bd --- /dev/null +++ b/etc/release_notes/v0.1.8.md @@ -0,0 +1,116 @@ +Dear all, + +the 0.1.8 release of `coq-lsp` is out. + +This release brings important fixes and a few performance +improvements; in particular editing inside opaque proofs should behave +much better w.r.t. incremental engine; formatting inside the error and +message panels has been fixed, as well as display for light mode. + +On the protocol side, the LSP `textDocument/selectionRange` method is +now supported, allowing clients to easily select full Coq sentences. + +On the developer side, the Plugin API has seen some enhancements, +and hover plugins can now be declared. + +We consider `coq-lsp` to be in beta, but fully usable status for a +large majority of setups; we encourage Coq users to try `coq-lsp` now +and report back. Documentation seems to be the main hurdle new users +are facing, please let us know about problems in this area so we can +improve. + +We'd like to thank to all the contributors and bug reporters for their +work; contributions, bug reports, and feedback over `coq-lsp` are much +welcome, get in touch with us at GitHub or Zulip if you have +questions or comments. + +See `coq-lsp`'s README for detailed installation instructions. + +Also new in this release are the official windows installers, built on +the Coq platform. Nix support has also been generously improved by +contributors. + +Note that currently released Coq versions do contain critical bugs +w.r.t. async interruptions. We strongly recommend that you install a +fixed Coq version as outlined in `coq-lsp`'s README. Windows +installers are already built with a fixed Coq version. + +We take this opportunity to highlight a couple of recently released +projects built over `coq-lsp`: + +- WaterProof "2.0" [1], by the WaterProof team, an educational + mathematical environment for Coq + +- CoREACT Yade [2], by Ambroise Lafont, a graphical editor for + diagrammatic category theory proofs in Coq + +`coq-lsp` is compatible with Coq 8.16-8.18 and master. We will be +phasing out Coq 8.16 support soon due to lack of manpower, contact us +if you are interested in helping maintaining it. + +Detailed Changelog: +------------------- + + - 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) + +Kind regards, +Emilio + +[1] https://marketplace.visualstudio.com/items?itemName=waterproof-tue.waterproof +[2] https://marketplace.visualstudio.com/items?itemName=amblafont.coreact-yade