diff options
author | Austin Seipp <aseipp@pobox.com> | 2019-01-12 18:37:30 -0600 |
---|---|---|
committer | Austin Seipp <aseipp@pobox.com> | 2019-01-12 20:06:28 -0600 |
commit | 53fb3bb3ef297314141fd0041922846d63e05925 (patch) | |
tree | 704c779d532ad552b000e5263b483b7adca56b1f /pkgs/development/compilers/compcert | |
parent | 570d84a01eb5d511b1d5b75162e97c1c347d49f2 (diff) | |
download | nixpkgs-53fb3bb3ef297314141fd0041922846d63e05925.tar nixpkgs-53fb3bb3ef297314141fd0041922846d63e05925.tar.gz nixpkgs-53fb3bb3ef297314141fd0041922846d63e05925.tar.bz2 nixpkgs-53fb3bb3ef297314141fd0041922846d63e05925.tar.lz nixpkgs-53fb3bb3ef297314141fd0041922846d63e05925.tar.xz nixpkgs-53fb3bb3ef297314141fd0041922846d63e05925.tar.zst nixpkgs-53fb3bb3ef297314141fd0041922846d63e05925.zip |
compcert: clean up expression
- Require Coq 8.6.1+ - Split substituteInPlace call into patchPhase - Constrain platforms correctly to x86_64 Linux/Darwin, which was all it supported anyway (there was no way to properly configure i686 builds, nor cross builds. In the future there might be) - Minor stylistic cleanups - Add new 'man' and 'doc' outputs (the previous attempt to move the build artifact outputs into $lib no longer worked correctly and they were installed into 'out' instead, this fixes it completely). - Clean up weird binary artifacts left in $out (that were already in $lib) - Wrap ccomp to undefine _FORTIFY_SOURCE; otherwise it causes annoying warnings on every invocation Signed-off-by: Austin Seipp <aseipp@pobox.com>
Diffstat (limited to 'pkgs/development/compilers/compcert')
-rw-r--r-- | pkgs/development/compilers/compcert/default.nix | 50 |
1 files changed, 37 insertions, 13 deletions
diff --git a/pkgs/development/compilers/compcert/default.nix b/pkgs/development/compilers/compcert/default.nix index a0058242bad..4a9f585b252 100644 --- a/pkgs/development/compilers/compcert/default.nix +++ b/pkgs/development/compilers/compcert/default.nix @@ -1,10 +1,15 @@ -{ stdenv, lib, fetchurl, fetchpatch +{ stdenv, lib, fetchurl, fetchpatch, makeWrapper , coq, ocamlPackages, coq2html , tools ? stdenv.cc }: assert lib.versionAtLeast ocamlPackages.ocaml.version "4.02"; +assert lib.versionAtLeast coq.coq-version "8.6.1"; +let + ocaml-pkgs = with ocamlPackages; [ ocaml findlib menhir ]; + ccomp-platform = if stdenv.isDarwin then "x86_64-macosx" else "x86_64-linux"; +in stdenv.mkDerivation rec { name = "compcert-${version}"; version = "3.4"; @@ -14,34 +19,53 @@ stdenv.mkDerivation rec { sha256 = "12gchwvkzhd2bhrnwzfb4a06wc4hgv98z987k06vj7ga31ii763h"; }; - buildInputs = [ coq coq2html ] - ++ (with ocamlPackages; [ ocaml findlib menhir ]); - + nativeBuildInputs = [ makeWrapper ]; + buildInputs = ocaml-pkgs ++ [ coq coq2html ]; enableParallelBuilding = true; + patchPhase = '' + substituteInPlace ./configure \ + --replace '{toolprefix}gcc' '{toolprefix}cc' + ''; + configurePhase = '' - substituteInPlace ./configure --replace '{toolprefix}gcc' '{toolprefix}cc' - ./configure -clightgen -prefix $out -toolprefix ${tools}/bin/ '' + - (if stdenv.isDarwin then "x86_64-macosx" else "x86_64-linux"); + ./configure -clightgen \ + -prefix $out \ + -toolprefix ${tools}/bin/ \ + ${ccomp-platform} + ''; installTargets = "documentation install"; - postInstall = '' - mkdir -p $lib/share/doc/compcert - mv doc/html $lib/share/doc/compcert/ + # move man into place + mkdir -p $man/share + mv $out/share/man/ $man/share/ + + # move docs into place + mkdir -p $doc/share/doc/compcert + mv doc/html $doc/share/doc/compcert/ + + # install compcert lib files; remove copy from $out, too mkdir -p $lib/lib/coq/${coq.coq-version}/user-contrib/compcert/ mv backend cfrontend common cparser driver flocq x86 x86_64 lib \ $lib/lib/coq/${coq.coq-version}/user-contrib/compcert/ + rm -rf $out/lib/compcert/coq + + # wrap ccomp to undefine _FORTIFY_SOURCE; ccomp invokes cc1 which sets + # _FORTIFY_SOURCE=2 by default, but undefines __GNUC__ (as it should), + # which causes a warning in libc. this suppresses it. + for x in ccomp clightgen; do + wrapProgram $out/bin/$x --add-flags "-U_FORTIFY_SOURCE" + done ''; - outputs = [ "out" "lib" ]; + outputs = [ "out" "lib" "doc" "man" ]; meta = with stdenv.lib; { description = "Formally verified C compiler"; homepage = "http://compcert.inria.fr"; license = licenses.inria-compcert; - platforms = platforms.linux ++ - platforms.darwin; + platforms = [ "x86_64-linux" "x86_64-darwin" ]; maintainers = with maintainers; [ thoughtpolice jwiegley vbgl ]; }; } |