Merge pull request #934 from coq/update-flake

Fix the CI by updating the coq pin in nix flake

flake.nix

@@ -4,7 +4,7 @@
   inputs = {
     flake-utils.url = "github:numtide/flake-utils";
 
-    coq-master = { url = "github:coq/coq/b42eb84e4422dcf428d46553f002c728f705a6a9"; }; # Should be kept in sync with PIN_COQ in CI workflow
+    coq-master = { url = "github:coq/coq/e9d68d22c6605f2980f6bdccf9ac615c2eb16a0b"; }; # Should be kept in sync with PIN_COQ in CI workflow
     coq-master.inputs.nixpkgs.follows = "nixpkgs";
 
   };
@@ -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

language-server/dm/document.ml

@@ -359,13 +359,18 @@ let string_of_diff_item doc = function
 let string_of_diff doc l =
   String.concat "\n" (List.flatten (List.map (string_of_diff_item doc) l))
 
+[%%if coq = "8.18" || coq = "8.19" || coq = "8.20"]
+  let get_keyword_state = Pcoq.get_keyword_state
+[%%else]
+  let get_keyword_state = Procq.get_keyword_state
+[%%endif]
+
 let rec stream_tok n_tok acc str begin_line begin_char =
-  let e = LStream.next (Pcoq.get_keyword_state ()) str in
+  let e = LStream.next (get_keyword_state ()) str in
   if Tok.(equal e EOI) then
     List.rev acc
   else
     stream_tok (n_tok+1) (e::acc) str begin_line begin_char
