[debug windows ci problem]

.github/workflows/build.yml

@@ -24,18 +24,6 @@ jobs:
     strategy:
       matrix:
         include:
-          - os: ubuntu-latest
-            ocaml: 4.14.x
-          - os: ubuntu-latest
-            ocaml: 4.13.x
-          - os: ubuntu-latest
-            ocaml: 4.12.x
-          - os: ubuntu-latest
-            ocaml: 4.11.x
-          - os: ubuntu-latest
-            ocaml: 5.0.x
-          - os: macos-latest
-            ocaml: 4.14.x
           - name: Windows Latest
             ocaml: 4.14
             os: windows-latest
@@ -50,6 +38,11 @@ jobs:
         with:
           submodules: recursive
 
+      - name: Setup tmate session
+        uses: mxschmitt/action-tmate@v3
+        with:
+          detached: true
+
       - name: 🐫 Setup OCaml
         uses: ocaml/setup-ocaml@v2
         with:
@@ -59,15 +52,16 @@ jobs:
       - name: 🐫🐪🐫 Get dependencies
         run: opam exec -- make opam-deps
 
+      - name: Configure coq-lsp natively with Windows paths
+        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:

Makefile

@@ -47,9 +47,23 @@ build-all: coq_boot
 
 # We set -libdir due to a Coq bug on win32, see https://github.com/coq/coq/pull/17289
 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

coq/workspace.ml

@@ -159,6 +159,12 @@ let pp_load_path fmt
     (Names.DirPath.to_string coq_path)
     unix_path
 
+let pp_as fmt (d, dl) =
+  Format.fprintf fmt "(%s, %a)" d Format.(pp_print_list pp_print_string) dl
+
+let pp_ap fmt (dl, d) =
+  Format.fprintf fmt "(%a, %s)" Format.(pp_print_list pp_print_string) dl d
+
 let describe { coqlib; kind; vo_load_path; ml_include_path; require_libs; _ } =
   let require_msg =
     String.concat " " (List.map (fun (s, _, _) -> s) require_libs)
@@ -172,14 +178,46 @@ let describe { coqlib; kind; vo_load_path; ml_include_path; require_libs; _ } =
       Format.(pp_print_list pp_print_string)
       ml_include_path
   in
-  ( Format.asprintf
+  let base =
+    Format.asprintf
       "@[Configuration loaded from %s@\n\
       \ - coqlib is at: %s@\n\
       \ - Modules [%s] will be loaded by default@\n\
       \ - %d Coq path directory bindings in scope; %d Coq plugin directory \
        bindings in scope@]"
       kind coqlib require_msg n_vo n_ml
-  , extra )
+  in
+  let c11 = System.all_subdirs ~unix_path:coqlib in
+  let c12 = System.all_subdirs ~unix_path:(Filename.concat coqlib "..") in
+  let c13 =
+    System.all_subdirs ~unix_path:Filename.(concat (concat coqlib "..") "..")
+  in
+  let c11' = System.all_subdirs ~unix_path:coqlib in
+  let c12' = System.all_subdirs ~unix_path:(coqlib ^ "/..") in
+  let c13' = System.all_subdirs ~unix_path:(coqlib ^ "/../..") in
+  let c2 = Sys.readdir coqlib in
+  let c3 = System.all_in_path c11 "Prelude.vo" in
+  let base =
+    Format.asprintf
+      "l1:%a@\nl2:%a@\nl3:%a@\nl1':%a@\nl2':%a@\nl3':%a@\n%a@\n%a@\n@\n%s"
+      Format.(pp_print_list pp_as)
+      c11
+      Format.(pp_print_list pp_as)
+      c12
+      Format.(pp_print_list pp_as)
+      c13
+      Format.(pp_print_list pp_as)
+      c11'
+      Format.(pp_print_list pp_as)
+      c12'
+      Format.(pp_print_list pp_as)
+      c13'
+      Format.(pp_print_list pp_print_string)
+      (Array.to_list c2)
+      Format.(pp_print_list pp_ap)
+      c3 base
+  in
+  (base, extra)
 
 (* Require a set of libraries *)
 let load_objs libs =

test/server/package.json

@@ -13,6 +13,6 @@
     "vscode-uri": "^3.0.7"
   },
   "scripts": {
-    "test": "jest --detectOpenHandles"
+    "test": "jest --detectOpenHandles --silent false"
   }
 }

test/server/src/Check.test.ts

@@ -24,6 +24,15 @@ test("Open file with wrong URI", async () => {
 
   await languageServer.initialize(initializeParameters);
 
+  languageServer.onNotification(Protocol.LogTraceNotification.type, (e) => {
+    console.log(e.message);
+    if (e.verbose) console.log(e.verbose);
+  });
+
+  languageServer.onNotification(Protocol.LogMessageNotification.type, (e) => {
+    console.log(e.message);
+  });
+
   let textDocument = Types.TextDocumentItem.create(
     "wrong_file.v",
     "coq",
@@ -37,6 +46,7 @@ test("Open file with wrong URI", async () => {
       textDocument,
     }
   );
+
   let p = new Promise<Protocol.PublishDiagnosticsParams>((resolve) => {
     languageServer.onNotification(
       Protocol.PublishDiagnosticsNotification.type,