Merge branch 'v8.18' into v8.17

.github/workflows/build.yml

@@ -4,12 +4,14 @@ on:
   push:
     branches:
       - main
+      - v8.18
       - v8.17
       - v8.16
       - v8.15
   pull_request:
     branches:
       - main
+      - v8.18
       - v8.17
       - v8.16
       - v8.15
@@ -59,15 +61,17 @@ jobs:
       - name: 🐫🐪🐫 Get dependencies
         run: opam exec -- make opam-deps
 
+      - name: 🐛 Test coq-lsp
+        if: matrix.os == 'windows-latest'
+        run: opam exec -- make winconfig
+
       - name: 🧱 Build coq-lsp
         run: opam exec -- make build
 
       - name: 🐛 Test coq-lsp
-        if: matrix.os != 'windows-latest'
         run: opam exec -- make test
 
       - name: 🐛 Test fcc
-        if: matrix.os != 'windows-latest'
         run: opam exec -- make test-compiler
 
   build-nix:
@@ -102,9 +106,9 @@ jobs:
       - name: 🚀 Setup node
         uses: actions/setup-node@v3
         with:
-          node-version: 16
+          node-version: 18
       - run: npm ci
-      - run: npx --yes vsce ls
+      - run: npx --yes @vscode/vsce ls
 
   nix-flake-check:
     name: Nix Flake Check

CHANGES.md

@@ -1,3 +1,17 @@
+# coq-lsp 0.1.8: Dot / Bracket
+------------------------------
+
+ - 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)
+
 # coq-lsp 0.1.7: Just-in-time
 -----------------------------
 

CONTRIBUTING.md

@@ -125,6 +125,19 @@ nix build .?submodules=1
 This currently only applies to building the default package (`coq-lsp`), which is
 the server. Clients don't have specific submodules as of yet.
 
+When the flake is out-of-date, for instance when a new version of ocamlformat
+is out, you can update the flake inputs with:
+```sh
+nix flake update
+```
+
+You can also add the `dev` version build to your flake as:
+```nix
+inputs.coq-lsp = { type = "git"; url = "https://github.com/ejgallego/coq-lsp.git"; submodules = true; };
+...
+coq-lsp.packages.${system}.default
+```
+
 ### Code organization
 
 The `coq-lsp` server consists of several components, we present them bottom-up

Makefile

@@ -26,8 +26,8 @@ test: build test/server/node_modules
 	cd test/server && npm test
 
 .PHONY: test-compiler
-test-compiler: build
-	OCAMLPATH=_build/install/default/lib:$$OCAMLPATH FCC_TEST=true dune runtest
+test-compiler:
+	dune runtest
 
 .PHONY: fmt format
 fmt format:
@@ -41,19 +41,35 @@ watch: coq_boot
 build-all: coq_boot
 	dune build $(DUNEOPT) @all
 
-# We set -libdir due to a Coq bug on win32, see https://github.com/coq/coq/pull/17289
+# We set -libdir due to a Coq bug on win32, see
+# https://github.com/coq/coq/pull/17289 , this can be removed once we
+# drop support for Coq 8.16
 vendor/coq/config/coq_config.ml:
-	cd vendor/coq \
-	&& ./configure -no-ask -prefix $(shell pwd)/_build/install/default/ \
-	        -libdir $(shell pwd)/_build/install/default/lib/coq \
+	EPATH=$(shell pwd) \
+	&& cd vendor/coq \
+	&& ./configure -no-ask -prefix "$$EPATH/_build/install/default/" \
+	        -libdir "$$EPATH/_build/install/default/lib/coq" \
+		-native-compiler no \
+	&& cp theories/dune.disabled theories/dune \
+	&& cp user-contrib/Ltac2/dune.disabled user-contrib/Ltac2/dune
+
+# We set windows parameters a bit better, note the need to use forward
+# slashed (cygpath -m) due to escaping :( , a conversion to `-w` is
+# welcomed if someones has time for this
+.PHONY: winconfig
+winconfig:
+	EPATH=$(shell cygpath -am .) \
+	&& cd vendor/coq \
+	&& ./configure -no-ask -prefix "$$EPATH\\_build\\install\\default\\" \
+	        -libdir "$$EPATH\\_build\\install\\default\\lib\\coq\\" \
 		-native-compiler no \
 	&& cp theories/dune.disabled theories/dune \
 	&& cp user-contrib/Ltac2/dune.disabled user-contrib/Ltac2/dune
 
 .PHONY: coq_boot
 coq_boot:
 # We do nothing for release versions
