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/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/flake.nix b/flake.nix index 4924db6a..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,54 @@ }; 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 - ]); + ]) + ++ ([git]); }; default = with import nixpkgs {inherit system;}; let @@ -321,10 +334,12 @@ 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 - ]); + ]) + ++ ([git]); }; }; }); 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