Fix flake + adapt to coq/coq#18529

Fixing Coq pin in flake and adding correction to make coq master branch compile.
coq · Feb 6, 2024 · bf063d8 · bf063d8
1 parent 87dd6d0
commit bf063d8
Show file tree

Hide file tree

Showing 3 changed files with 14 additions and 6 deletions.
diff --git a/flake.lock b/flake.lock
diff --git a/flake.nix b/flake.nix
@@ -5,7 +5,7 @@
 
     flake-utils.url = "github:numtide/flake-utils";
 
-    coq-master = { url = "github:coq/coq/fbaea89860348ca2b2ca485e52df7215bea27746"; }; # Should be kept in sync with PIN_COQ in CI workflow
+    coq-master = { url = "github:coq/coq/b157d65080076498ad04dd3918c1e508eb9740c0"; }; # Should be kept in sync with PIN_COQ in CI workflow
     coq-master.inputs.nixpkgs.follows = "nixpkgs";
 
   };
@@ -156,9 +156,13 @@
 
     devShells.vscoq-language-server-coq-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-language-server-coq-master.buildInputs
+          ++ (with ocamlPackages; [
+            ocaml-lsp
+          ]);
       };
 
     devShells.default = 

diff --git a/language-server/dm/parTactic.ml b/language-server/dm/parTactic.ml
@@ -60,7 +60,11 @@ let assign_tac ~abstract res : unit Proofview.tactic =
       tclUNIT ()
   end)
 
+[%%if coq = "8.18" || coq = "8.19"]
 let command_focus = Proof.new_focus_kind ()
+[%%else]
+let command_focus = Proof.new_focus_kind "vscoq_command_focus"
+[%%endif]
 
 let worker_solve_one_goal { TacticJob.state; ast; goalno; goal } ~send_back =
   let focus_cond = Proof.no_cond command_focus in