-
     (*
 let parse_one_sentence stream ~st =
   let pa = Pcoq.Parsable.make stream in
@@ -381,7 +386,7 @@ let parse_one_sentence ?loc stream ~st =
   let pa = Pcoq.Parsable.make ?loc stream in
   let sentence = Pcoq.Entry.parse entry pa in
   (sentence, [])
-[%%else]
+[%%elif coq = "8.20"]
 let parse_one_sentence ?loc stream ~st =
   Vernacstate.Synterp.unfreeze st;
   Flags.record_comments := true;
@@ -390,6 +395,15 @@ let parse_one_sentence ?loc stream ~st =
   let sentence = Pcoq.Entry.parse entry pa in
   let comments = Pcoq.Parsable.comments pa in
   (sentence, comments)
+[%%else]
+let parse_one_sentence ?loc stream ~st =
+  Vernacstate.Synterp.unfreeze st;
+  Flags.record_comments := true;
+  let entry = Pvernac.main_entry (Some (Synterp.get_default_proof_mode ())) in
+  let pa = Procq.Parsable.make ?loc stream in
+  let sentence = Procq.Entry.parse entry pa in
+  let comments = Procq.Parsable.comments pa in
+  (sentence, comments)
 [%%endif]
 
 let rec junk_sentence_end stream =

language-server/dm/documentManager.ml

@@ -581,6 +581,17 @@ let get_completions st pos =
     | None -> Error ("Can't get completions")
     | Some lemmas -> Ok (lemmas)
 
+[%%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
+  let entry_parse = Procq.Entry.parse
+[%%endif]
+
 [%%if coq = "8.18" || coq = "8.19"]
 let parse_entry st pos entry pattern =
   let pa = Pcoq.Parsable.make (Gramlib.Stream.of_string pattern) in
@@ -591,13 +602,19 @@ let parse_entry st pos entry pattern =
   Vernacstate.Parser.parse st entry pa
 [%%else]
 let parse_entry st pos entry pattern =
-  let pa = Pcoq.Parsable.make (Gramlib.Stream.of_string pattern) in
+  let pa = parsable_make (Gramlib.Stream.of_string pattern) in
   let st = match Document.find_sentence_before st.document pos with
   | None -> Vernacstate.(Synterp.parsing st.init_vs.synterp)
   | Some { synterp_state } -> Vernacstate.Synterp.parsing synterp_state
   in  
-  Pcoq.unfreeze st;
-  Pcoq.Entry.parse entry pa
+  unfreeze st;
+  entry_parse entry pa
+[%%endif]
+
+[%%if coq = "8.18" || coq = "8.19" || coq = "8.20"]
+  let smart_global = Pcoq.Prim.smart_global
+[%%else]
+  let smart_global = Procq.Prim.smart_global
 [%%endif]
 
 let about st pos ~pattern =
@@ -606,7 +623,7 @@ let about st pos ~pattern =
   | None -> Error ("No context found") (*TODO execute *)
   | Some (sigma, env) ->
     try
-      let ref_or_by_not = parse_entry st loc (Pcoq.Prim.smart_global) pattern in
+      let ref_or_by_not = parse_entry st loc (smart_global) pattern in
       let udecl = None (* TODO? *) in
       Ok (pp_of_coqpp @@ Prettyp.print_about env sigma ref_or_by_not udecl)
     with e ->
@@ -627,7 +644,7 @@ let hover_of_sentence st loc pattern sentence =
   | None -> log "hover: no context found"; None
   | Some (sigma, env) ->
     try
-      let ref_or_by_not = parse_entry st loc (Pcoq.Prim.smart_global) pattern in
+      let ref_or_by_not = parse_entry st loc (smart_global) pattern in
       Language.Hover.get_hover_contents env sigma ref_or_by_not
     with e ->
       let e, info = Exninfo.capture e in
@@ -664,12 +681,18 @@ let hover st pos =
         hover_of_sentence st loc pattern (Document.find_next_qed st.document loc)
     | _ -> None
 
+[%%if coq = "8.18" || coq = "8.19" || coq = "8.20"]
+  let lconstr = Pcoq.Constr.lconstr
+[%%else]
+  let lconstr = Procq.Constr.lconstr
+[%%endif]
+
 let check st pos ~pattern =
   let loc = RawDocument.loc_of_position (Document.raw_document st.document) pos in
   match get_context st pos with
   | None -> Error ("No context found") (*TODO execute *)
   | Some (sigma,env) ->
-    let rc = parse_entry st loc Pcoq.Constr.lconstr pattern in
+    let rc = parse_entry st loc lconstr pattern in
     try
       let redexpr = None in
       Ok (pp_of_coqpp @@ Vernacentries.check_may_eval env sigma redexpr rc)
@@ -688,34 +711,29 @@ let locate st pos ~pattern =
   match get_context st pos with
   | None -> Error ("No context found") (*TODO execute *)
   | Some (sigma, env) ->
-    match parse_entry st loc (Pcoq.Prim.smart_global) pattern with
+    match parse_entry st loc (smart_global) pattern with
     | { v = AN qid } -> Ok (pp_of_coqpp @@ print_located_qualid env qid)
     | { v = ByNotation (ntn, sc)} ->
       Ok( pp_of_coqpp @@ Notation.locate_notation
         (Constrextern.without_symbols (Printer.pr_glob_constr_env env sigma)) ntn sc)
 
 [%%if coq = "8.18" || coq = "8.19"]
-let print st pos ~pattern = 
-  let loc = RawDocument.loc_of_position (Document.raw_document st.document) pos in
-  match get_context st pos with
-  | None -> Error("No context found")
-  | Some (sigma, env) ->
-    let qid = parse_entry st loc (Pcoq.Prim.smart_global) pattern in
-    let udecl = None in (*TODO*)
-    Ok ( pp_of_coqpp @@ Prettyp.print_name env sigma qid udecl )
+  let print_name = Prettyp.print_name
 [%%else]
-let print st pos ~pattern =
+  let print_name =
+    let access = Library.indirect_accessor[@@warning "-3"] in
+    Prettyp.print_name access
+[%%endif]
+
+let print st pos ~pattern = 
   let loc = RawDocument.loc_of_position (Document.raw_document st.document) pos in
   match get_context st pos with
   | None -> Error("No context found")
   | Some (sigma, env) ->
-    let qid = parse_entry st loc (Pcoq.Prim.smart_global) pattern in
+    let qid = parse_entry st loc (smart_global) pattern in
     let udecl = None in (*TODO*)
-    let access = Library.indirect_accessor[@@warning "-3"] in
-    Ok ( pp_of_coqpp @@ Prettyp.print_name access env sigma qid udecl )
-[%%endif]
+    Ok ( pp_of_coqpp @@ print_name env sigma qid udecl )
 
-
 module Internal = struct
 
   let document st =