diff options
author | Vincent Laporte <Vincent.Laporte@gmail.com> | 2020-12-07 22:03:47 +0100 |
---|---|---|
committer | Vincent Laporte <vbgl@users.noreply.github.com> | 2020-12-09 08:28:04 +0100 |
commit | a35e7daa2b4aa70f7f8ed857f276ad33593bd322 (patch) | |
tree | 78f6476b523c38ace15cfd56da5fa56b62315c75 /pkgs/development/compilers/compcert | |
parent | 23290bd131fe33cb5844a9722662e8c458811ce3 (diff) |
compcert: 3.7 → 3.8
Diffstat (limited to 'pkgs/development/compilers/compcert')
-rw-r--r-- | pkgs/development/compilers/compcert/default.nix | 47 |
1 files changed, 32 insertions, 15 deletions
diff --git a/pkgs/development/compilers/compcert/default.nix b/pkgs/development/compilers/compcert/default.nix index 3dea91970e24e..99bd09d8d9e56 100644 --- a/pkgs/development/compilers/compcert/default.nix +++ b/pkgs/development/compilers/compcert/default.nix @@ -1,36 +1,52 @@ -{ 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 + +let param = { + "3.7" = { + sha256 = "1h4zhk9rrqki193nxs9vjvya7nl9yxjcf07hfqb6g77riy1vd2jr"; + patches = [ + (fetchpatch { + url = "https://github.com/AbsInt/CompCert/commit/0a2db0269809539ccc66f8ec73637c37fbd23580.patch"; + sha256 = "0n8qrba70x8f422jdvq9ddgsx6avf2dkg892g4ldh3jiiidyhspy"; + }) + (fetchpatch { + url = "https://github.com/AbsInt/CompCert/commit/5e29f8b5ba9582ecf2a1d0baeaef195873640607.patch"; + sha256 = "184nfdgxrkci880lkaj5pgnify3plka7xfgqrgv16275sqppc5hc"; + }) + ]; + }; + "3.8" = { + sha256 = "1gzlyxvw64ca12qql3wnq3bidcx9ygsklv9grjma3ib4hvg7vnr7"; + useExternalFlocq = true; + }; +}."${version}"; in + stdenv.mkDerivation rec { pname = "compcert"; - version = "3.7"; + inherit version; src = fetchFromGitHub { owner = "AbsInt"; repo = "CompCert"; rev = "v${version}"; - sha256 = "1h4zhk9rrqki193nxs9vjvya7nl9yxjcf07hfqb6g77riy1vd2jr"; + inherit (param) sha256; }; - patches = [ - (fetchpatch { - url = "https://github.com/AbsInt/CompCert/commit/0a2db0269809539ccc66f8ec73637c37fbd23580.patch"; - sha256 = "0n8qrba70x8f422jdvq9ddgsx6avf2dkg892g4ldh3jiiidyhspy"; - }) - (fetchpatch { - url = "https://github.com/AbsInt/CompCert/commit/5e29f8b5ba9582ecf2a1d0baeaef195873640607.patch"; - sha256 = "184nfdgxrkci880lkaj5pgnify3plka7xfgqrgv16275sqppc5hc"; - }) - ]; + 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 ]; |