tjh.dev
1{
2 lib,
3 mkCoqDerivation,
4 coq,
5 compcert,
6 ITree,
7 version ? null,
8}:
9
10# A few modules that are not built and installed by default
11# but that may be useful to some users.
12# They depend on ITree.
13let
14 extra_floyd_files = [
15 "ASTsize.v"
16 "io_events.v"
17 "powerlater.v"
18 ]
19 # floyd/printf.v is broken in VST 2.9
20 ++ lib.optional (!lib.versions.isGe "8.13" coq.coq-version) "printf.v"
21 ++ [
22 "quickprogram.v"
23 ];
24in
25
26mkCoqDerivation {
27 pname = "coq${coq.coq-version}-VST";
28 namePrefix = [ ];
29 displayVersion = {
30 coq = false;
31 };
32 owner = "PrincetonUniversity";
33 repo = "VST";
34 inherit version;
35 defaultVersion =
36 let
37 case = case: out: { inherit case out; };
38 in
39 with lib.versions;
40 lib.switch coq.coq-version [
41 (case (range "8.19" "8.20") "2.15")
42 (case (range "8.15" "8.19") "2.14")
43 (case (range "8.15" "8.17") "2.13")
44 (case (range "8.14" "8.16") "2.10")
45 (case (range "8.13" "8.15") "2.9")
46 (case (range "8.12" "8.13") "2.8")
47 ] null;
48 release."2.15".sha256 = "sha256-51k2W4efMaEO4nZ0rdkRT9rA8ZJLpot1YpFmd6RIAXw=";
49 release."2.14".sha256 = "sha256-NHc1ZQ2VmXZy4lK2+mtyeNz1Qr9Nhj2QLxkPhhQB7Iw=";
50 release."2.13".sha256 = "sha256-i6rvP3cpayBln5KHZOpeNfraYU5h0O9uciBQ4jRH4XA=";
51 release."2.12".sha256 = "sha256-4HL0U4HA5/usKNXC0Dis1UZY/Hb/LRd2IGOrqrvdWkw=";
52 release."2.11.1".sha256 = "sha256-unpNstZBnRT4dIqAYOv9n1J0tWJMeRuaaa2RG1U0Xs0=";
53 release."2.10".sha256 = "sha256-RIxfPWoHnV1CFkpxCusoGY/LIk07TgC7wWGRP4BSq8w=";
54 release."2.9".sha256 = "sha256:1adwzbl1pprrrwrm7cm493098fizxanxpv7nyfbvwdhgbhcnv6qf";
55 release."2.8".sha256 = "sha256-cyK88uzorRfjapNQ6XgQEmlbWnDsiyLve5po1VG52q0=";
56 releaseRev = v: "v${v}";
57 buildInputs = [ ITree ];
58 propagatedBuildInputs = [ compcert ];
59
60 preConfigure = ''
61 patchShebangs util
62 ''
63 +
64 lib.optionalString
65 (coq.coq-version != null && coq.coq-version != "dev" && lib.versions.isLe "8.20" coq.coq-version)
66 ''
67 substituteInPlace Makefile \
68 --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 '\
69 --replace-fail 'FLOYD_FILES=' 'FLOYD_FILES= ${toString extra_floyd_files}'
70 '';
71
72 makeFlags = [
73 "BITSIZE=64"
74 "COMPCERT=inst_dir"
75 "COMPCERT_INST_DIR=${compcert.lib}/lib/coq/${coq.coq-version}/user-contrib/compcert"
76 "INSTALLDIR=$(out)/lib/coq/${coq.coq-version}/user-contrib/VST"
77 ]
78 ++ lib.optional (coq.coq-version == "dev") "IGNORECOQVERSION=true"
79 ++ lib.optional (coq.coq-version == "dev") "IGNORECOMPCERTVERSION=true";
80
81 postInstall = ''
82 for d in msl veric floyd sepcomp progs64
83 do
84 cp -r $d $out/lib/coq/${coq.coq-version}/user-contrib/VST/
85 done
86 '';
87
88 meta = {
89 description = "Verified Software Toolchain";
90 homepage = "https://vst.cs.princeton.edu/";
91 inherit (compcert.meta) platforms;
92 };
93}