sbvPlugin 9.4.4 → 9.6.1
raw patch · 7 files changed
+26/−10 lines, 7 filesdep ~ghcdep ~sbv
Dependency ranges changed: ghc, sbv
Files
- CHANGES.md +5/−1
- COPYRIGHT +1/−1
- Data/SBV/Plugin/Analyze.hs +4/−2
- Data/SBV/Plugin/Common.hs +1/−0
- LICENSE +1/−1
- sbvPlugin.cabal +4/−4
- tests/Run.hs +10/−1
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.4.4, 2023-01-16+* Latest Hackage released version: 9.6.1, 2023-04-14++### Version 9.6.1, 2023-04-14+ * Changes required to compile with GHC 9.6.1+ * Bump up sbv dependence to >= 10.1 ### Version 9.4.4, 2023-01-16 * Changes required to compile with GHC 9.4.4
COPYRIGHT view
@@ -1,4 +1,4 @@-Copyright (c) 2015-2022, Levent Erkok (erkokl@gmail.com)+Copyright (c) 2015-2023, Levent Erkok (erkokl@gmail.com) All rights reserved. The sbvPlugin is distributed with the BSD3 license. See the LICENSE file
Data/SBV/Plugin/Analyze.hs view
@@ -18,7 +18,9 @@ import GHC.Core.TyCo.Rep as TyCoRep import GHC.Plugins+import GHC.Tc.Utils.TcType +import Control.Monad (unless, mplus, zipWithM) import Control.Monad.Reader import System.Exit @@ -263,7 +265,7 @@ k <- getType noSrcSpan t nm <- mkValidName (showSDoc flags (ppr e)) case k of- KBase b -> return $ Base $ S.svUninterpreted b nm Nothing []+ KBase b -> return $ Base $ S.svUninterpreted b nm S.UINone [] _ -> error $ "Impossible: The type for literal resulted in non base kind: " ++ sh (e, k) tgo tFun orig@App{} = do@@ -531,7 +533,7 @@ bArgs = concatMap mkArg (reverse args) mkRes :: String -> SKind -> Eval [S.SVal]- mkRes n (KBase b) = return [S.svUninterpreted b n Nothing bArgs]+ mkRes n (KBase b) = return [S.svUninterpreted b n S.UINone bArgs] mkRes n (KTup bs) = concat `fmap` zipWithM mkRes [n ++ "_" ++ show i | i <- [(1 :: Int) .. ]] bs mkRes n (KLst b) = do ls <- case mbListSize of Just i -> return i
Data/SBV/Plugin/Common.hs view
@@ -16,6 +16,7 @@ module Data.SBV.Plugin.Common where +import Control.Monad (zipWithM, mplus) import Control.Monad.Reader import GHC.Plugins
LICENSE view
@@ -1,6 +1,6 @@ sbvPlugin: SMT based theorem prover for Haskell -Copyright (c) 2015-2022, Levent Erkok (erkokl@gmail.com)+Copyright (c) 2015-2023, Levent Erkok (erkokl@gmail.com) All rights reserved. Redistribution and use in source and binary forms, with or without
sbvPlugin.cabal view
@@ -1,5 +1,5 @@ Name : sbvPlugin-Version : 9.4.4+Version : 9.6.1 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 @@ Cabal-Version : 1.14 Extra-Source-Files: INSTALL, README.md, COPYRIGHT, CHANGES.md -Tested-With : GHC==9.4.4+Tested-With : GHC==9.6.1 source-repository head type: git@@ -34,8 +34,8 @@ , Data.SBV.Plugin.Examples.MergeSort , Data.SBV.Plugin.Examples.MicroController build-depends : base >= 4.11 && < 5- , sbv >= 9.2- , ghc >= 9.4.4+ , sbv >= 10.1+ , ghc >= 9.6.1 , ghc-prim , containers , mtl
tests/Run.hs view
@@ -27,10 +27,19 @@ _ -> False return $ filter testFile allEntries +packages :: [String]+packages = ["-package " ++ p | p <- ps]+ where ps = [ "base"+ , "containers"+ , "mtl"+ , "template-haskell"+ , "ghc-prim"+ ]+ runTest :: String -> TestTree runTest f = goldenVsFile f gld out act where (inp, hi, o, gld, out) = fileNames f- act = do void $ system $ unwords ["ghc", "-c", inp, ">", out, "2>&1"]+ act = do void $ system $ unwords $ ["ghc"] ++ packages ++ ["-c", inp, ">", out, "2>&1"] void $ system $ unwords ["sed", "-i", "''", "'s/^Loaded package environment from.*/Loaded package environment from test-modified path/g'", out] void $ system $ unwords ["/bin/rm", "-f", hi, o]