Merge branch 'v8.17' into v8.16

CONTRIBUTING.md

@@ -280,20 +280,30 @@ The checklist for the release as of today is the following:
 - `dune release tag` for each `$coq_lsp_version+$coq_version`
 - `dune release` for each version that should to the main opam repos
 - [optional] update pre-release packages to coq-opam-archive
-- [important] bump `version.ml` and `package.json` version string
+- [important] after the release, bump `version.ml` and `package.json` version string
+
+The above can be done with:
+```
+export COQLSPV=0.1.7
+git checkout main  && make                    && dune-release tag ${COQLSPV}
+git checkout v8.17 && git merge main  && make && dune-release tag ${COQLSPV}+8.17 && dune-release
+git checkout v8.16 && git merge v8.17 && make && dune-release tag ${COQLSPV}+8.16 && dune-release
+```
 
 ## Emacs
 
 You should be able to use `coq-lsp` with
-[eglot](https://joaotavora.github.io/eglot/).
+[eglot](https://joaotavora.github.io/eglot/) or [lsp-mode](https://github.com/emacs-lsp/lsp-mode)
 
 Emacs support is a goal of `coq-lsp`, so if you find any trouble using
 `eglot` or `lsp-mode` with `coq-lsp`, please don't hesitate to open an
-issue.
+issue. See `coq-lsp` README for more notes on Emacs support.
 
 ## VIM
 
 You should be able to use `coq-lsp` with VIM.
 
 VIM support is a goal of `coq-lsp`, so if you find any trouble using
 `coq-lsp` with VIM, please don't hesitate to open an issue.
+
+See `coq-lsp` README for more notes on VIM support.

editor/code/CHANGELOG.md

@@ -1,4 +1,24 @@
-# coq-lsp 0.1.5: Peek
+# coq-lsp 0.1.7: Just-in-time
+-----------------------------
+
+- Enable web extension support (worker server will happen in next release)
+- Improvements and clenaups on hover display, in particular we don't
+  print repeated `Notation` strings.
+- Fix bug that prevented "Goal after tactic" from working properly.
+- Fix "Error message browser becomes non-visible when there are many
+  goals" by using a fixed-position separated error display.
+- Display the list of pending obligations in info panel.
+- Preliminary panel to display document performance data.
+- Fix keybinding for the "Show Goals at Point" command
+- Hook coq-lsp to ViZX extension
+- Warnings settings from `_CoqProject` files are now applied
+- Limit the number of messages displayed in the goal window to 101,
+  as to workaround slow render of Coq's pretty printing format. This
+  is an issue for example in Search where we can get thousand of
+  results. We also speed up the rendering a bit by not hashing twice,
+  and fix a parameter-passing bug in the React setup.
+
+# coq-lsp 0.1.6: Peek
 ----------------------
 
 - The information / goal view now uses a new layout-aware printer; the

editor/code/README.md

@@ -6,7 +6,8 @@ server](https://github.com/ejgallego/coq-lsp).
 
 The server provides many nice features such as incremental checking,
 advanced error recovery, document information, ... See the server
-documentation for more information.
+documentation at the project page for more information and full
+changelog.
 
 ## Features
 
@@ -17,6 +18,7 @@ client by Microsoft, with 2 main addons:
   errors at point. It does also support client-side rendering.  By
   default, Cmd-Enter and mouse click will enable the panel for the
   current point.
+
 - document checking progress, using the right lane decoration.
 
 See the extension configuration options for more information.
@@ -31,4 +33,3 @@ opam install coq-lsp
 
 The server should also appear in the Coq Platform, and likely by other
 channels.
-

etc/ContributionIdeas.md

@@ -43,7 +43,8 @@ like to:
 
 ## "Semantic" goal and document printing
 
-Based on the `coq-layout-engine` project.
+- Add support for the `coq-layout-engine` project.
+- Port the current pp printer code to React
 
 ## LaTeX and Markdown document support
 

etc/release_notes/v0.1.7.md

@@ -3,6 +3,10 @@ Hi folks,
 it's been a while, but we are happy to announce a new release of
 `coq-lsp`.
 
+Install for Coq 8.17 and Visual Studio Code is as easy as:
+
+$ opam install coq-lsp && code --install-extension ejgallego.coq-lsp
+
 The 0.1.7 release has been focused on refinement and bugfixes; we'd
 like to thank all the users and contributors for their feedback and
 work, and in particular Alex Sanchez-Stern who did a large amount of
@@ -32,6 +36,9 @@ This release also ships with some new features:
 
 - The UI for error display was improved by Tomás Díaz.
 
+- The goal panel now display information about open and solved
+  obligations.
+
 - `coq-lsp/VSCode` is now a web extension, and thus it will activate
   on `github.dev` and `vscode.dev`. The server has been refactored so
   it can run on the Browser context, full support is expected in the