From 8eb8c5705733f2229f605042cfdd4ce76eab6682 Mon Sep 17 00:00:00 2001 From: Romain Tetley Date: Tue, 19 Nov 2024 09:41:42 +0100 Subject: [PATCH 1/3] fix: update flake to have git in dev shell --- flake.nix | 15 ++++++++++----- 1 file changed, 10 insertions(+), 5 deletions(-) diff --git a/flake.nix b/flake.nix index 4924db6a..2b918f78 100644 --- a/flake.nix +++ b/flake.nix @@ -280,7 +280,8 @@ self.packages.${system}.vscoq-language-server-coq-8-18.buildInputs ++ (with ocamlPackages; [ ocaml-lsp - ]); + ]) + ++ ([git]); }; vscoq-language-server-coq-8-19 = with import nixpkgs {inherit system;}; let @@ -291,7 +292,8 @@ self.packages.${system}.vscoq-language-server-coq-8-19.buildInputs ++ (with ocamlPackages; [ ocaml-lsp - ]); + ]) + ++ ([git]); }; vscoq-language-server-coq-8-20 = with import nixpkgs {inherit system;}; let @@ -302,7 +304,8 @@ self.packages.${system}.vscoq-language-server-coq-8-20.buildInputs ++ (with ocamlPackages; [ ocaml-lsp - ]); + ]) + ++ ([git]); }; vscoq-language-server-coq-master = with import nixpkgs {inherit system;}; let @@ -313,7 +316,8 @@ self.packages.${system}.vscoq-language-server-coq-master.buildInputs ++ (with ocamlPackages; [ ocaml-lsp - ]); + ]) + ++ ([git]); }; default = with import nixpkgs {inherit system;}; let @@ -324,7 +328,8 @@ self.packages.${system}.vscoq-language-server-coq-8-19.buildInputs ++ (with ocamlPackages; [ ocaml-lsp - ]); + ]) + ++ ([git]); }; }; }); From 0454b11bb79c2d8e66204289dedc8f02e3909ac2 Mon Sep 17 00:00:00 2001 From: Romain Tetley Date: Tue, 19 Nov 2024 10:13:42 +0100 Subject: [PATCH 2/3] fix: fix lspManager for prior versions of coq (8.18, 8.19, 8.20) and test --- client/src/test/suite/extension.test.ts | 2 ++ language-server/vscoqtop/lspManager.ml | 16 +++++++++++++++- 2 files changed, 17 insertions(+), 1 deletion(-) diff --git a/client/src/test/suite/extension.test.ts b/client/src/test/suite/extension.test.ts index e02aef00..1e6ecc98 100644 --- a/client/src/test/suite/extension.test.ts +++ b/client/src/test/suite/extension.test.ts @@ -12,6 +12,7 @@ suite('Should get diagnostics', function () { const ext = vscode.extensions.getExtension('maximedenes.vscoq')!; await ext.activate(); + vscode.workspace.getConfiguration().update('vscoq.proof.mode','Continuous'); const doc = await common.openTextFile('basic.v'); @@ -34,6 +35,7 @@ suite('Should get diagnostics', function () { const ext = vscode.extensions.getExtension('maximedenes.vscoq')!; await ext.activate(); + vscode.workspace.getConfiguration().update('vscoq.proof.mode','Continuous'); const doc1 = await common.openTextFile('basic.v'); const doc2 = await common.openTextFile('warn.v'); diff --git a/language-server/vscoqtop/lspManager.ml b/language-server/vscoqtop/lspManager.ml index 446e4ce6..9982545b 100644 --- a/language-server/vscoqtop/lspManager.ml +++ b/language-server/vscoqtop/lspManager.ml @@ -268,6 +268,19 @@ let init_document local_args vst = Vernacstate.freeze_full_state () [%%endif] +[%%if coq = "8.18" || coq = "8.19" || coq = "8.20"] + let parse_args args = + let usage = { + Boot.Usage.executable_name = ""; + extra_args = ""; + extra_options = ""; + } in + fst @@ Coqargs.parse_args ~init:Coqargs.default ~usage args +[%%else] + let parse_args args = + fst @@ Coqargs.parse_args ~init:Coqargs.default args +[%%endif] + let open_new_document uri text = let vst = get_init_state () in @@ -282,7 +295,8 @@ let open_new_document uri text = let project = CoqProject_file.read_project_file ~warning_fn:(fun _ -> ()) f in let args = CoqProject_file.coqtop_args_from_project project in log (Printf.sprintf "Arguments from project file %s: %s" f (String.concat " " args)); - fst @@ Coqargs.parse_args ~init:Coqargs.default args + parse_args args + in let vst = init_document local_args vst in From 0f0f29b8fe472b9ed21111960d8034569537a925 Mon Sep 17 00:00:00 2001 From: Romain Tetley Date: Fri, 22 Nov 2024 10:19:47 +0100 Subject: [PATCH 3/3] fix: flake file clean up and ci fixes --- .github/workflows/ci.yml | 12 ++++----- flake.nix | 58 +++++++++++++++++++++++----------------- 2 files changed, 40 insertions(+), 30 deletions(-) diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index a683b034..2df9ad8f 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -28,7 +28,7 @@ jobs: fail-fast: false matrix: os: [ubuntu-latest, macos-latest] - coq: [coq-8-18, coq-8-19, coq-master] + coq: [8-18, 8-19, 8-20, master] profile: [dev, fatalwarnings] runs-on: ${{ matrix.os }} steps: @@ -53,11 +53,11 @@ jobs: diff new_yarn.nix yarn.nix diff goal-view-ui/new_yarn.nix goal-view-ui/yarn.nix diff search-ui/new_yarn.nix search-ui/yarn.nix - - run: nix develop .#vscoq-language-server-${{ matrix.coq }} -c bash -c "cd language-server && dune build --profile ${{ matrix.profile }}" - - run: nix develop .#vscoq-client -c bash -c "cd client && yarn run install:all && yarn run build:all && yarn run compile" - - run: xvfb-run nix develop .#vscoq-client -c bash -c "cd client && yarn test" + - run: nix develop .#vscoq-${{ matrix.coq }} -c bash -c "cd language-server && dune build --profile ${{ matrix.profile }}" + - run: nix develop .#vscoq-${{ matrix.coq }} -c bash -c "cd client && yarn run install:all && yarn run build:all && yarn run compile" + - run: xvfb-run nix develop .#vscoq-${{ matrix.coq }} -c bash -c "cd client && yarn test" if: runner.os == 'Linux' - - run: nix develop .#vscoq-client -c bash -c "cd client && yarn test" + - run: nix develop .#vscoq-${{ matrix.coq }} -c bash -c "cd client && yarn test" if: runner.os != 'Linux' - if: ${{ failure() }} run: cat /tmp/vscoq_init_log.* @@ -68,7 +68,7 @@ jobs: matrix: os: [ubuntu-latest] ocaml-compiler: [4.14.x] - coq: [8.18.0, 8.19.0, 8.20+rc1, dev] + coq: [8.18.0, 8.19.0, 8.20.0, dev] runs-on: ${{ matrix.os }} steps: - name: Checkout diff --git a/flake.nix b/flake.nix index 2b918f78..2769b9b0 100644 --- a/flake.nix +++ b/flake.nix @@ -26,7 +26,7 @@ formatter = nixpkgs.legacyPackages.${system}.alejandra; packages = { - default = self.packages.${system}.vscoq-language-server-coq-8-19; + default = self.packages.${system}.vscoq-language-server-coq-8-20; vscoq-language-server-coq-8-18 = # Notice the reference to nixpkgs here. @@ -52,9 +52,8 @@ gnome.adwaita-icon-theme wrapGAppsHook ocaml - yojson - zarith findlib + yojson ppx_inline_test ppx_assert ppx_sexp_conv @@ -66,6 +65,10 @@ lsp sel ]); + propagatedBuildInputs= (with coq.ocamlPackages; + [ + zarith + ]); }; vscoq-language-server-coq-8-19 = @@ -93,7 +96,6 @@ wrapGAppsHook ocaml yojson - zarith findlib ppx_inline_test ppx_assert @@ -106,6 +108,10 @@ lsp sel ]); + propagatedBuildInputs= (with coq.ocamlPackages; + [ + zarith + ]); }; vscoq-language-server-coq-8-20 = @@ -133,7 +139,6 @@ wrapGAppsHook ocaml yojson - zarith findlib ppx_inline_test ppx_assert @@ -146,6 +151,10 @@ lsp sel ]); + propagatedBuildInputs= (with coq.ocamlPackages; + [ + zarith + ]); }; vscoq-language-server-coq-master = @@ -173,7 +182,6 @@ wrapGAppsHook ocaml yojson - zarith findlib ppx_inline_test ppx_assert @@ -186,6 +194,10 @@ lsp sel ]); + propagatedBuildInputs= (with coq.ocamlPackages; + [ + zarith + ]); }; vscoq-client = with import nixpkgs {inherit system;}; let @@ -267,53 +279,50 @@ }; devShells = { - vscoq-client = with import nixpkgs {inherit system;}; - mkShell { - buildInputs = self.packages.${system}.vscoq-client.extension.buildInputs; - }; - - vscoq-language-server-coq-8-18 = with import nixpkgs {inherit system;}; let - ocamlPackages = ocaml-ng.ocamlPackages_4_14; - in + vscoq-8-18 = with import nixpkgs {inherit system;}; mkShell { - buildInputs = - self.packages.${system}.vscoq-language-server-coq-8-18.buildInputs + buildInputs = + self.packages.${system}.vscoq-client.extension.buildInputs + ++ self.packages.${system}.vscoq-language-server-coq-8-18.buildInputs ++ (with ocamlPackages; [ ocaml-lsp ]) ++ ([git]); }; - - vscoq-language-server-coq-8-19 = with import nixpkgs {inherit system;}; let + + vscoq-8-19 = with import nixpkgs {inherit system;}; let ocamlPackages = ocaml-ng.ocamlPackages_4_14; in mkShell { buildInputs = - self.packages.${system}.vscoq-language-server-coq-8-19.buildInputs + self.packages.${system}.vscoq-client.extension.buildInputs + ++ self.packages.${system}.vscoq-language-server-coq-8-19.buildInputs ++ (with ocamlPackages; [ ocaml-lsp ]) ++ ([git]); }; - vscoq-language-server-coq-8-20 = with import nixpkgs {inherit system;}; let + vscoq-8-20 = with import nixpkgs {inherit system;}; let ocamlPackages = ocaml-ng.ocamlPackages_4_14; in mkShell { buildInputs = - self.packages.${system}.vscoq-language-server-coq-8-20.buildInputs + self.packages.${system}.vscoq-client.extension.buildInputs + ++ self.packages.${system}.vscoq-language-server-coq-8-20.buildInputs ++ (with ocamlPackages; [ ocaml-lsp ]) ++ ([git]); }; - vscoq-language-server-coq-master = with import nixpkgs {inherit system;}; let + vscoq-master = with import nixpkgs {inherit system;}; let ocamlPackages = ocaml-ng.ocamlPackages_4_14; in mkShell { buildInputs = - self.packages.${system}.vscoq-language-server-coq-master.buildInputs + self.packages.${system}.vscoq-client.extension.buildInputs + ++ self.packages.${system}.vscoq-language-server-coq-master.buildInputs ++ (with ocamlPackages; [ ocaml-lsp ]) @@ -325,7 +334,8 @@ in mkShell { buildInputs = - self.packages.${system}.vscoq-language-server-coq-8-19.buildInputs + self.packages.${system}.vscoq-client.extension.buildInputs + ++ self.packages.${system}.vscoq-language-server-coq-8-20.buildInputs ++ (with ocamlPackages; [ ocaml-lsp ])