From bf063d8c4e800b423ce0d274c0bdd95bab45705b Mon Sep 17 00:00:00 2001
From: Romain Tetley <romain.tetley@inria.fr>
Date: Tue, 6 Feb 2024 11:46:14 +0100
Subject: [PATCH] Fix flake + adapt to https://github.com/coq/coq/pull/18529

Fixing Coq pin in flake and adding correction to make coq master
branch compile.
---
 flake.lock                      | 8 ++++----
 flake.nix                       | 8 ++++++--
 language-server/dm/parTactic.ml | 4 ++++
 3 files changed, 14 insertions(+), 6 deletions(-)

diff --git a/flake.lock b/flake.lock
index 3f6eb2ac..e25910e3 100644
--- a/flake.lock
+++ b/flake.lock
@@ -8,17 +8,17 @@
         ]
       },
       "locked": {
-        "lastModified": 1692621436,
-        "narHash": "sha256-fLkFHuL8vu4v7Oc9v2701d7pVM/eS/7mCJTEuAFfksA=",
+        "lastModified": 1707209540,
+        "narHash": "sha256-C3ZnIXZQptLo76iqltf/GYu/EqFU5yT7nSMClKTriiI=",
         "owner": "coq",
         "repo": "coq",
-        "rev": "fbaea89860348ca2b2ca485e52df7215bea27746",
+        "rev": "b157d65080076498ad04dd3918c1e508eb9740c0",
         "type": "github"
       },
       "original": {
         "owner": "coq",
         "repo": "coq",
-        "rev": "fbaea89860348ca2b2ca485e52df7215bea27746",
+        "rev": "b157d65080076498ad04dd3918c1e508eb9740c0",
         "type": "github"
       }
     },
diff --git a/flake.nix b/flake.nix
index f4652bf8..89bcc24e 100644
--- 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
index 4f85bace..169e62bc 100644
--- 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