pkgs/development/coq-modules/VST/default.nix

   1 { lib, mkCoqDerivation, coq, compcert, version ? null }:
   2
   3 with lib; mkCoqDerivation {
   4   pname = "coq${coq.coq-version}-VST";
   5   namePrefix = [];
   6   displayVersion = { coq = false; };
   7   owner = "PrincetonUniversity";
   8   repo = "VST";
   9   inherit version;
  10   defaultVersion = if coq.coq-version == "8.11" then "2.6" else null;
  11   release."2.6".sha256 = "00bf9hl4pvmsqa08lzjs1mrxyfgfxq4k6778pnldmc8ichm90jgk";
  12   releaseRev = v: "v${v}";
  13   propagatedBuildInputs = [ compcert ];
  14
  15   preConfigure = "patchShebangs util";
  16
  17   makeFlags = [
  18     "BITSIZE=64"
  19     "COMPCERT=inst_dir"
  20     "COMPCERT_INST_DIR=${compcert.lib}/lib/coq/${coq.coq-version}/user-contrib/compcert"
  21     "INSTALLDIR=$(out)/lib/coq/${coq.coq-version}/user-contrib/VST"
  22   ];
  23
  24   postInstall = ''
  25     for d in msl veric floyd sepcomp progs64
  26     do
  27       cp -r $d $out/lib/coq/${coq.coq-version}/user-contrib/VST/
  28     done
  29   '';
  30
  31   meta = {
  32     description = "Verified Software Toolchain";
  33     homepage = "https://vst.cs.princeton.edu/";
  34     inherit (compcert.meta) platforms;
  35   };
  36 }