diff options
Diffstat (limited to 'pkgs/development/coq-modules/VST/default.nix')
| -rw-r--r-- | pkgs/development/coq-modules/VST/default.nix | 21 |
1 files changed, 19 insertions, 2 deletions
diff --git a/pkgs/development/coq-modules/VST/default.nix b/pkgs/development/coq-modules/VST/default.nix index 5ee1df77418..1d2a1a3c05f 100644 --- a/pkgs/development/coq-modules/VST/default.nix +++ b/pkgs/development/coq-modules/VST/default.nix @@ -1,4 +1,16 @@ -{ 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"; @@ -12,9 +24,14 @@ with lib; mkCoqDerivation { ] 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" |