[version] Bump version, improve doc on release process.

We also include more detailed version info if available, for example
for pins.

CONTRIBUTING.md

@@ -99,6 +99,23 @@ Clients don't have specific submodules as of yet.
 
 `coq-lsp` is released using `dune-release tag` + `dune-release`.
 
+The checklist for the release as of today is:
+
+##### Client:
+
+- update the client changelog at `editor/code/CHANGELOG.md`, commit
+- for the `main` branch: `dune release tag $coq_lsp_version`
+- check with `vsce ls` that the client contents are OK
+- `vsce publish`
+
+##### Server:
+
+- 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 Coq repos
+- [optional] update pre-release packages to coq-opam-archive
+- [important] bump `version.ml` and `package.json` version string
+
 ### Code organization
 
 The `coq-lsp` server consists of several components, we present them bottom-up

controller/dune

@@ -1,7 +1,7 @@
 (library
  (name controller)
  (modules :standard \ coq_lsp)
- (libraries coq fleche lsp))
+ (libraries coq fleche lsp dune-build-info))
 
 (executable
  (name coq_lsp)

controller/lsp_core.ml

@@ -274,11 +274,21 @@ let log_workspace w =
   LIO.trace "workspace" "initialized" ~extra;
   LIO.logMessage ~lvl:3 ~message
 
+let version () =
+  match Build_info.V1.version () with
+  | None -> Format.asprintf "version: %s" Version.server
+  | Some bi ->
+    Format.asprintf "version %s, dev: %s" Version.server
+      (Build_info.V1.Version.to_string bi)
+
 let rec lsp_init_loop ic ofmt ~cmdline ~debug : Coq.Workspace.t =
   match LIO.read_request ic with
   | LSP.Message.Request { method_ = "initialize"; id; params } ->
     (* At this point logging is allowed per LSP spec *)
-    LIO.logMessage ~lvl:3 ~message:"Initializing server";
+    let message =
+      Format.asprintf "Initializing coq-lsp server %s" (version ())
+    in
+    LIO.logMessage ~lvl:3 ~message;
     let result, dir = Rq_init.do_initialize ~params in
     Rq.answer ~ofmt ~id (Result.ok result);
     LIO.logMessage ~lvl:3 ~message:"Server initialized";

controller/version.ml

@@ -12,6 +12,6 @@ type t = string
 
 (************************************************************************)
 (*                        UPDATE VERSION HERE                           *)
-let server = "0.1.5"
+let server = "0.1.6"
 (*                        UPDATE VERSION HERE                           *)
 (************************************************************************)

coq-lsp.opam

@@ -19,12 +19,13 @@ doc: "https://ejgallego.github.io/coq-lsp/"
 
 depends: [
   "ocaml"        { >= "4.11.0" }
-  "dune"         { >= "3.5.0"  }
+  "dune"         { >= "3.5.0"  } # This is 3.2.0 for non-composed builds
 
   # lsp dependencies
   "cmdliner"     { >= "1.1.0" }
   "yojson"       { >= "1.7.0" }
   "uri"          { >= "4.2.0" }
+  "dune-build-info" { >= "3.2.0" }
 
   # waterproof parser
   "menhir"       { >= "20220210" }

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.1.5",
+  "version": "0.1.6",
   "contributors": [
     "Emilio Jesús Gallego Arias <e@x80.org>",
     "Ali Caglayan <alizter@gmail.com>",