From f40afea4178949c171d37f9114b552185fca7010 Mon Sep 17 00:00:00 2001 From: Kai Harries Date: Mon, 14 Sep 2020 06:43:11 +0200 Subject: [PATCH] haskellPackages.sbv: fix tests By patching paths of the external provers and excluding not available provers from the test. ZHF: #97479 --- .../haskell-modules/configuration-nix.nix | 13 ++++++++++++- 1 file changed, 12 insertions(+), 1 deletion(-) diff --git a/pkgs/development/haskell-modules/configuration-nix.nix b/pkgs/development/haskell-modules/configuration-nix.nix index cff7cc2cd80..a1938de0ab3 100644 --- a/pkgs/development/haskell-modules/configuration-nix.nix +++ b/pkgs/development/haskell-modules/configuration-nix.nix @@ -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.