Something went wrong. Try again.
What happens if I push all of nixpkgs
Something went wrong. Try again.
2.9 kB · 93 lines
Nix
12345678910111213141516171819202122232425262728293031323334353637383940414243444546474849505152535455565758596061626364656667686970717273747576777879808182838485868788899091929394{ lib, mkCoqDerivation, coq, compcert, ITree, version ? null,}:
# A few modules that are not built and installed by default# but that may be useful to some users.# They depend on ITree.let extra_floyd_files = [ "ASTsize.v" "io_events.v" "powerlater.v" ] # floyd/printf.v is broken in VST 2.9 ++ lib.optional (!lib.versions.isGe "8.13" coq.coq-version) "printf.v" ++ [ "quickprogram.v" ];in
mkCoqDerivation { pname = "coq${coq.coq-version}-VST"; namePrefix = [ ]; displayVersion = { coq = false; }; owner = "PrincetonUniversity"; repo = "VST"; inherit version; defaultVersion = let case = case: out: { inherit case out; }; in with lib.versions; lib.switch coq.coq-version [ (case (range "8.19" "8.20") "2.15") (case (range "8.15" "8.19") "2.14") (case (range "8.15" "8.17") "2.13") (case (range "8.14" "8.16") "2.10") (case (range "8.13" "8.15") "2.9") (case (range "8.12" "8.13") "2.8") ] null; release."2.15".sha256 = "sha256-51k2W4efMaEO4nZ0rdkRT9rA8ZJLpot1YpFmd6RIAXw="; release."2.14".sha256 = "sha256-NHc1ZQ2VmXZy4lK2+mtyeNz1Qr9Nhj2QLxkPhhQB7Iw="; release."2.13".sha256 = "sha256-i6rvP3cpayBln5KHZOpeNfraYU5h0O9uciBQ4jRH4XA="; release."2.12".sha256 = "sha256-4HL0U4HA5/usKNXC0Dis1UZY/Hb/LRd2IGOrqrvdWkw="; release."2.11.1".sha256 = "sha256-unpNstZBnRT4dIqAYOv9n1J0tWJMeRuaaa2RG1U0Xs0="; release."2.10".sha256 = "sha256-RIxfPWoHnV1CFkpxCusoGY/LIk07TgC7wWGRP4BSq8w="; release."2.9".sha256 = "sha256:1adwzbl1pprrrwrm7cm493098fizxanxpv7nyfbvwdhgbhcnv6qf"; release."2.8".sha256 = "sha256-cyK88uzorRfjapNQ6XgQEmlbWnDsiyLve5po1VG52q0="; releaseRev = v: "v${v}"; buildInputs = [ ITree ]; propagatedBuildInputs = [ compcert ];
preConfigure = '' patchShebangs util '' + lib.optionalString (coq.coq-version != null && coq.coq-version != "dev" && lib.versions.isLe "8.20" coq.coq-version) '' substituteInPlace Makefile \ --replace-fail 'COQVERSION= ' 'COQVERSION= 8.20.1 or-else 8.19.2 or-else 8.17.1 or-else 8.16.1 or-else 8.16.0 or-else 8.15.2 or-else 8.15.1 or-else '\ --replace-fail 'FLOYD_FILES=' 'FLOYD_FILES= ${toString extra_floyd_files}' '';
makeFlags = [ "BITSIZE=64" "COMPCERT=inst_dir" "COMPCERT_INST_DIR=${compcert.lib}/lib/coq/${coq.coq-version}/user-contrib/compcert" "INSTALLDIR=$(out)/lib/coq/${coq.coq-version}/user-contrib/VST" ] ++ lib.optional (coq.coq-version == "dev") "IGNORECOQVERSION=true" ++ lib.optional (coq.coq-version == "dev") "IGNORECOMPCERTVERSION=true";
postInstall = '' for d in msl veric floyd sepcomp progs64 do cp -r $d $out/lib/coq/${coq.coq-version}/user-contrib/VST/ done '';
meta = { description = "Verified Software Toolchain"; homepage = "https://vst.cs.princeton.edu/"; inherit (compcert.meta) platforms; };}