Fix compilation with new CompCert version

4 files changed, 16 insertions, 34 deletions

diff --git a/Makefile b/Makefile
index 763c892..d14ef13 100644
--- a/Makefile
+++ b/Makefile
@@ -31,8 +31,10 @@ all: lib/COMPCERTSTAMP
 	$(MAKE) proof
 	$(MAKE) compile
 
-lib/COMPCERTSTAMP:
+lib/CompCert/Makefile.config: lib/CompCert/configure
 	(cd lib/CompCert && ./configure --ignore-coq-version $(ARCH))
+
+lib/COMPCERTSTAMP: lib/CompCert/Makefile.config
 	$(MAKE) HAS_RUNTIME_LIB=false CLIGHTGEN=false INSTALL_COQDEV=false -C lib/CompCert
 	touch $@
 
diff --git a/default.nix b/default.nix
index 8308389..1121469 100644
--- a/default.nix
+++ b/default.nix
@@ -1,35 +1,15 @@
-with import (fetchTarball "https://github.com/NixOS/nixpkgs/archive/269fc4ddb896c1c5994eb4bb8c750ec18cb3db82.tar.gz") {};
+with import (fetchTarball "https://github.com/NixOS/nixpkgs/archive/8dd8bd8be74879f9f7919b16a4cb5ab2a75f18e5.tar.gz") {};
 let
-  ncoq = coq_8_12;
-  ncoqPackages = coqPackages_8_12;
-  bbv = ncoqPackages.callPackage
-    ( { coq, stdenv, fetchFromGitHub }:
-      stdenv.mkDerivation {
-        name = "coq${coq.coq-version}-bbv";
-
-        src = fetchFromGitHub {
-          owner = "mit-plv";
-          repo = "bbv";
-          rev = "5099237c52d2910f79a1a3ca9ae4dfa80129bf86";
-          sha256 = "0qnha333h7dc8105prdxvmkgy6l8swvyf6kz9v5s5dk4dvr5nra8";
-        };
-
-        buildInputs = with coq.ocamlPackages; [ ocaml camlp5 ];
-        propagatedBuildInputs = [ coq ];
-        enableParallelBuilding = true;
-
-        installPhase = ''
-          make -f Makefile.coq.all install COQLIB='$(out)/lib/coq/${coq.coq-version}/'
-        '';
-      } ) { };
+  ncoq = coq_8_13;
+  ncoqPackages = coqPackages_8_13;
 in
 stdenv.mkDerivation {
   name = "vericert";
   src = ./.;
 
   buildInputs = [ ncoq dune_2 gcc
-                  ocaml ocamlPackages.findlib ocamlPackages.menhir
-                  ocamlPackages.ocamlgraph
+                  ncoq.ocaml ncoq.ocamlPackages.findlib ncoq.ocamlPackages.menhir
+                  ncoq.ocamlPackages.ocamlgraph
                 ];
 
   enableParallelBuilding = true;
diff --git a/lib/CompCert b/lib/CompCert
-Subproject 48a9dcbdc968bcf05b4eec17b8c7fd471fb8024
+Subproject 1daf96cdca4d828c333cea5c9a314ef86134298
diff --git a/src/hls/RTLBlockInstr.v b/src/hls/RTLBlockInstr.v
index 5d9d578..3fab464 100644
--- a/src/hls/RTLBlockInstr.v
+++ b/src/hls/RTLBlockInstr.v
@@ -183,30 +183,30 @@ Fixpoint trans_pred (bound: nat) (p: pred_op) :
      | Pvar p' => Some (exist _ (((true, p') :: nil) :: nil) _)
      | Pand p1 p2 =>
       match trans_pred n p1, trans_pred n p2 with
-      | Some (exist p1' _), Some (exist p2' _) =>
+      | Some (exist _ p1' _), Some (exist _ p2' _) =>
         Some (exist _ (p1' ++ p2') _)
       | _, _ => None
       end
      | Por p1 p2 =>
       match trans_pred n p1, trans_pred n p2 with
-      | Some (exist p1' _), Some (exist p2' _) =>
+      | Some (exist _ p1' _), Some (exist _ p2' _) =>
         Some (exist _ (mult p1' p2') _)
       | _, _ => None
       end
      | Pnot (Pvar p') => Some (exist _ (((false, p') :: nil) :: nil) _)
      | Pnot (Pnot p') =>
        match trans_pred n p' with
-       | Some (exist p1' _) => Some (exist _ p1' _)
+       | Some (exist _ p1' _) => Some (exist _ p1' _)
        | None => None
        end
      | Pnot (Pand p1 p2) =>
        match trans_pred n (Por (Pnot p1) (Pnot p2)) with
-       | Some (exist p1' _) => Some (exist _ p1' _)
+       | Some (exist _ p1' _) => Some (exist _ p1' _)
        | None => None
        end
      | Pnot (Por p1 p2) =>
        match trans_pred n (Pand (Pnot p1) (Pnot p2)) with
-       | Some (exist p1' _) => Some (exist _ p1' _)
+       | Some (exist _ p1' _) => Some (exist _ p1' _)
        | None => None
        end
      end
@@ -239,9 +239,9 @@ Definition sat_pred (bound: nat) (p: pred_op) :
           + {forall a : asgn, sat_predicate p a = false}).
   refine
   ( match trans_pred bound p with
-    | Some (exist fm _) =>
+    | Some (exist _ fm _) =>
       match boundedSat bound fm with
-      | Some (inleft (exist a _)) => Some (inleft (exist _ a _))
+      | Some (inleft (exist _ a _)) => Some (inleft (exist _ a _))
       | Some (inright _) => Some (inright _)
       | None => None
       end
@@ -255,7 +255,7 @@ Qed.
 
 Definition sat_pred_simple (bound: nat) (p: pred_op) :=
   match sat_pred bound p with
-  | Some (inleft (exist al _)) => Some (Some al)
+  | Some (inleft (exist _ al _)) => Some (Some al)
   | Some (inright _) => Some None
   | None => None
   end.