git.iko.soy/typeable/nixpkgs
on master help sign in
coqPackages.VST: init at 2.6
d5f1dceVincent Laporte
pkgs/development/coq-modules/VST/default.nixnew file+43
compare with master
unifiedsplit
@@ -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+}
pkgs/top-level/coq-packages.nix+1
@@ -59,6 +59,7 @@ let
59 tlc = callPackage ../development/coq-modules/tlc {};
59 tlc = callPackage ../development/coq-modules/tlc {};
60 Velisarios = callPackage ../development/coq-modules/Velisarios {};
60 Velisarios = callPackage ../development/coq-modules/Velisarios {};
61 Verdi = callPackage ../development/coq-modules/Verdi {};
61 Verdi = callPackage ../development/coq-modules/Verdi {};
62+ VST = callPackage ../development/coq-modules/VST {};
62
63
63 filterPackages = filterCoqPackages;
64 filterPackages = filterCoqPackages;
64 };
65 };