Merge pull request #702 from coq-community/coq-8.19

Coq 8.19 compatibility

Author: rtetley

.github/workflows/ci.yml

@@ -27,6 +27,7 @@ jobs:
     strategy:
       matrix:
         os: [ubuntu-latest, macos-latest]
+        coq: [coq-8-18, coq-8-19, coq-master]
     runs-on: ${{ matrix.os }}
     steps:
     - name: Checkout
@@ -41,7 +42,7 @@ jobs:
     - uses: cachix/install-nix-action@v22
       with:
         nix_path: nixpkgs=channel:nixos-unstable
-    - run: nix develop .#vscoq-language-server -c bash -c "cd language-server && dune build"
+    - run: nix develop .#vscoq-language-server-${{ matrix.coq }} -c bash -c "cd language-server && dune build"
     - run: nix develop .#vscoq-client -c bash -c "cd client && yarn run install:all && yarn run build:all && yarn run compile"
     - run: xvfb-run nix develop .#vscoq-client -c bash -c "cd client && yarn test"
       if: runner.os == 'Linux'
@@ -52,9 +53,11 @@ jobs:
 
   install-opam:
     strategy:
+      fail-fast: false
       matrix:
         os: [ubuntu-latest]
         ocaml-compiler: [4.13.x]
+        coq: [8.18.0, 8.19+rc1, dev]
     runs-on: ${{ matrix.os }}
     steps:
     - name: Checkout
@@ -70,6 +73,7 @@ jobs:
         OPAMYES: true
       run: |
         opam repo add coq-core-dev https://coq.inria.fr/opam/core-dev
+        opam install coq-core.${{ matrix.coq }}
         opam pin add vscoq-language-server ./language-server/ --with-doc --with-test -y
 
     - run: |

flake.lock

@@ -5,16 +5,88 @@
 
     flake-utils.url = "github:numtide/flake-utils";
 
+    coq-master = { url = "github:coq/coq/b157d65080076498ad04dd3918c1e508eb9740c0"; }; # Should be kept in sync with PIN_COQ in CI workflow
+    coq-master.inputs.nixpkgs.follows = "nixpkgs";
+
   };
 
-  outputs = { self, nixpkgs, flake-utils }:
+  outputs = { self, nixpkgs, flake-utils, coq-master }:
     flake-utils.lib.eachDefaultSystem (system:
 
+   let coq = coq-master.defaultPackage.${system}; in
    rec {
 
-    packages.default = self.packages.${system}.vscoq-language-server;
+    packages.default = self.packages.${system}.vscoq-language-server-coq-8-19;
+
+    packages.vscoq-language-server-coq-8-18 =
+      # 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 = "2.0.3";
+        src = ./language-server;
+        buildInputs = [
+          coq_8_18
+          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
+        ]);
+      };
+
+      packages.vscoq-language-server-coq-8-19 =
+      # 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 = "2.0.3";
+        src = ./language-server;
+        buildInputs = [
+          coq_8_19
+          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
+        ]);
+      };
 
-    packages.vscoq-language-server =
+    packages.vscoq-language-server-coq-master =
       # Notice the reference to nixpkgs here.
       with import nixpkgs { inherit system; };
       let ocamlPackages = ocaml-ng.ocamlPackages_4_14; in
@@ -39,6 +111,7 @@
           ppx_assert
           ppx_sexp_conv
           ppx_deriving
+          ppx_optcomp
           ppx_import
           sexplib
           ppx_yojson_conv
@@ -61,11 +134,42 @@
 
     };
 
