[doc] Release notes for 0.1.8

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