sbvPlugin 9.8.1 → 9.8.2
raw patch · 4 files changed
+15/−5 lines, 4 filesdep ~ghcdep ~sbv
Dependency ranges changed: ghc, sbv
Files
- CHANGES.md +5/−1
- Data/SBV/Plugin/Examples/MergeSort.hs +4/−0
- Data/SBV/Plugin/Examples/MicroController.hs +2/−0
- sbvPlugin.cabal +4/−4
CHANGES.md view
@@ -1,7 +1,11 @@ * Hackage: <http://hackage.haskell.org/package/sbvPlugin> * GitHub: <http://github.com/LeventErkok/sbvPlugin> -* 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
Data/SBV/Plugin/Examples/MergeSort.hs view
@@ -19,7 +19,9 @@ module Data.SBV.Plugin.Examples.MergeSort where +#ifndef HADDOCK import Data.SBV.Plugin+#endif ----------------------------------------------------------------------------- -- * Implementing merge-sort@@ -101,7 +103,9 @@ -- [SBV] tests/T48.hs:100:1-16 Proving "mergeSortCorrect", using Z3. -- [Z3] Q.E.D. -- @+#ifndef HADDOCK {-# ANN mergeSortCorrect theorem { options = [ListSize 4] } #-}+#endif mergeSortCorrect :: [Int] -> Bool mergeSortCorrect xs = nonDecreasing ys && isPermutationOf xs ys where ys = mergeSort xs
Data/SBV/Plugin/Examples/MicroController.hs view
@@ -86,7 +86,9 @@ -- We're being told that if the range is 200, and manual override is off, and time-since last is 9, -- then our "calculator" returns 10. But that violates the @minRate@ requirement, since we -- never want to go 'maxTimeSince' cycles without sending a signal!+#ifndef HADDOCK {-# ANN checkBad theorem {options = [IgnoreFailure]} #-}+#endif checkBad :: Int -> Bool -> Int -> Bool checkBad range manual timeSince = checkSpec computeLastBad range manual timeSince
sbvPlugin.cabal view
@@ -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 @@ 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 @@ , 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