[Git][haskell-team/DHG_packages][master] what4: Disable tests
Ilias Tsitsimpis (@iliastsi)
gitlab at salsa.debian.org
Sat Nov 4 11:49:31 GMT 2023
Ilias Tsitsimpis pushed to branch master at Debian Haskell Group / DHG_packages
Commits:
6e5bfbec by Ilias Tsitsimpis at 2023-11-04T13:43:01+02:00
what4: Disable tests
- - - - -
7 changed files:
- p/haskell-what4/debian/changelog
- p/haskell-what4/debian/control
- − p/haskell-what4/debian/patches/disable-tests-non-x86_64
- − p/haskell-what4/debian/patches/disable-tests-yices
- − p/haskell-what4/debian/patches/no-tasty-sugar
- − p/haskell-what4/debian/patches/series
- p/haskell-what4/debian/rules
Changes:
=====================================
p/haskell-what4/debian/changelog
=====================================
@@ -1,3 +1,9 @@
+haskell-what4 (1.5.1-3) unstable; urgency=medium
+
+ * Disable tests (Closes: #1054704)
+
+ -- Ilias Tsitsimpis <iliastsi at debian.org> Sat, 04 Nov 2023 13:41:56 +0200
+
haskell-what4 (1.5.1-2) unstable; urgency=medium
* Build-Depend on both cvc4 and cvc5 for testsuite.
=====================================
p/haskell-what4/debian/control
=====================================
@@ -6,7 +6,7 @@ Section: haskell
Build-Depends: debhelper (>= 10),
haskell-devscripts-minimal | haskell-devscripts (>= 0.13),
cdbs,
- ghc,
+ ghc (>= 9.4),
ghc-prof,
libghc-boundedchan-dev (>= 1),
libghc-boundedchan-dev (<< 2),
@@ -101,39 +101,6 @@ Build-Depends: debhelper (>= 10),
libghc-zenc-dev (>= 0.1.0),
libghc-zenc-dev (<< 0.2.0),
libghc-zenc-prof,
- libghc-parameterized-utils-dev,
- cvc4,
- cvc5,
- z3,
- libghc-quickcheck2-dev (>= 2.12),
- libghc-quickcheck2-prof,
- libghc-bv-sized-dev,
- libghc-contravariant-dev,
- libghc-contravariant-prof,
- libghc-hedgehog-dev (>= 1.0.2),
- libghc-hedgehog-prof,
- libghc-io-streams-dev,
- libghc-libbf-dev,
- libghc-lumberjack-dev,
- libghc-lumberjack-prof,
- libghc-ordered-containers-dev,
- libghc-prettyprinter-dev,
- libghc-tasty-dev (>= 0.10),
- libghc-tasty-prof,
- libghc-tasty-checklist-dev (>= 1.0.3),
- libghc-tasty-checklist-dev (<< 1.1),
- libghc-tasty-checklist-prof,
- libghc-tasty-expected-failure-dev (>= 0.12),
- libghc-tasty-expected-failure-dev (<< 0.13),
- libghc-tasty-expected-failure-prof,
- libghc-tasty-hedgehog-dev (>= 1.2),
- libghc-tasty-hedgehog-prof,
- libghc-tasty-hunit-dev (>= 0.9),
- libghc-tasty-hunit-prof,
- libghc-tasty-quickcheck-dev (>= 0.10),
- libghc-tasty-quickcheck-prof,
- libghc-temporary-dev,
- libghc-versions-dev,
Build-Depends-Indep: ghc-doc,
libghc-boundedchan-doc,
libghc-async-doc,
=====================================
p/haskell-what4/debian/patches/disable-tests-non-x86_64 deleted
=====================================
@@ -1,24 +0,0 @@
---- a/what4.cabal
-+++ b/what4.cabal
-@@ -353,6 +353,10 @@ test-suite expr-builder-smtlib2
- tasty-checklist >= 1.0.3 && < 1.1,
- text,
- versions
-+ if arch(x86_64)
-+ buildable: True
-+ else
-+ buildable: False
-
-
- test-suite exprs_tests
-@@ -411,6 +415,10 @@ test-suite template_tests
- build-depends: bv-sized
- , libBF
- , transformers
-+ if arch(x86_64)
-+ buildable: True
-+ else
-+ buildable: False
-
- test-suite what4-serialize-tests
- default-language: Haskell2010
=====================================
p/haskell-what4/debian/patches/disable-tests-yices deleted
=====================================
@@ -1,78 +0,0 @@
---- a/test/ExprBuilderSMTLib2.hs
-+++ b/test/ExprBuilderSMTLib2.hs
-@@ -1159,39 +1159,13 @@ testUnsafeSetAbstractValue2 = testCase "
- , "compound symbolic expression"
- ]
-
--testResolveSymBV :: WURB.SearchStrategy -> TestTree
--testResolveSymBV searchStrat =
-- testProperty ("test resolveSymBV (" ++ show (PP.pretty searchStrat) ++ ")") $
-- H.property $ do
-- let w = knownNat @8
-- lb <- H.forAll $ HGen.word8 $ HRange.constant 0 maxBound
-- ub <- H.forAll $ HGen.word8 $ HRange.constant lb maxBound
--
-- rbv <- liftIO $ withYices $ \sym proc -> do
-- bv <- freshConstant sym (safeSymbol "bv") knownRepr
-- p1 <- bvUge sym bv =<< bvLit sym w (BV.mkBV w (toInteger lb))
-- p2 <- bvUle sym bv =<< bvLit sym w (BV.mkBV w (toInteger ub))
-- p3 <- andPred sym p1 p2
-- assume (solverConn proc) p3
-- WURB.resolveSymBV sym searchStrat w proc bv
--
-- case rbv of
-- WURB.BVConcrete bv -> do
-- let bv' = fromInteger $ BV.asUnsigned bv
-- lb H.=== bv'
-- ub H.=== bv'
-- WURB.BVSymbolic bounds -> do
-- let (lb', ub') = WUBA.ubounds bounds
-- lb H.=== fromInteger lb'
-- ub H.=== fromInteger ub'
--
- ----------------------------------------------------------------------
-
-
- main :: IO ()
- main = do
- testLevel <- TestLevel . fromMaybe "0" <$> lookupEnv "CI_TEST_LEVEL"
-- let solverNames = SolverName <$> [ "cvc4", "cvc5", "yices", "z3" ]
-+ let solverNames = SolverName <$> [ "cvc4", "cvc5", "z3" ]
- solvers <- reportSolverVersions testLevel id
- =<< (zip solverNames <$> mapM getSolverVersion solverNames)
- let z3Tests =
-@@ -1278,17 +1252,6 @@ main = do
-
- , testCase "CVC4 #182 test case" $ withCVC4 issue182Test
- ]
-- let yicesTests =
-- [
-- testResolveSymBV WURB.ExponentialSearch
-- , testResolveSymBV WURB.BinarySearch
--
-- , testCase "Yices 0-tuple" $ withYices zeroTupleTest
-- , testCase "Yices 1-tuple" $ withYices oneTupleTest
-- , testCase "Yices pair" $ withYices pairTest
-- , testCase "Yices rounding" $ withYices roundingTest
-- , testCase "Yices #182 test case" $ withYices issue182Test
-- ]
- let cvc5Tests = cvc4Tests
- let skipIfNotPresent nm = if SolverName nm `elem` (fst <$> solvers) then id
- else fmap (ignoreTestBecause (nm <> " not present"))
-@@ -1311,5 +1274,4 @@ main = do
- ]
- <> (skipIfNotPresent "cvc4" cvc4Tests)
- <> (skipIfNotPresent "cvc5" cvc5Tests)
-- <> (skipIfNotPresent "yices" yicesTests)
- <> (skipIfNotPresent "z3" z3Tests)
---- a/test/OnlineSolverTest.hs
-+++ b/test/OnlineSolverTest.hs
-@@ -61,8 +61,6 @@ allOnlineSolvers =
- , AnOnlineSolver @(SMT2.Writer CVC4) Proxy, cvc4Features, cvc4Options, Just cvc4Timeout)
- , (SolverName "CVC5"
- , AnOnlineSolver @(SMT2.Writer CVC5) Proxy, cvc5Features, cvc5Options, Just cvc5Timeout)
-- , (SolverName "Yices"
-- , AnOnlineSolver @Yices.Connection Proxy, yicesDefaultFeatures, yicesOptions, Just yicesGoalTimeout)
- , (SolverName "Boolector"
- , AnOnlineSolver @(SMT2.Writer Boolector) Proxy, boolectorFeatures, boolectorOptions, Just boolectorTimeout)
- #ifdef TEST_STP
=====================================
p/haskell-what4/debian/patches/no-tasty-sugar deleted
=====================================
@@ -1,21 +0,0 @@
---- a/what4.cabal
-+++ b/what4.cabal
-@@ -412,18 +412,6 @@ test-suite template_tests
- , libBF
- , transformers
-
--
--test-suite solver_parsing_tests
-- import: bldflags, testdefs-hunit
-- type: exitcode-stdio-1.0
-- main-is : SolverParserTest.hs
-- build-depends: contravariant
-- , exceptions
-- , io-streams
-- , lumberjack
-- , tasty-sugar >= 2.0 && < 2.3
-- , text
--
- test-suite what4-serialize-tests
- default-language: Haskell2010
- type: exitcode-stdio-1.0
=====================================
p/haskell-what4/debian/patches/series deleted
=====================================
@@ -1,3 +0,0 @@
-no-tasty-sugar
-disable-tests-non-x86_64
-disable-tests-yices
=====================================
p/haskell-what4/debian/rules
=====================================
@@ -1,9 +1,9 @@
#!/usr/bin/make -f
-DEB_ENABLE_TESTS = yes
-DEB_SETUP_BIN_NAME = debian/hlibrary.setup
-DEB_CABAL_PACKAGE = what4
-DEB_DEFAULT_COMPILER = ghc
+# Tests for CVC4 fail on Debian, because the cvc4 binary in Debian is
+# compiled without symfpu support.
+# https://github.com/GaloisInc/what4-solvers/issues/23
+DEB_ENABLE_TESTS = no
include /usr/share/cdbs/1/rules/debhelper.mk
include /usr/share/cdbs/1/class/hlibrary.mk
View it on GitLab: https://salsa.debian.org/haskell-team/DHG_packages/-/commit/6e5bfbec15ce28be16f1487244af295d2245055d
--
View it on GitLab: https://salsa.debian.org/haskell-team/DHG_packages/-/commit/6e5bfbec15ce28be16f1487244af295d2245055d
You're receiving this email because of your account on salsa.debian.org.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://alioth-lists.debian.net/pipermail/pkg-haskell-commits/attachments/20231104/01b66d6b/attachment-0001.htm>
More information about the Pkg-haskell-commits
mailing list