-# coq_boot: coq/config/coq_config.ml
+# coq_boot: vendor/coq/config/coq_config.ml
 
 .PHONY: clean
 clean:

README.md

@@ -8,11 +8,15 @@ Studio Code](https://code.visualstudio.com/) extension for the [Coq Proof
 Assistant](https://coq.inria.fr). Experimental support for [Vim](#vim) and
 [Neovim](#neovim) is also available in their own projects.
 
-Install for Visual Studio is as easy as:
+**[Install: 🐧 Linux / 🍎 macOs]**:
 ```
 $ opam install coq-lsp && code --install-extension ejgallego.coq-lsp
 ```
 
+**[Install: 🪟 Windows ]:**
+
+> see the [instructions](#-server); we will provide an `.exe` installer very soon
+
 Key [features](#Features) of `coq-lsp` are continuous and incremental document
 checking, advanced error recovery, markdown support, positional goals and
 information panel, performance data, and more.
@@ -54,6 +58,7 @@ and web native usage, providing quite a few extra features from vanilla Coq.
   - [🦄 Emacs](#-emacs)
   - [✅ Vim](#-vim)
   - [🩱 Neovim](#-neovim)
+  - [🐍 Python](#-python)
 - [🗣️ Discussion Channel](#️-discussion-channel)
 - [☎ Weekly Calls](#-weekly-calls)
 - [❓FAQ](#faq)
@@ -213,13 +218,15 @@ SerAPI](etc/SerAPI.md) document.
 ## 🛠️ Installation
 
 In order to use `coq-lsp` you'll need to install [**both**](etc/FAQ.md)
-`coq-lsp` and a suitable client. We recommend the Visual Studio Code Extension
-as client.
+`coq-lsp` and a suitable LSP client that understands `coq-lsp` extensions. The
+recommended client is the Visual Studio Code Extension, but we aim to fully
+support other clients officially and will do so once their authors consider them
+ready.
 
 ### 🏘️ Supported Coq Versions
 
-`coq-lsp` supports Coq 8.15, 8.16, Coq 8.17, and Coq's `master` branch. Code for
-each Coq version can be found in the corresponding branch.
+`coq-lsp` supports Coq 8.15, 8.16, Coq 8.17, Coq 8.18, and Coq's `master`
+branch. Code for each Coq version can be found in the corresponding branch.
 
 We recommended a minimum of Coq 8.17, due to better test coverage for that
 version. For 8.16, we recommend users to install the custom Coq tree as detailed
@@ -229,32 +236,29 @@ Support for older Coq versions is possible; it is possible to make `coq-lsp`
 work with Coq back to Coq 8.10/8.9. If you are interested in making that happen
 don't hesitate to get in touch with us.
 
+Note that this section covers user installs, if you would like to contribute to
+`coq-lsp` and build a development version, please check our [contributing
+guide](./CONTRIBUTING.md)
+
 ### 🏓 Server
 
-- **opam**:
+- **opam** (OSX/Linux):
   ```
   opam install coq-lsp
   ```
 - **Nix**:
-   - In nixpkgs: [#213397](https://github.com/NixOS/nixpkgs/pull/213397)
-   - In your flake:
-   ```nix
-   inputs.coq-lsp = { type = "git"; url = "https://github.com/ejgallego/coq-lsp.git"; submodules = true; };
-   ...
-   coq-lsp.packages.${system}.default
-   ```
-- **Windows**: To install `coq-lsp` on windows, we recommend you use a cygwin
-  build, such as the [one described
-  here](https://github.com/coq/platform/blob/main/doc/README_Windows.md#installation-by-compiling-from-sources-using-opam-on-cygwin), tho
-  any OCaml env where Coq can be built should work.
-  - build `coq-lsp` from source (branch `v8.16`, which will become 0.1.7)
-  - Set the path to `coq-lsp.exe` binary in VS Code settings
-  - Set the `--ocamlpath=c:\$path_to_opam\lib` argument in VS Code settings if
-    you get a findlib error. The Coq Platform ships with an un-configured
-    binary. Note, the path should be unquoted
-  - If the binary doesn't work, try to run it from the file explorer; if you get
-    a `.dll` error you'll need to copy that dll (often `libgmp-10.dll`) to the
-    `C:\Windows` folder for `coq-lsp` to work.
+  - In nixpkgs: [coqPackages.coq-lsp](https://github.com/NixOS/nixpkgs/tree/master/pkgs/development/coq-modules/coq-lsp)
+  - An example of a `flake` that uses `coq-lsp` in a development environment is here
+     https://github.com/HoTT/Coq-HoTT/blob/master/flake.nix .
+- **Windows**: To install `coq-lsp` on windows, you need to build the Coq Platform:
+  - Download and uncompress the Platform Script: https://github.com/coq/platform/archive/refs/tags/2023.03.0.zip
+  - From a shell, execute `./coq_platform_make_windows.bat`
+  - Select `C:\cp_817` as the install path, select the packages you want
+  - Run `C:\cp_817\Cygwin.bat`
+  - Run `opam install coq-lsp`
+  - Run `cp /cygdrive/c/cp_817/usr/x86_64-w64-mingw32/sys-root/mingw/bin/libgmp-10.dll /home/User/.opam/CP.2023.03.0~8.17~2023.08/bin`
+  - In VSCode native, you can now set the `Coq-lsp: Path` setting to `C:\cp_817\home\User\.opam\CP.2023.03.0~8.17~2023.08\bin\coq-lsp.exe`
+  - Things should work !
 - **Coq Platform** (coming soon)
   - See the [bug tracking coq-lsp inclusion](https://github.com/coq/platform/issues/319)
 - [Do it yourself!](#server-1)
@@ -296,6 +300,11 @@ programs.vscode = {
 
 - Experimental client by Jaehwang Jung: https://github.com/tomtomjhj/coq-lsp.nvim
 
+### 🐍 Python
+
+- Interact programmatically with Coq files by using the [Python `coq-lsp` client](https://github.com/sr-lab/coq-lsp-pyclient)
+  by Pedro Carrott and Nuno Saavedra.
+
 ## 🗣️ Discussion Channel
 
 `coq-lsp` discussion channel it at [Coq's

controller/lsp_core.ml

@@ -35,11 +35,21 @@ module LIO = Lsp.Io
 module LSP = Lsp.Base
 
 module Helpers = struct
-  (* helpers; fix to have better errors on wrong protocol code *)
+  (* XXX helpers; fix to have better errors on wrong protocol code *)
+  (* Also note that rely sometimes on "subtyping" of fields, that's something to
+     think about better and fix, see #547 *)
   let get_uri params =
     let document =
-      field "textDocument" params
-      |> Lsp.Doc.TextDocumentIdentifier.of_yojson |> Result.get_ok
+      match
+        field "textDocument" params |> Lsp.Doc.TextDocumentIdentifier.of_yojson
+      with
+      | Ok uri -> uri
+      | Error err ->
+        (* ppx_deriving_yojson error messages leave a lot to be desired *)
+        let message = Format.asprintf "json parsing failed: %s" err in
+        LIO.logMessage ~lvl:1 ~message;
+        (* XXX Fixme *)
+        CErrors.user_err (Pp.str "failed to parse uri")
     in
     let Lsp.Doc.TextDocumentIdentifier.{ uri } = document in
     uri

coq/workspace.ml

@@ -34,16 +34,18 @@ module Warning : sig
   type t
 
   val make : string -> t
-  val apply : t -> unit
+
+  (** Adds new warnings to the list of current warnings *)
+  val apply : t list -> unit
 end = struct
   type t = string
 
   let make x = x
-  let to_string x = x
 
   let apply w =
-    let warn = CWarnings.get_flags () in
-    CWarnings.set_flags (warn ^ to_string w)
+    let old_warn = CWarnings.get_flags () in
+    let new_warn = String.concat "," w in
+    CWarnings.set_flags (old_warn ^ "," ^ new_warn)
 end
 
 type t =
@@ -236,7 +238,7 @@ let apply ~uri
     } =
   if debug then CDebug.set_flags "backtrace";
   Flags.apply flags;
-  List.iter Warning.apply warnings;
+  Warning.apply warnings;
   List.iter Mltop.add_ml_dir ml_include_path;
   findlib_init ~ml_include_path ~ocamlpath;
   List.iter Loadpath.add_vo_path vo_load_path;

coq/workspace.mli

@@ -26,7 +26,10 @@ module Warning : sig
   type t
 
   val make : string -> t
-  val apply : t -> unit
+
+  (** Adds new warnings to the list of current warnings, the Coq API here is a
+      bit tricky... *)
+  val apply : t list -> unit
 end
 
 type t = private

editor/code/.prettierrc

@@ -0,0 +1,6 @@
+{
+  "trailingComma": "es5",
+  "tabWidth": 2,
+  "semi": true,
+  "singleQuote": false
+}

editor/code/.vscodeignore

@@ -3,6 +3,7 @@
 .prettierignore
 .gitignore
 .vscode/
+flakeModule.nix
 
 # Source files
 **/*.ts
@@ -18,3 +19,4 @@ esbuild.mjs
 views/info/media/
 
 # Perf view
+views/perf/media/