diff options
author | Théo Zimmermann <theo.zimmermann@inria.fr> | 2021-06-14 14:21:41 +0200 |
---|---|---|
committer | GitHub <noreply@github.com> | 2021-06-14 14:21:41 +0200 |
commit | 2bbf6c86876ecf75fe0ed1d8e3dff413bf255024 (patch) | |
tree | 409de0733b8a3bbb10f6a89e46385bd900e17de5 /pkgs/development/coq-modules | |
parent | 19c5fd76f885e63ee030037254cc93d1006f3387 (diff) | |
download | nixpkgs-2bbf6c86876ecf75fe0ed1d8e3dff413bf255024.tar nixpkgs-2bbf6c86876ecf75fe0ed1d8e3dff413bf255024.tar.gz nixpkgs-2bbf6c86876ecf75fe0ed1d8e3dff413bf255024.tar.bz2 nixpkgs-2bbf6c86876ecf75fe0ed1d8e3dff413bf255024.tar.lz nixpkgs-2bbf6c86876ecf75fe0ed1d8e3dff413bf255024.tar.xz nixpkgs-2bbf6c86876ecf75fe0ed1d8e3dff413bf255024.tar.zst nixpkgs-2bbf6c86876ecf75fe0ed1d8e3dff413bf255024.zip |
Move CompCert into coqPackages. (#126214)
* compcert: preparation to move in coqPackages * compcert: move into coqPackages * compcert: remove version 3.7 As a consequence, also remove VST version 2.6 These were broken.
Diffstat (limited to 'pkgs/development/coq-modules')
-rw-r--r-- | pkgs/development/coq-modules/VST/default.nix | 2 | ||||
-rw-r--r-- | pkgs/development/coq-modules/compcert/default.nix | 109 |
2 files changed, 109 insertions, 2 deletions
diff --git a/pkgs/development/coq-modules/VST/default.nix b/pkgs/development/coq-modules/VST/default.nix index ad5caec9492..c3bd33ce4bf 100644 --- a/pkgs/development/coq-modules/VST/default.nix +++ b/pkgs/development/coq-modules/VST/default.nix @@ -9,10 +9,8 @@ with lib; mkCoqDerivation { inherit version; defaultVersion = with versions; switch coq.coq-version [ { case = range "8.12" "8.13"; out = "2.7.1"; } - { case = "8.11"; out = "2.6"; } ] null; release."2.7.1".sha256 = "1674j7bkvihiv19vizm99dp6gj3lryb00zx6a87jz214f3ydcvnj"; - release."2.6".sha256 = "00bf9hl4pvmsqa08lzjs1mrxyfgfxq4k6778pnldmc8ichm90jgk"; releaseRev = v: "v${v}"; propagatedBuildInputs = [ compcert ]; diff --git a/pkgs/development/coq-modules/compcert/default.nix b/pkgs/development/coq-modules/compcert/default.nix new file mode 100644 index 00000000000..978cea5b09e --- /dev/null +++ b/pkgs/development/coq-modules/compcert/default.nix @@ -0,0 +1,109 @@ +{ lib, fetchzip, mkCoqDerivation, coq, flocq, compcert +, ocamlPackages, fetchpatch, makeWrapper, coq2html +, stdenv, tools ? stdenv.cc +, version ? null +}: + +with lib; + +let compcert = mkCoqDerivation rec { + + pname = "compcert"; + owner = "AbsInt"; + + inherit version; + releaseRev = v: "v${v}"; + + defaultVersion = with versions; switch coq.version [ + { case = range "8.8" "8.13"; out = "3.8"; } + ] null; + + release = { + "3.8".sha256 = "1gzlyxvw64ca12qql3wnq3bidcx9ygsklv9grjma3ib4hvg7vnr7"; + "3.9".sha256 = "1srcz2dqrvmbvv5cl66r34zqkm0hsbryk7gd3i9xx4slahc9zvdb"; + }; + + nativeBuildInputs = [ makeWrapper ]; + buildInputs = with ocamlPackages; [ ocaml findlib menhir menhirLib ] ++ [ coq coq2html ]; + propagatedBuildInputs = [ flocq ]; + + enableParallelBuilding = true; + + postPatch = '' + substituteInPlace ./configure \ + --replace \$\{toolprefix\}ar 'ar' \ + --replace '{toolprefix}gcc' '{toolprefix}cc' + ''; + + configurePhase = '' + ./configure -clightgen \ + -prefix $out \ + -coqdevdir $lib/lib/coq/${coq.coq-version}/user-contrib/compcert/ \ + -toolprefix ${tools}/bin/ \ + -use-external-Flocq \ + ${if stdenv.isDarwin then "x86_64-macosx" else "x86_64-linux"} + ''; + + installTargets = "documentation install"; + postInstall = '' + # 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/ + + # 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" "doc" "man" ]; + + meta = with lib; { + description = "Formally verified C compiler"; + homepage = "https://compcert.org"; + license = licenses.inria-compcert; + platforms = [ "x86_64-linux" "x86_64-darwin" ]; + maintainers = with maintainers; [ thoughtpolice jwiegley vbgl ]; + }; +}; in +compcert.overrideAttrs (o: + { + patches = with versions; switch [ coq.version o.version ] [ + { cases = [ (range "8.12.2" "8.13.2") "3.8" ]; + out = [ + # Support for Coq 8.12.2 + (fetchpatch { + url = "https://github.com/AbsInt/CompCert/commit/06956421b4307054af221c118c5f59593c0e67b9.patch"; + sha256 = "1f90q6j3xfvnf3z830bkd4d8526issvmdlrjlc95bfsqs78i1yrl"; + }) + # Support for Coq 8.13.0 + (fetchpatch { + url = "https://github.com/AbsInt/CompCert/commit/0895388e7ebf9c9f3176d225107e21968919fb97.patch"; + sha256 = "0qhkzgb2xl5kxys81pldp3mr39gd30lvr2l2wmplij319vp3xavd"; + }) + # Support for Coq 8.13.1 + (fetchpatch { + url = "https://github.com/AbsInt/CompCert/commit/6bf310dd678285dc193798e89fc2c441d8430892.patch"; + sha256 = "026ahhvpj5pksy90f8pnxgmhgwfqk4kwyvcf8x3dsanvz98d4pj5"; + }) + # Drop support for Coq < 8.9 + (fetchpatch { + url = "https://github.com/AbsInt/CompCert/commit/7563a5df926a4c6fb1489a7a4c847641c8a35095.patch"; + sha256 = "05vkslzy399r3dm6dmjs722rrajnyfa30xsyy3djl52isvn4gyfb"; + }) + # Support for Coq 8.13.2 + (fetchpatch { + url = "https://github.com/AbsInt/CompCert/commit/48bc183167c4ce01a5c9ea86e49d60530adf7290.patch"; + sha256 = "0j62lppfk26d1brdp3qwll2wi4gvpx1k70qivpvby5f7dpkrkax1"; + }) + ]; + } + ] []; + } +) |