Commit 2107c026 authored by Pierre Roux's avatar Pierre Roux Committed by Vincent Laporte
Browse files

coqPackages.VST: adapt to master

parent 82bf4690

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

+30 −36
Original line number Diff line number Diff line
@@ -34,32 +34,17 @@ mkCoqDerivation { 
  repo = "VST";

  inherit version;

  defaultVersion =

    let

      case = case: out: { inherit case out; };

    in

    with lib.versions;

    lib.switch coq.coq-version [

      {

        case = range "8.19" "8.20";

        out = "2.15";

      }

      {

        case = range "8.15" "8.19";

        out = "2.14";

      }

      {

        case = range "8.15" "8.17";

        out = "2.13";

      }

      {

        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";

      }

      (case (range "8.19" "8.20") "2.15")

      (case (range "8.15" "8.19") "2.14")

      (case (range "8.15" "8.17") "2.13")

      (case (range "8.14" "8.16") "2.10")

      (case (range "8.13" "8.15") "2.9")

      (case (range "8.12" "8.13") "2.8")

    ] null;

  release."2.15".sha256 = "sha256-51k2W4efMaEO4nZ0rdkRT9rA8ZJLpot1YpFmd6RIAXw=";

  release."2.14".sha256 = "sha256-NHc1ZQ2VmXZy4lK2+mtyeNz1Qr9Nhj2QLxkPhhQB7Iw=";
@@ -73,19 +58,28 @@ mkCoqDerivation { 
  buildInputs = [ ITree ];

  propagatedBuildInputs = [ compcert ];



  preConfigure = ''

  preConfigure =

    ''

      patchShebangs util

    ''

    +

      lib.optionalString

        (coq.coq-version != null && coq.coq-version != "dev" && lib.versions.isLe "8.20" coq.coq-version)

        ''

          substituteInPlace Makefile \

      --replace '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 '\

      --replace 'FLOYD_FILES=' 'FLOYD_FILES= ${toString extra_floyd_files}'

            --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 '\

            --replace-fail 'FLOYD_FILES=' 'FLOYD_FILES= ${toString extra_floyd_files}'

        '';



  makeFlags = [

  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"

  ];

    ]

    ++ lib.optional (coq.coq-version == "dev") "IGNORECOQVERSION=true"

    ++ lib.optional (coq.coq-version == "dev") "IGNORECOMPCERTVERSION=true";



  postInstall = ''

    for d in msl veric floyd sepcomp progs64