blob: 150148cfe00d3b982b6f849bb4203db14cf1db25 (
plain) (
blame)
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
|
{ 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 = with lib.versions; lib.switch coq.coq-version [
{ case = range "8.15" "8.17"; out = "2.12"; }
{ case = range "8.14" "8.16"; out = "2.10"; }
{ case = range "8.13" "8.15"; out = "2.9"; }
{ case = range "8.12" "8.13"; out = "2.8"; }
] null;
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
substituteInPlace Makefile \
--replace 'COQVERSION= ' 'COQVERSION= 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 '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"
];
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;
};
}
|