[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