From 18b1cdebdbeb38ae5c1b54069e4dc055eeac3758 Mon Sep 17 00:00:00 2001
From: Romain Tetley <romain.tetley@inria.fr>
Date: Mon, 28 Oct 2024 16:51:01 +0100
Subject: [PATCH] fix: add coq 8.20 in flake and fix the build for that version

---
 flake.lock                            | 18 +++++-----
 flake.nix                             | 51 +++++++++++++++++++++++++++
 language-server/dm/documentManager.ml |  7 ++--
 3 files changed, 65 insertions(+), 11 deletions(-)

diff --git a/flake.lock b/flake.lock
index c5bb52ff..f84eebcf 100644
--- a/flake.lock
+++ b/flake.lock
@@ -27,11 +27,11 @@
         "systems": "systems"
       },
       "locked": {
-        "lastModified": 1681202837,
-        "narHash": "sha256-H+Rh19JDwRtpVPAWp64F+rlEtxUWBAQW28eAi3SRSzg=",
+        "lastModified": 1710146030,
+        "narHash": "sha256-SZ5L6eA7HJ/nmkzGG7/ISclqe6oZdOZTNoesiInkXPQ=",
         "owner": "numtide",
         "repo": "flake-utils",
-        "rev": "cfacdce06f30d2b68473a46042957675eebb3401",
+        "rev": "b1d9ab70662946ef0850d488da1c9019f3a9752a",
         "type": "github"
       },
       "original": {
@@ -45,11 +45,11 @@
         "systems": "systems_2"
       },
       "locked": {
-        "lastModified": 1710146030,
-        "narHash": "sha256-SZ5L6eA7HJ/nmkzGG7/ISclqe6oZdOZTNoesiInkXPQ=",
+        "lastModified": 1726560853,
+        "narHash": "sha256-X6rJYSESBVr3hBoH0WbKE5KvhPU5bloyZ2L4K60/fPQ=",
         "owner": "numtide",
         "repo": "flake-utils",
-        "rev": "b1d9ab70662946ef0850d488da1c9019f3a9752a",
+        "rev": "c1dfcf08411b08f6b8615f7d8971a2bfa81d5e8a",
         "type": "github"
       },
       "original": {
@@ -60,11 +60,11 @@
     },
     "nixpkgs": {
       "locked": {
-        "lastModified": 1710827359,
-        "narHash": "sha256-/KY8hffTh9SN/tTcDn/FrEiYwTXnU8NKnr4D7/stmmA=",
+        "lastModified": 1729980323,
+        "narHash": "sha256-eWPRZAlhf446bKSmzw6x7RWEE4IuZgAp8NW3eXZwRAY=",
         "owner": "NixOS",
         "repo": "nixpkgs",
-        "rev": "5710127d9693421e78cca4f74fac2db6d67162b1",
+        "rev": "86e78d3d2084ff87688da662cf78c2af085d8e73",
         "type": "github"
       },
       "original": {
diff --git a/flake.nix b/flake.nix
index cd96cd33..445585bb 100644
--- a/flake.nix
+++ b/flake.nix
@@ -108,6 +108,46 @@
                 ]);
             };
 
+        vscoq-language-server-coq-8-20 =
+          # Notice the reference to nixpkgs here.
+          with import nixpkgs {inherit system;}; let
+            ocamlPackages = ocaml-ng.ocamlPackages_4_14;
+          in
+            ocamlPackages.buildDunePackage {
+              duneVersion = "3";
+              pname = "vscoq-language-server";
+              version = vscoq_version;
+              src = ./language-server;
+              nativeBuildInputs = [
+                coq_8_20
+              ];
+              buildInputs =
+                [
+                  coq_8_20
+                  dune_3
+                ]
+                ++ (with coq.ocamlPackages; [
+                  lablgtk3-sourceview3
+                  glib
+                  gnome.adwaita-icon-theme
+                  wrapGAppsHook
+                  ocaml
+                  yojson
+                  zarith
+                  findlib
+                  ppx_inline_test
+                  ppx_assert
+                  ppx_sexp_conv
+                  ppx_deriving
+                  ppx_optcomp
+                  ppx_import
+                  sexplib
+                  ppx_yojson_conv
+                  lsp
+                  sel
+                ]);
+            };
+
         vscoq-language-server-coq-master =
           # Notice the reference to nixpkgs here.
           with import nixpkgs {inherit system;}; let
@@ -254,6 +294,17 @@
               ]);
           };
 
+        vscoq-language-server-coq-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
+              ++ (with ocamlPackages; [
+                ocaml-lsp
+              ]);
+          };
+
         vscoq-language-server-coq-master = with import nixpkgs {inherit system;}; let
           ocamlPackages = ocaml-ng.ocamlPackages_4_14;
         in
diff --git a/language-server/dm/documentManager.ml b/language-server/dm/documentManager.ml
index 8adc123a..6e38e7b6 100644
--- a/language-server/dm/documentManager.ml
+++ b/language-server/dm/documentManager.ml
@@ -575,8 +575,11 @@ let get_completions st pos =
     | None -> Error ("Can't get completions")
     | Some lemmas -> Ok (lemmas)
 
-[%%if coq = "8.18" || coq = "8.19" || coq = "8.20"]
+[%%if coq = "8.18" || coq = "8.19"]
+[%%elif coq = "8.20"]
   let parsable_make = Pcoq.Parsable.make
+  let unfreeze = Pcoq.unfreeze
+  let entry_parse = Pcoq.Entry.parse
 [%%else]
   let parsable_make = Procq.Parsable.make
   let unfreeze = Procq.unfreeze
@@ -585,7 +588,7 @@ let get_completions st pos =
 
 [%%if coq = "8.18" || coq = "8.19"]
 let parse_entry st pos entry pattern =
-  let pa = parsable_make (Gramlib.Stream.of_string pattern) in
+  let pa = Pcoq.Parsable.make (Gramlib.Stream.of_string pattern) in
   let st = match Document.find_sentence_before st.document pos with
   | None -> st.init_vs.Vernacstate.synterp.parsing
   | Some { synterp_state } -> synterp_state.Vernacstate.Synterp.parsing