@@ -0,0 +1,43 @@
1+{ stdenv, fetchFromGitHub, coq, compcert }:
2+
3+stdenv.mkDerivation rec {
4+ pname = "coq${coq.coq-version}-VST";
5+ version = "2.6";
6+
7+ src = fetchFromGitHub {
8+ owner = "PrincetonUniversity";
9+ repo = "VST";
10+ rev = "v${version}";
11+ sha256 = "00bf9hl4pvmsqa08lzjs1mrxyfgfxq4k6778pnldmc8ichm90jgk";
12+ };
13+
14+ buildInputs = [ coq ];
15+ propagatedBuildInputs = [ compcert ];
16+
17+ preConfigure = "patchShebangs util";
18+
19+ makeFlags = [
20+ "BITSIZE=64"
21+ "COMPCERT=inst_dir"
22+ "COMPCERT_INST_DIR=${compcert.lib}/lib/coq/${coq.coq-version}/user-contrib/compcert"
23+ "INSTALLDIR=$(out)/lib/coq/${coq.coq-version}/user-contrib/VST"
24+ ];
25+
26+ postInstall = ''
27+ for d in msl veric floyd sepcomp progs64
28+ do
29+ cp -r $d $out/lib/coq/${coq.coq-version}/user-contrib/VST/
30+ done
31+ '';
32+
33+ enableParallelBuilding = true;
34+
35+ passthru.compatibleCoqVersions = stdenv.lib.flip builtins.elem [ "8.11" ];
36+
37+ meta = {
38+ description = "Verified Software Toolchain";
39+ homepage = "https://vst.cs.princeton.edu/";
40+ inherit (compcert.meta) platforms;
41+ };
42+
43+}