From c2302eaae55e0b54a241ad0b382c4998fc6c534c Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Thu, 23 Feb 2023 00:36:48 +0100 Subject: [PATCH 1/5] [test] Add logging for failing test on windows. --- .github/workflows/build.yml | 14 -------------- test/server/package.json | 2 +- test/server/src/Check.test.ts | 10 ++++++++++ 3 files changed, 11 insertions(+), 15 deletions(-) diff --git a/.github/workflows/build.yml b/.github/workflows/build.yml index bd96fd03..a1e73026 100644 --- a/.github/workflows/build.yml +++ b/.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 @@ -63,11 +51,9 @@ jobs: 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: diff --git a/test/server/package.json b/test/server/package.json index ae606502..88a0aaf5 100644 --- a/test/server/package.json +++ b/test/server/package.json @@ -13,6 +13,6 @@ "vscode-uri": "^3.0.7" }, "scripts": { - "test": "jest --detectOpenHandles" + "test": "jest --detectOpenHandles --silent false" } } diff --git a/test/server/src/Check.test.ts b/test/server/src/Check.test.ts index fcf0f5d4..52653345 100644 --- a/test/server/src/Check.test.ts +++ b/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((resolve) => { languageServer.onNotification( Protocol.PublishDiagnosticsNotification.type, From 2bf243b9c345fdc96d7836d75ad997d857b43719 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Fri, 24 Feb 2023 00:24:42 +0100 Subject: [PATCH 2/5] wip --- coq/workspace.ml | 24 +++++++++++++++++++++--- 1 file changed, 21 insertions(+), 3 deletions(-) diff --git a/coq/workspace.ml b/coq/workspace.ml index ffa96e2f..32011228 100644 --- a/coq/workspace.ml +++ b/coq/workspace.ml @@ -158,6 +158,11 @@ let pp_load_path fmt Format.fprintf fmt "Path %s ---> %s" (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 = @@ -172,14 +177,27 @@ 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 ) + kind coqlib require_msg n_vo n_ml 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 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@\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_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 = From 7a329a6bc0ef27eeb26d0837736dbffe8094e886 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Fri, 24 Feb 2023 01:00:04 +0100 Subject: [PATCH 3/5] tmp --- coq/workspace.ml | 48 ++++++++++++++++++++++++++++++++++-------------- 1 file changed, 34 insertions(+), 14 deletions(-) diff --git a/coq/workspace.ml b/coq/workspace.ml index 32011228..7d8a63f2 100644 --- a/coq/workspace.ml +++ b/coq/workspace.ml @@ -158,11 +158,12 @@ let pp_load_path fmt Format.fprintf fmt "Path %s ---> %s" (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 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 = @@ -184,20 +185,39 @@ let describe { coqlib; kind; vo_load_path; ml_include_path; require_libs; _ } = \ - 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 in + kind coqlib require_msg n_vo n_ml + 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 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@\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_print_string) (Array.to_list c2) - Format.(pp_print_list pp_ap) c3 - base in - ( base, extra ) + 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 = From 05d4e68cc686df798720701bf0a456913914f629 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Tue, 26 Sep 2023 16:06:18 +0200 Subject: [PATCH 4/5] tmate --- .github/workflows/build.yml | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/.github/workflows/build.yml b/.github/workflows/build.yml index a1e73026..416d999d 100644 --- a/.github/workflows/build.yml +++ b/.github/workflows/build.yml @@ -38,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: From 253c288e9b6eeb26a34968ffc1d781fa7470b49c Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Tue, 26 Sep 2023 16:51:59 +0200 Subject: [PATCH 5/5] Try better config method --- .github/workflows/build.yml | 3 +++ Makefile | 20 +++++++++++++++++--- 2 files changed, 20 insertions(+), 3 deletions(-) diff --git a/.github/workflows/build.yml b/.github/workflows/build.yml index 416d999d..99b86ffa 100644 --- a/.github/workflows/build.yml +++ b/.github/workflows/build.yml @@ -52,6 +52,9 @@ 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 diff --git a/Makefile b/Makefile index 53f25281..49a20e37 100644 --- a/Makefile +++ b/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