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