@@ -1,36 +1,52 @@
1−{ stdenv, lib, fetchFromGitHub, fetchpatch, makeWrapper
2−, coq, ocamlPackages, coq2html
1+{ stdenv, fetchFromGitHub, fetchpatch, makeWrapper
2+, coqPackages, ocamlPackages, coq2html
33, tools ? stdenv.cc
4+, version ? "3.8"
45}:
56
67let
78 ocaml-pkgs = with ocamlPackages; [ ocaml findlib menhir ];
89 ccomp-platform = if stdenv.isDarwin then "x86_64-macosx" else "x86_64-linux";
10+ inherit (coqPackages) coq flocq;
11+ inherit (stdenv.lib) optional optionalString;
912in
13+
14+let param = {
15+ "3.7" = {
16+ sha256 = "1h4zhk9rrqki193nxs9vjvya7nl9yxjcf07hfqb6g77riy1vd2jr";
17+ patches = [
18+ (fetchpatch {
19+ url = "https://github.com/AbsInt/CompCert/commit/0a2db0269809539ccc66f8ec73637c37fbd23580.patch";
20+ sha256 = "0n8qrba70x8f422jdvq9ddgsx6avf2dkg892g4ldh3jiiidyhspy";
21+ })
22+ (fetchpatch {
23+ url = "https://github.com/AbsInt/CompCert/commit/5e29f8b5ba9582ecf2a1d0baeaef195873640607.patch";
24+ sha256 = "184nfdgxrkci880lkaj5pgnify3plka7xfgqrgv16275sqppc5hc";
25+ })
26+ ];
27+ };
28+ "3.8" = {
29+ sha256 = "1gzlyxvw64ca12qql3wnq3bidcx9ygsklv9grjma3ib4hvg7vnr7";
30+ useExternalFlocq = true;
31+ };
32+}."${version}"; in
33+
1034stdenv.mkDerivation rec {
1135 pname = "compcert";
12− version = "3.7";
36+ inherit version;
1337
1438 src = fetchFromGitHub {
1539 owner = "AbsInt";
1640 repo = "CompCert";
1741 rev = "v${version}";
18− sha256 = "1h4zhk9rrqki193nxs9vjvya7nl9yxjcf07hfqb6g77riy1vd2jr";
42+ inherit (param) sha256;
1943 };
2044
21− patches = [
22− (fetchpatch {
23− url = "https://github.com/AbsInt/CompCert/commit/0a2db0269809539ccc66f8ec73637c37fbd23580.patch";
24− sha256 = "0n8qrba70x8f422jdvq9ddgsx6avf2dkg892g4ldh3jiiidyhspy";
25− })
26− (fetchpatch {
27− url = "https://github.com/AbsInt/CompCert/commit/5e29f8b5ba9582ecf2a1d0baeaef195873640607.patch";
28− sha256 = "184nfdgxrkci880lkaj5pgnify3plka7xfgqrgv16275sqppc5hc";
29− })
30− ];
45+ patches = param.patches or [];
3146
3247 nativeBuildInputs = [ makeWrapper ];
3348 buildInputs = ocaml-pkgs ++ [ coq coq2html ];
49+ propagatedBuildInputs = optional (param.useExternalFlocq or false) flocq;
3450 enableParallelBuilding = true;
3551
3652 postPatch = ''
@@ -43,6 +59,7 @@ stdenv.mkDerivation rec {
4359 -prefix $out \
4460 -coqdevdir $lib/lib/coq/${coq.coq-version}/user-contrib/compcert/ \
4561 -toolprefix ${tools}/bin/ \
62+ ${optionalString (param.useExternalFlocq or false) "-use-external-Flocq"} \
4663 ${ccomp-platform}
4764 '';
4865
@@ -68,7 +85,7 @@ stdenv.mkDerivation rec {
6885
6986 meta = with stdenv.lib; {
7087 description = "Formally verified C compiler";
71− homepage = "http://compcert.inria.fr";
88+ homepage = "https://compcert.org";
7289 license = licenses.inria-compcert;
7390 platforms = [ "x86_64-linux" "x86_64-darwin" ];
7491 maintainers = with maintainers; [ thoughtpolice jwiegley vbgl ];