Merge pull request #131828 from vbgl/coq-VST-io_events

{ lib, mkCoqDerivation, coq, compcert, version ? null }:

{ lib, mkCoqDerivation, coq, compcert, ITree, version ? null }:

# A few modules that are not built and installed by default

#  but that may be useful to some users.

# They depend on ITree.

let extra_floyd_files = [

  "ASTsize.v"

  "io_events.v"

  "powerlater.v"

  "printf.v"

  "quickprogram.v"

  ];

in

with lib; mkCoqDerivation {

  pname = "coq${coq.coq-version}-VST";

  ] null;

  release."2.8".sha256 = "sha256-cyK88uzorRfjapNQ6XgQEmlbWnDsiyLve5po1VG52q0=";

  releaseRev = v: "v${v}";

  extraBuildInputs = [ ITree ];

  propagatedBuildInputs = [ compcert ];

  preConfigure = "patchShebangs util";

  preConfigure = ''

    patchShebangs util

    substituteInPlace Makefile \

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

  '';

  makeFlags = [

    "BITSIZE=64"