blob: 382e27c45004ed99894d2332005082809873b27f (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
|
{
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".sha256 = "sha256-/IlFLiojtuENHE9d+j55Z2rYw5HUkltwVim75w/UFVE=";
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 "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;
};
}
|
