Merge pull request #946 from coq/fixing-italian-boulette

Fix for prior versions of Coq
coq · Nov 22, 2024 · 98c1c0d · 98c1c0d
2 parents ef6a163 + 0f0f29b
commit 98c1c0d
Show file tree

Hide file tree

Showing 4 changed files with 67 additions and 36 deletions.
diff --git 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
@@ -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
@@ -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,64 +279,67 @@
       };
 
       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
           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-20.buildInputs
               ++ (with ocamlPackages; [
                 ocaml-lsp
-              ]);
+              ])
+              ++ ([git]);
           };
       };
     });

diff --git 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