compcert: 2.7.1 -> 3.0.1
This commit is contained in:
parent
8697fb9ec7
commit
b634622be0
@ -1,25 +1,25 @@
|
||||
{ stdenv, lib, fetchurl
|
||||
, coq, ocaml, findlib, menhir
|
||||
, coq, ocamlPackages
|
||||
, tools ? stdenv.cc
|
||||
}:
|
||||
|
||||
assert lib.versionAtLeast ocaml.version "4.02";
|
||||
assert lib.versionAtLeast ocamlPackages.ocaml.version "4.02";
|
||||
|
||||
stdenv.mkDerivation rec {
|
||||
name = "compcert-${version}";
|
||||
version = "2.7.1";
|
||||
version = "3.0.1";
|
||||
|
||||
src = fetchurl {
|
||||
url = "http://compcert.inria.fr/release/${name}.tgz";
|
||||
sha256 = "1vhbs1fmr9x2imqyd6yfvkbz763jhjfm9wk4nizf9rn1cvxrjqa4";
|
||||
sha256 = "0dgrj26dzdy4n3s9b5hwc6lm54vans1v4qx9hdp1q8w1qqcdriq9";
|
||||
};
|
||||
|
||||
buildInputs = [ coq ocaml findlib menhir ];
|
||||
buildInputs = [ coq ]
|
||||
++ (with ocamlPackages; [ ocaml findlib menhir ]);
|
||||
|
||||
enableParallelBuilding = true;
|
||||
|
||||
configurePhase = ''
|
||||
substituteInPlace ./configure --replace pl2 pl3
|
||||
substituteInPlace ./configure --replace '{toolprefix}gcc' '{toolprefix}cc'
|
||||
./configure -clightgen -prefix $out -toolprefix ${tools}/bin/ '' +
|
||||
(if stdenv.isDarwin then "ia32-macosx" else "ia32-linux");
|
||||
@ -30,7 +30,7 @@ stdenv.mkDerivation rec {
|
||||
mkdir -p $lib/share/doc/compcert
|
||||
mv doc/html $lib/share/doc/compcert/
|
||||
mkdir -p $lib/lib/coq/${coq.coq-version}/user-contrib/compcert/
|
||||
mv backend cfrontend common cparser driver flocq ia32 lib \
|
||||
mv backend cfrontend common cparser driver flocq x86 x86_32 lib \
|
||||
$lib/lib/coq/${coq.coq-version}/user-contrib/compcert/
|
||||
'';
|
||||
|
||||
|
@ -4766,7 +4766,14 @@ with pkgs;
|
||||
|
||||
cmucl_binary = callPackage_i686 ../development/compilers/cmucl/binary.nix { };
|
||||
|
||||
inherit (ocaml-ng.ocamlPackages_4_02) compcert;
|
||||
compcert = callPackage ../development/compilers/compcert ((
|
||||
if system == "x86_64-linux"
|
||||
then { tools = pkgsi686Linux.stdenv.cc; }
|
||||
else {}
|
||||
) // {
|
||||
coq = coq_8_6;
|
||||
});
|
||||
|
||||
|
||||
# Users installing via `nix-env` will likely be using the REPL,
|
||||
# which has a hard dependency on Z3, so make sure it is available.
|
||||
|
@ -671,14 +671,6 @@ let
|
||||
|
||||
wyrd = callPackage ../tools/misc/wyrd { };
|
||||
|
||||
compcert = callPackage ../development/compilers/compcert ((
|
||||
if system == "x86_64-linux"
|
||||
then { tools = pkgs.pkgsi686Linux.stdenv.cc; }
|
||||
else {}
|
||||
) // {
|
||||
coq = pkgs.coq_8_5;
|
||||
});
|
||||
|
||||
haxe = callPackage ../development/compilers/haxe { };
|
||||
|
||||
ocaml-top = callPackage ../development/tools/ocaml/ocaml-top { };
|
||||
|
Loading…
Reference in New Issue
Block a user