|
|
|
@ -1,5 +1,7 @@ |
|
|
|
|
{ lib, mkCoqDerivation, coq, compcert, ITree, version ? null }: |
|
|
|
|
|
|
|
|
|
with lib; |
|
|
|
|
|
|
|
|
|
# A few modules that are not built and installed by default |
|
|
|
|
# but that may be useful to some users. |
|
|
|
|
# They depend on ITree. |
|
|
|
@ -7,12 +9,15 @@ let extra_floyd_files = [ |
|
|
|
|
"ASTsize.v" |
|
|
|
|
"io_events.v" |
|
|
|
|
"powerlater.v" |
|
|
|
|
"printf.v" |
|
|
|
|
] |
|
|
|
|
# floyd/printf.v is broken in VST 2.9 |
|
|
|
|
++ optional (!versions.isGe "8.13" coq.coq-version) "printf.v" |
|
|
|
|
++ [ |
|
|
|
|
"quickprogram.v" |
|
|
|
|
]; |
|
|
|
|
in |
|
|
|
|
|
|
|
|
|
with lib; mkCoqDerivation { |
|
|
|
|
mkCoqDerivation { |
|
|
|
|
pname = "coq${coq.coq-version}-VST"; |
|
|
|
|
namePrefix = []; |
|
|
|
|
displayVersion = { coq = false; }; |
|
|
|
@ -20,8 +25,10 @@ with lib; mkCoqDerivation { |
|
|
|
|
repo = "VST"; |
|
|
|
|
inherit version; |
|
|
|
|
defaultVersion = with versions; switch coq.coq-version [ |
|
|
|
|
{ case = range "8.13" "8.15"; out = "2.9"; } |
|
|
|
|
{ case = range "8.12" "8.13"; out = "2.8"; } |
|
|
|
|
] null; |
|
|
|
|
release."2.9".sha256 = "sha256:1adwzbl1pprrrwrm7cm493098fizxanxpv7nyfbvwdhgbhcnv6qf"; |
|
|
|
|
release."2.8".sha256 = "sha256-cyK88uzorRfjapNQ6XgQEmlbWnDsiyLve5po1VG52q0="; |
|
|
|
|
releaseRev = v: "v${v}"; |
|
|
|
|
extraBuildInputs = [ ITree ]; |
|
|
|
|