diff --git a/CHANGES.md b/CHANGES.md index 8c316a4..1485809 100644 --- a/CHANGES.md +++ b/CHANGES.md @@ -1,7 +1,11 @@ * Hackage: * GitHub: -* Latest Hackage released version: 9.8.1, 2024-01-05 +* Latest Hackage released version: 9.8.2, 2024-03-23 + +### Version 9.8.2, 2024-01-05 + * Changes required to compile with GHC 9.8.2 + * Bump up sbv dependence to >= 10.7 ### Version 9.8.1, 2024-01-05 * Changes required to compile with GHC 9.8.1 diff --git a/Makefile b/Makefile index 9382dc8..6126ccb 100644 --- a/Makefile +++ b/Makefile @@ -33,7 +33,7 @@ docs: cabal new-haddock --haddock-for-hackage --enable-doc --haddock-option="--optghc=-DHADDOCK" upload-docs-to-hackage: - cabal upload -d --publish ./dist-newstyle/sbvPlugin-9.8.1-docs.tar.gz + cabal upload -d --publish ./dist-newstyle/sbvPlugin-9.8.2-docs.tar.gz # use this as follows: make gold TGT=T49 gold: diff --git a/sbvPlugin.cabal b/sbvPlugin.cabal index 4769f57..c005183 100644 --- a/sbvPlugin.cabal +++ b/sbvPlugin.cabal @@ -1,6 +1,6 @@ Cabal-Version : 2.2 Name : sbvPlugin -Version : 9.8.1 +Version : 9.8.2 Category : Formal methods, Theorem provers, Math, SMT, Symbolic Computation Synopsis : Formally prove properties of Haskell programs using SBV/SMT Description : GHC plugin for proving properties over Haskell functions using SMT solvers, based @@ -18,7 +18,7 @@ Maintainer : Levent Erkok (erkokl@gmail.com) Build-Type : Simple Extra-Source-Files: INSTALL, README.md, COPYRIGHT, CHANGES.md -Tested-With : GHC==9.8.1 +Tested-With : GHC==9.8.2 source-repository head type: git @@ -34,8 +34,8 @@ Library , Data.SBV.Plugin.Examples.MergeSort , Data.SBV.Plugin.Examples.MicroController build-depends : base >= 4.19 && < 5 - , sbv >= 10.3 - , ghc >= 9.8.1 + , sbv >= 10.7 + , ghc >= 9.8.2 , ghc-prim , containers , mtl diff --git a/tests/GoldFiles/T16.hs.golden b/tests/GoldFiles/T16.hs.golden index eb0b1f6..14ba2ee 100644 --- a/tests/GoldFiles/T16.hs.golden +++ b/tests/GoldFiles/T16.hs.golden @@ -2,8 +2,8 @@ Loaded package environment from test-modified path [SBV] tests/T16.hs:11:1 Proving "f", using Z3. [Z3] Falsifiable. Counter-example: - ds_daqd = 0 :: Int64 + ds_dap7 = 0 :: Int64 age = Age!val!0 :: Age [SBV] Counter-example might be bogus due to uninterpreted constant: - [] ds_daqd :: Int + [] ds_dap7 :: Int [SBV] Failed. (Use option 'IgnoreFailure' to continue.) diff --git a/tests/GoldFiles/T46.hs.golden b/tests/GoldFiles/T46.hs.golden index 125ad4a..2ea8705 100644 --- a/tests/GoldFiles/T46.hs.golden +++ b/tests/GoldFiles/T46.hs.golden @@ -2,17 +2,17 @@ Loaded package environment from test-modified path [SBV] tests/T46.hs:22:1-10 Proving "filtLenBad", using Z3. [Z3] Falsifiable. Counter-example: - xs_1 = 1898904026880687412 :: Int64 - xs_2 = -1898904026880687413 :: Int64 - xs_3 = 967593163855872713 :: Int64 - xs_4 = 1892166082921774645 :: Int64 - xs_5 = -3384346643702766540 :: Int64 + xs_1 = 1896580642610626484 :: Int64 + xs_2 = -1896580642610626485 :: Int64 + xs_3 = 2122839034131759177 :: Int64 + xs_4 = 1896667638314056885 :: Int64 + xs_5 = -3347824179180231500 :: Int64 f :: Int64 -> Bool - f 967593163855872713 = True - f 1892166082921774645 = True - f 1898904026880687412 = True - f _ = False + f (-3347824179180231500) = True + f 1896667638314056885 = True + f 1896580642610626484 = True + f _ = False [SBV] tests/T46.hs:26:1-11 Proving "filtLenGood", using Z3. [Z3] Q.E.D.