Yifei Sun
95 lines
2.7 KiB
Nix
95 lines
2.7 KiB
Nix
{
|
|
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 "9.0" "9.1") "2.16")
|
|
(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.16".hash = "sha256-/IlFLiojtuENHE9d+j55Z2rYw5HUkltwVim75w/UFVE=";
|
|
release."2.15".hash = "sha256-51k2W4efMaEO4nZ0rdkRT9rA8ZJLpot1YpFmd6RIAXw=";
|
|
release."2.14".hash = "sha256-NHc1ZQ2VmXZy4lK2+mtyeNz1Qr9Nhj2QLxkPhhQB7Iw=";
|
|
release."2.13".hash = "sha256-i6rvP3cpayBln5KHZOpeNfraYU5h0O9uciBQ4jRH4XA=";
|
|
release."2.12".hash = "sha256-4HL0U4HA5/usKNXC0Dis1UZY/Hb/LRd2IGOrqrvdWkw=";
|
|
release."2.11.1".hash = "sha256-unpNstZBnRT4dIqAYOv9n1J0tWJMeRuaaa2RG1U0Xs0=";
|
|
release."2.10".hash = "sha256-RIxfPWoHnV1CFkpxCusoGY/LIk07TgC7wWGRP4BSq8w=";
|
|
release."2.9".hash = "sha256:1adwzbl1pprrrwrm7cm493098fizxanxpv7nyfbvwdhgbhcnv6qf";
|
|
release."2.8".hash = "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 "9.1" coq.coq-version)
|
|
''
|
|
substituteInPlace Makefile \
|
|
--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"
|
|
"IGNORECOQVERSION=true"
|
|
"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;
|
|
};
|
|
}
|