haskellPackages.sbv: fix tests

By patching paths of the external provers and excluding not available
provers from the test.

ZHF: #97479
This commit is contained in:
Kai Harries 2020-09-14 06:43:11 +02:00 committed by Peter Simons
parent eb523e8663
commit f40afea417
1 changed files with 12 additions and 1 deletions

View File

@ -571,9 +571,20 @@ self: super: builtins.intersectAttrs super {
}));
# Expects z3 to be on path so we replace it with a hard
#
# The tests expect additional solvers on the path, replace the
# available ones also with hard coded paths, and remove the missing
# ones from the test.
sbv = overrideCabal super.sbv (drv: {
postPatch = ''
sed -i -e 's|"z3"|"${pkgs.z3}/bin/z3"|' Data/SBV/Provers/Z3.hs'';
sed -i -e 's|"abc"|"${pkgs.abc-verifier}/bin/abc"|' Data/SBV/Provers/ABC.hs
sed -i -e 's|"boolector"|"${pkgs.boolector}/bin/boolector"|' Data/SBV/Provers/Boolector.hs
sed -i -e 's|"cvc4"|"${pkgs.cvc4}/bin/cvc4"|' Data/SBV/Provers/CVC4.hs
sed -i -e 's|"yices-smt2"|"${pkgs.yices}/bin/yices-smt2"|' Data/SBV/Provers/Yices.hs
sed -i -e 's|"z3"|"${pkgs.z3}/bin/z3"|' Data/SBV/Provers/Z3.hs
sed -i -e 's|\[abc, boolector, cvc4, mathSAT, yices, z3, dReal\]|[abc, boolector, cvc4, yices, z3]|' SBVTestSuite/SBVConnectionTest.hs
'';
});
# The test-suite requires a running PostgreSQL server.