-    devShells.default =
+    devShells.vscoq-client = 
+      with import nixpkgs { inherit system; };
+      mkShell {
+        buildInputs = self.packages.${system}.vscoq-client.buildInputs;
+      };
+
+    devShells.vscoq-language-server-coq-8-18 = 
+        with import nixpkgs { inherit system; };
+        mkShell {
+            buildInputs =
+            self.packages.${system}.vscoq-language-server-coq-8-18.buildInputs;
+        };
+        
+    devShells.vscoq-language-server-coq-8-19 = 
+      with import nixpkgs { inherit system; };
+      mkShell {
+        buildInputs =
+          self.packages.${system}.vscoq-language-server-coq-8-19.buildInputs;
+      };
+    
+    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
+          ++ (with ocamlPackages; [
+            ocaml-lsp
+          ]);
+      };
+
+    devShells.default = 
       with import nixpkgs { inherit system; };
       mkShell {
         buildInputs =
-          self.packages.${system}.vscoq-language-server.buildInputs
+          self.packages.${system}.vscoq-language-server-coq-8-19.buildInputs
           ++ (with ocamlPackages; [
             ocaml-lsp
           ]);

flake.nix

@@ -415,13 +415,18 @@ let get_completion_items env proof lemmas options =
     log ("Ranking of lemmas failed: " ^ (Printexc.to_string e));
     lemmas
 
+[%%if coq = "8.18"]
+let generic_search e s f = Search.generic_search e (fun r k e c -> f r k e s c)
+[%%else]
+let generic_search = Search.generic_search
+[%%endif]
 let get_lemmas sigma env =
   let open CompletionItems in
   let results = ref [] in
-  let display ref _kind env c =
+  let display ref _kind env sigma c =
     results := mk_completion_item sigma ref env c :: results.contents;
   in
-  Search.generic_search env display;
+  generic_search env sigma display;
   results.contents
 
 let get_completions options st =

language-server/dm/completionSuggester.ml

@@ -252,6 +252,12 @@ let rec junk_sentence_end stream =
   | [] -> ()
   | _ ->  Stream.junk () stream; junk_sentence_end stream
 
+[%%if coq = "8.18"]
+exception E = Stream.Error
+[%%else]
+exception E = Grammar.Error
+[%%endif]
+
 let rec parse_more synterp_state stream raw parsed errors =
   let handle_parse_error start msg =
     log @@ "handling parse error at " ^ string_of_int start;
@@ -290,7 +296,7 @@ let rec parse_more synterp_state stream raw parsed errors =
           let loc = Loc.get_loc @@ info in
           handle_parse_error start (loc, Pp.string_of_ppcmds @@ CErrors.iprint_no_report (e,info))
         end
-    | exception (Stream.Error msg as exn) ->
+    | exception (E msg as exn) ->
       let loc = Loc.get_loc @@ Exninfo.info exn in
       junk_sentence_end stream;
       handle_parse_error start (loc,msg)
@@ -388,4 +394,4 @@ module Internal = struct
     sentence.start
     sentence.stop
 
-end
+end

language-server/dm/document.ml

@@ -2,6 +2,7 @@
  (name dm)
  (public_name vscoq-language-server.dm)
  (modules :standard \ vscoqtop_proof_worker vscoqtop_tactic_worker)
+ (preprocess (pps ppx_optcomp -- -cookie "ppx_optcomp.env=env ~coq:(Defined \"%{coq:version.major}.%{coq:version.minor}\")"))
  (libraries base coq-core.sysinit coq-core.vernac coq-core.parsing lsp sel protocol language))
 
 (executable

language-server/dm/dune

@@ -182,14 +182,22 @@ let interp_ast ~doc_id ~state_id ~st ~error_recovery ast =
         st, status, []
 
 (* This adapts the Future API with our event model *)
+[%%if coq = "8.18"]
+let definition_using e s ~fixnames:_ ~using ~terms =
+  Proof_using.definition_using e s ~using ~terms
+[%%else]
+let definition_using = Proof_using.definition_using
+[%%endif]
 let interp_qed_delayed ~proof_using ~state_id ~st =
+  let lemmas = Option.get @@ st.Vernacstate.interp.lemmas in
   let f proof =
     let proof =
       let env = Global.env () in
       let sigma, _ = Declare.Proof.get_current_context proof in
       let initial_goals pf = Proofview.initial_goals Proof.((data pf).entry) in
       let terms = List.map (fun (_,_,x) -> x) (initial_goals (Declare.Proof.get proof)) in
-      let using = Proof_using.definition_using env sigma ~using:proof_using ~terms in
+      let names = Vernacstate.LemmaStack.get_all_proof_names lemmas in
+      let using = definition_using env sigma ~fixnames:names ~using:proof_using ~terms in
       let vars = Environ.named_context env in
       Names.Id.Set.iter (fun id ->
           if not (List.exists Util.(Context.Named.Declaration.get_id %> Names.Id.equal id) vars) then
@@ -202,7 +210,6 @@ let interp_qed_delayed ~proof_using ~state_id ~st =
     let f, assign = Future.create_delegate ~blocking:false ~name:"XX" fix_exn in
     Declare.Proof.close_future_proof ~feedback_id:state_id proof f, assign
   in
-  let lemmas = Option.get @@ st.Vernacstate.interp.lemmas in
   let proof, assign = Vernacstate.LemmaStack.with_top lemmas ~f in
   let control = [] (* FIXME *) in
   let opaque = Vernacexpr.Opaque in

language-server/dm/executionManager.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