diff options
author | Vincent Laporte <Vincent.Laporte@gmail.com> | 2015-07-15 19:14:18 +0200 |
---|---|---|
committer | Vincent Laporte <Vincent.Laporte@gmail.com> | 2015-07-15 19:14:18 +0200 |
commit | 475527adb7b7cf1f0063f54f299b71a0ee720b70 (patch) | |
tree | 00d5b8b047dac8317c65f9dfb489200e4886884b /pkgs/development/compilers/compcert | |
parent | 7151be27cffc5cd8b54bc0451d3f6bb25469bb32 (diff) |
compcert: 2.4 -> 2.5
Also installs the Coq library as a separate output.
Diffstat (limited to 'pkgs/development/compilers/compcert')
-rw-r--r-- | pkgs/development/compilers/compcert/default.nix | 24 |
1 files changed, 19 insertions, 5 deletions
diff --git a/pkgs/development/compilers/compcert/default.nix b/pkgs/development/compilers/compcert/default.nix index 00a0e7b9c2b..3b1ebca1796 100644 --- a/pkgs/development/compilers/compcert/default.nix +++ b/pkgs/development/compilers/compcert/default.nix @@ -1,23 +1,37 @@ -{ stdenv, fetchurl, coq, ocaml, ocamlPackages }: +{ stdenv, fetchurl, coq, ocamlPackages +, tools ? stdenv.cc +}: stdenv.mkDerivation rec { name = "compcert-${version}"; - version = "2.4"; + version = "2.5"; src = fetchurl { url = "http://compcert.inria.fr/release/${name}.tgz"; - sha256 = "1qrb1cplx3v5wxn1c46kx67v1j52yznvjm2hkrsdybphhki2pyia"; + sha256 = "15gxarl2a8mz33fdn8pycj0ccazgmllbg2940n7aqdjlz807p11n"; }; - buildInputs = [ coq ocaml ocamlPackages.menhir ]; + buildInputs = [ coq ] ++ (with ocamlPackages; [ ocaml menhir ]); enableParallelBuilding = true; configurePhase = '' substituteInPlace ./configure --replace '{toolprefix}gcc' '{toolprefix}cc' - ./configure -prefix $out -toolprefix ${stdenv.cc}/bin/ '' + + ./configure -prefix $out -toolprefix ${tools}/bin/ '' + (if stdenv.isDarwin then "ia32-macosx" else "ia32-linux"); + installTargets = "documentation install"; + + postInstall = '' + 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 \ + $lib/lib/coq/${coq.coq-version}/user-contrib/compcert/ + ''; + + outputs = [ "out" "lib" ]; + meta = with stdenv.lib; { description = "Formally verified C compiler"; homepage = "http://compcert.inria.fr"; |