compcert: 3.7 → 3.8

pkgs/development/compilers/compcert/default.nix

@@ -1,23 +1,19 @@
-{ stdenv, lib, fetchFromGitHub, fetchpatch, makeWrapper
-, coq, ocamlPackages, coq2html
+{ stdenv, fetchFromGitHub, fetchpatch, makeWrapper
+, coqPackages, ocamlPackages, coq2html
 , tools ? stdenv.cc
+, version ? "3.8"
 }:
 
 let
   ocaml-pkgs      = with ocamlPackages; [ ocaml findlib menhir ];
   ccomp-platform = if stdenv.isDarwin then "x86_64-macosx" else "x86_64-linux";
+  inherit (coqPackages) coq flocq;
+  inherit (stdenv.lib) optional optionalString;
 in
-stdenv.mkDerivation rec {
-  pname = "compcert";
-  version = "3.7";
 
-  src = fetchFromGitHub {
-    owner = "AbsInt";
-    repo = "CompCert";
-    rev = "v${version}";
+let param = {
+  "3.7" = {
     sha256 = "1h4zhk9rrqki193nxs9vjvya7nl9yxjcf07hfqb6g77riy1vd2jr";
-  };
-
     patches = [
      (fetchpatch {
         url = "https://github.com/AbsInt/CompCert/commit/0a2db0269809539ccc66f8ec73637c37fbd23580.patch";
@@ -28,9 +24,29 @@ stdenv.mkDerivation rec {
         sha256 = "184nfdgxrkci880lkaj5pgnify3plka7xfgqrgv16275sqppc5hc";
       })
     ];
+  };
+  "3.8" = {
+    sha256 = "1gzlyxvw64ca12qql3wnq3bidcx9ygsklv9grjma3ib4hvg7vnr7";
+    useExternalFlocq = true;
+  };
+}."${version}"; in
+
+stdenv.mkDerivation rec {
+  pname = "compcert";
+  inherit version;
+
+  src = fetchFromGitHub {
+    owner = "AbsInt";
+    repo = "CompCert";
+    rev = "v${version}";
+    inherit (param) sha256;
+  };
+
+  patches = param.patches or [];
 
   nativeBuildInputs = [ makeWrapper ];
   buildInputs = ocaml-pkgs ++ [ coq coq2html ];
+  propagatedBuildInputs = optional (param.useExternalFlocq or false) flocq;
   enableParallelBuilding = true;
 
   postPatch = ''
@@ -43,6 +59,7 @@ stdenv.mkDerivation rec {
       -prefix $out \
       -coqdevdir $lib/lib/coq/${coq.coq-version}/user-contrib/compcert/ \
       -toolprefix ${tools}/bin/ \
+      ${optionalString (param.useExternalFlocq or false) "-use-external-Flocq"} \
       ${ccomp-platform}
   '';
 
@@ -68,7 +85,7 @@ stdenv.mkDerivation rec {
 
   meta = with stdenv.lib; {
     description = "Formally verified C compiler";
-    homepage    = "http://compcert.inria.fr";
+    homepage    = "https://compcert.org";
     license     = licenses.inria-compcert;
     platforms   = [ "x86_64-linux" "x86_64-darwin" ];
     maintainers = with maintainers; [ thoughtpolice jwiegley vbgl ];

pkgs/top-level/coq-packages.nix

@@ -1,4 +1,6 @@
-{ lib, callPackage, newScope, recurseIntoAttrs, ocamlPackages_4_05, ocamlPackages_4_09 }:
+{ lib, callPackage, newScope, recurseIntoAttrs, ocamlPackages_4_05, ocamlPackages_4_09
+, compcert
+}:
 
 let
   mkCoqPackages' = self: coq:
@@ -59,7 +61,9 @@ let
       tlc = callPackage ../development/coq-modules/tlc {};
       Velisarios = callPackage ../development/coq-modules/Velisarios {};
       Verdi = callPackage ../development/coq-modules/Verdi {};
-      VST = callPackage ../development/coq-modules/VST {};
+      VST = callPackage ../development/coq-modules/VST {
+        compcert = compcert.override { version = "3.7"; };
+      };
 
       filterPackages = filterCoqPackages;
     };