fix: add coq 8.20 in flake and fix the build for that version

coq · Oct 28, 2024 · 18b1cde · 18b1cde
1 parent 0b038bd
commit 18b1cde
Show file tree

Hide file tree

Showing 3 changed files with 65 additions and 11 deletions.
diff --git a/flake.lock b/flake.lock
diff --git 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
@@ -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