From f277183fabfc67dd0a5ed0a2d12b784e2aed5b1e Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Fri, 7 Jul 2023 15:23:03 +0200 Subject: [PATCH 1/7] [doc] [client] Client Changelog + update on notes --- editor/code/CHANGELOG.md | 22 +++++++++++++++++++++- editor/code/README.md | 5 +++-- etc/release_notes/v0.1.7.md | 3 +++ 3 files changed, 27 insertions(+), 3 deletions(-) diff --git a/editor/code/CHANGELOG.md b/editor/code/CHANGELOG.md index 35b7e447..a199fe16 100644 --- a/editor/code/CHANGELOG.md +++ b/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 diff --git a/editor/code/README.md b/editor/code/README.md index cb2c7649..0ae2c8ff 100644 --- a/editor/code/README.md +++ b/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. - diff --git a/etc/release_notes/v0.1.7.md b/etc/release_notes/v0.1.7.md index 25448d0c..8b16850f 100644 --- a/etc/release_notes/v0.1.7.md +++ b/etc/release_notes/v0.1.7.md @@ -32,6 +32,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 From 18671eff97e9916c90ce7aa91a7277c761bfc11d Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Fri, 7 Jul 2023 15:34:42 +0200 Subject: [PATCH 2/7] [doc] [contributing] Some improvs on release documentation. --- CONTRIBUTING.md | 16 +++++++++++++--- 1 file changed, 13 insertions(+), 3 deletions(-) diff --git a/CONTRIBUTING.md b/CONTRIBUTING.md index 133b3c1f..b528c2bd 100644 --- a/CONTRIBUTING.md +++ b/CONTRIBUTING.md @@ -280,16 +280,24 @@ 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 && make && git merge main && dune release tag ${COQLSPV}+8.17 && dune release +git checkout v8.16 && make && git merge v8.17 && 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 @@ -297,3 +305,5 @@ 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. From 2fc485792346ace19e069bc614a3e706fe39fd92 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Fri, 7 Jul 2023 15:36:30 +0200 Subject: [PATCH 3/7] [doc] [contributing] Fix typo. --- CONTRIBUTING.md | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/CONTRIBUTING.md b/CONTRIBUTING.md index b528c2bd..cc2df88b 100644 --- a/CONTRIBUTING.md +++ b/CONTRIBUTING.md @@ -285,9 +285,9 @@ The checklist for the release as of today is the following: The above can be done with: ``` export COQLSPV=0.1.7 -git checkout main && make && dune release tag $COQLSPV -git checkout v8.17 && make && git merge main && dune release tag ${COQLSPV}+8.17 && dune release -git checkout v8.16 && make && git merge v8.17 && dune release tag ${COQLSPV}+8.16 && dune release +git checkout main && make && dune-release tag ${COQLSPV} +git checkout v8.17 && make && git merge main && dune-release tag ${COQLSPV}+8.17 && dune release +git checkout v8.16 && make && git merge v8.17 && dune-release tag ${COQLSPV}+8.16 && dune release ``` ## Emacs From fe3a551162fec9f2db366e23200102d23a2486c8 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Fri, 7 Jul 2023 15:37:35 +0200 Subject: [PATCH 4/7] [doc] [contributing] Fix more typos. --- CONTRIBUTING.md | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/CONTRIBUTING.md b/CONTRIBUTING.md index cc2df88b..3cffc37a 100644 --- a/CONTRIBUTING.md +++ b/CONTRIBUTING.md @@ -286,8 +286,8 @@ The above can be done with: ``` export COQLSPV=0.1.7 git checkout main && make && dune-release tag ${COQLSPV} -git checkout v8.17 && make && git merge main && dune-release tag ${COQLSPV}+8.17 && dune release -git checkout v8.16 && make && git merge v8.17 && dune-release tag ${COQLSPV}+8.16 && dune release +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 From 991ecc50e0ac1740ba29408c1cb69e206f9985ad Mon Sep 17 00:00:00 2001 From: "dependabot[bot]" <49699333+dependabot[bot]@users.noreply.github.com> Date: Fri, 7 Jul 2023 13:39:12 +0000 Subject: [PATCH 5/7] Bump semver from 7.3.8 to 7.5.3 in /editor/code Bumps [semver](https://github.com/npm/node-semver) from 7.3.8 to 7.5.3. - [Release notes](https://github.com/npm/node-semver/releases) - [Changelog](https://github.com/npm/node-semver/blob/main/CHANGELOG.md) - [Commits](https://github.com/npm/node-semver/compare/v7.3.8...v7.5.3) --- updated-dependencies: - dependency-name: semver dependency-type: indirect ... Signed-off-by: dependabot[bot] --- editor/code/package-lock.json | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) diff --git a/editor/code/package-lock.json b/editor/code/package-lock.json index 66103517..e4fae0a3 100644 --- a/editor/code/package-lock.json +++ b/editor/code/package-lock.json @@ -671,9 +671,9 @@ } }, "node_modules/semver": { - "version": "7.3.8", - "resolved": "https://registry.npmjs.org/semver/-/semver-7.3.8.tgz", - "integrity": "sha512-NB1ctGL5rlHrPJtFDVIVzTyQylMLu9N9VICA6HSFJo8MCGVTMW6gfpicwKmmK/dAjTOrqu5l63JJOpDSrAis3A==", + "version": "7.5.3", + "resolved": "https://registry.npmjs.org/semver/-/semver-7.5.3.tgz", + "integrity": "sha512-QBlUtyVk/5EeHbi7X0fw6liDZc7BBmEaSYn01fMU1OUYbf6GPsbTtd8WmnqbI20SeycoHSeiybkE/q1Q+qlThQ==", "dependencies": { "lru-cache": "^6.0.0" }, @@ -1156,9 +1156,9 @@ } }, "semver": { - "version": "7.3.8", - "resolved": "https://registry.npmjs.org/semver/-/semver-7.3.8.tgz", - "integrity": "sha512-NB1ctGL5rlHrPJtFDVIVzTyQylMLu9N9VICA6HSFJo8MCGVTMW6gfpicwKmmK/dAjTOrqu5l63JJOpDSrAis3A==", + "version": "7.5.3", + "resolved": "https://registry.npmjs.org/semver/-/semver-7.5.3.tgz", + "integrity": "sha512-QBlUtyVk/5EeHbi7X0fw6liDZc7BBmEaSYn01fMU1OUYbf6GPsbTtd8WmnqbI20SeycoHSeiybkE/q1Q+qlThQ==", "requires": { "lru-cache": "^6.0.0" } From 09c1f79cd4f8410f036bc6b13fa1b3bc6baa29fa Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Fri, 7 Jul 2023 15:47:13 +0200 Subject: [PATCH 6/7] [doc] [release notes] Nit --- etc/release_notes/v0.1.7.md | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/etc/release_notes/v0.1.7.md b/etc/release_notes/v0.1.7.md index 8b16850f..77e5c093 100644 --- a/etc/release_notes/v0.1.7.md +++ b/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 From 259b7bc11eced6a07b0f969513159ca3c6da9dbb Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Fri, 7 Jul 2023 15:51:32 +0200 Subject: [PATCH 7/7] [doc] [contribution ideas] Add TODO for Pp print performance --- etc/ContributionIdeas.md | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/etc/ContributionIdeas.md b/etc/ContributionIdeas.md index 19e50f85..135c1904 100644 --- a/etc/ContributionIdeas.md +++ b/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