From 16f0aa85b6c022a4b72d9e74cb8a7f5b05e4a4a7 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Tue, 27 Aug 2024 20:32:13 +0200 Subject: [PATCH 1/4] [vendor] Bump Coq. --- vendor/coq | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/vendor/coq b/vendor/coq index 75110785d..6a2431e6f 160000 --- a/vendor/coq +++ b/vendor/coq @@ -1 +1 @@ -Subproject commit 75110785d70290302a1a88d03d23d1618693006c +Subproject commit 6a2431e6fa1f4a0bbee6d98c3b709aca781061d5 From 2260f2da0bd3f70c48cafc57ba478cd1d7bca328 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Thu, 29 Aug 2024 15:02:36 +0200 Subject: [PATCH 2/4] [meta] Release 0.2.0 This was requested for an AI course, but I consider this like a 0.2.0 beta, so I suggest to announce 0.2.1 as the first "public" version in the 0.2 series. --- CHANGES.md | 4 ++-- CONTRIBUTING.md | 2 ++ editor/code/CHANGELOG.md | 32 ++++++++++++++++++++++++++++++++ editor/code/package.json | 2 +- fleche/version.ml | 2 +- 5 files changed, 38 insertions(+), 4 deletions(-) diff --git a/CHANGES.md b/CHANGES.md index 33a4e70bf..bcc7ad96a 100644 --- a/CHANGES.md +++ b/CHANGES.md @@ -1,5 +1,5 @@ -# unreleased ------------- +# coq-lsp 0.2.0: From Green to Blue +----------------------------------- - [deps] merge serlib into coq-lsp. This allow us to drop the SerAPI dependency, and will greatly easy the development of tools that diff --git a/CONTRIBUTING.md b/CONTRIBUTING.md index 4ddf2a7bf..e744829de 100644 --- a/CONTRIBUTING.md +++ b/CONTRIBUTING.md @@ -386,12 +386,14 @@ The checklist for the release as of today is the following: ### Client: - update the client changelog at `editor/code/CHANGELOG.md`, commit +- update the version number at `editor/code/package.json` - for the `main` branch: `dune release tag $coq_lsp_version` - check with `vsce ls` that the client contents are OK - `vsce publish` ### Server: +- update the version number at `fleche/version.ml` - sync branches for previous Coq versions, using `git merge`, test and push to CI. - `dune release tag` for each `$coq_lsp_version+$coq_version` - `dune release` for each version that should to the main opam repos diff --git a/editor/code/CHANGELOG.md b/editor/code/CHANGELOG.md index e07b95b57..a85e940ab 100644 --- a/editor/code/CHANGELOG.md +++ b/editor/code/CHANGELOG.md @@ -1,3 +1,35 @@ +# coq-lsp 0.2.0: From Green to Blue +----------------------------------- + + - [fleche] Preserve view hint across document changes. With this + change, we get local continuous checking mode when the view-port + heuristic is enabled (@ejgallego, #748) + - [vscode] Fix focus race when a Coq file is in column 2 (@ejgallego, + #755, cc: #722, #725) + - [hover] Show input howto for unicode characters on hover + (@ejgallego, Léo Stefanesco, #756) + - [lsp] [definition] Support for jump to definition across workspace + files. The location information is obtained from `.glob` files, so + it is often not perfect. (@ejgallego, #762, fixes #317) + - [lsp] [hover] Show full name and provenance of identifiers + (@ejgallego, #762) + - [lsp] [definition] Try also to resolve and locate module imports + (@ejgallego, #764) + - [code] Don't start server on extension activation, unless an editor + we own is active. We also auto-start the server if a document that + we own is opened later (@ejgallego, #758, fixes #750) + - [hover] New option `show_universes_on_hover` that will display + universe data on hover (@ejgallego, @SkySkimmer, #666) + - [hover] New plugin `unidiff` that will elaborate a summary of + universe data a file, in particular regarding universes added at + `Qed` time (@ejgallego, #773) + - [fleche] Support meta-command `Abort All` (@ejgallego, #774, fixes + #550) + - [lsp] [petanque] Allow acces to `petanque` protocol from the lsp + server (@ejgallego, #778) + + See server changelog for full server-side changes. + # coq-lsp 0.1.10: Hasta el 40 de Mayo _en effect_... ---------------------------------------------------- diff --git a/editor/code/package.json b/editor/code/package.json index a5278d669..9db5b6922 100644 --- a/editor/code/package.json +++ b/editor/code/package.json @@ -2,7 +2,7 @@ "name": "coq-lsp", "displayName": "Coq LSP", "description": "Coq LSP provides native vsCode support for checking Coq proof documents", - "version": "0.2.0-dev", + "version": "0.2.0", "contributors": [ "Emilio Jesús Gallego Arias ", "Ali Caglayan ", diff --git a/fleche/version.ml b/fleche/version.ml index 77bb0c523..93c568871 100644 --- a/fleche/version.ml +++ b/fleche/version.ml @@ -12,6 +12,6 @@ type t = string (************************************************************************) (* UPDATE VERSION HERE *) -let server = "0.2.0-dev" +let server = "0.2.0" (* UPDATE VERSION HERE *) (************************************************************************) From 7e3ce61011064535fde73b9f3f57f7a525058007 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Thu, 29 Aug 2024 15:20:04 +0200 Subject: [PATCH 3/4] [code] Update package-lock.json --- editor/code/package-lock.json | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/editor/code/package-lock.json b/editor/code/package-lock.json index aae84a0d9..ba496c85b 100644 --- a/editor/code/package-lock.json +++ b/editor/code/package-lock.json @@ -1,12 +1,12 @@ { "name": "coq-lsp", - "version": "0.2.0-dev", + "version": "0.2.0", "lockfileVersion": 3, "requires": true, "packages": { "": { "name": "coq-lsp", - "version": "0.2.0-dev", + "version": "0.2.0", "dependencies": { "@vscode/webview-ui-toolkit": "^1.2.2", "jquery": "^3.7.1", From 2d53d567ac5c8499e865b9f4a730bdba67ca127a Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Thu, 29 Aug 2024 15:22:23 +0200 Subject: [PATCH 4/4] [doc] Nits on release instructions --- CONTRIBUTING.md | 17 +++++++++++++---- 1 file changed, 13 insertions(+), 4 deletions(-) diff --git a/CONTRIBUTING.md b/CONTRIBUTING.md index e744829de..d49232c5d 100644 --- a/CONTRIBUTING.md +++ b/CONTRIBUTING.md @@ -383,22 +383,26 @@ README there for more details. The checklist for the release as of today is the following: +### Pre-release + +- update the version number at `editor/code/package.json`, do `npm i` +- update the version number at `fleche/version.ml` + ### Client: - update the client changelog at `editor/code/CHANGELOG.md`, commit -- update the version number at `editor/code/package.json` - for the `main` branch: `dune release tag $coq_lsp_version` +- build the extension with `npm run vscode:prepublish` - check with `vsce ls` that the client contents are OK - `vsce publish` +- upload vsix to OpenVSX marketplace ### Server: -- update the version number at `fleche/version.ml` - sync branches for previous Coq versions, using `git merge`, test and push to CI. - `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] after the release, bump `version.ml` and `package.json` version string +- [deprecated] update pre-release packages to coq-opam-archive The above can be done with: ``` @@ -410,6 +414,11 @@ git checkout v8.18 && git merge v8.19 && make && dune-release tag ${COQLSPV}+8. git checkout v8.17 && git merge v8.18 && make && dune-release tag ${COQLSPV}+8.17 && dune-release ``` +### After release + +- [important] bump `version.ml` and `editor/code/package.json` version + string to a `-dev` suffix + ## Emacs You should be able to use `coq-lsp` with