Date: Saturday, March 27, 2021 @ 14:59:11 Author: felixonmars Revision: 905333
upgpkg: cryptol 2.11.0-1: rebuild with versions 4.0.1, what4 1.1, cryptol 2.11.0 Modified: cryptol/trunk/PKGBUILD Deleted: cryptol/trunk/libbf-0.6.patch cryptol/trunk/sbv-8.8.patch -----------------+ PKGBUILD | 29 +++------- libbf-0.6.patch | 156 ------------------------------------------------------ sbv-8.8.patch | 101 ---------------------------------- 3 files changed, 10 insertions(+), 276 deletions(-) Modified: PKGBUILD =================================================================== --- PKGBUILD 2021-03-27 14:54:48 UTC (rev 905332) +++ PKGBUILD 2021-03-27 14:59:11 UTC (rev 905333) @@ -1,32 +1,23 @@ # Maintainer: Felix Yan <[email protected]> pkgname=cryptol -pkgver=2.10.0 -pkgrel=109 +pkgver=2.11.0 +pkgrel=1 pkgdesc="The Language of Cryptography" url="https://www.cryptol.net"; license=("BSD") arch=('x86_64') depends=('ghc-libs' 'z3' 'haskell-async' 'haskell-base-compat' 'haskell-bv-sized' - 'haskell-cryptohash-sha1' 'haskell-exceptions' 'haskell-gitrev' 'haskell-graphscc' - 'haskell-heredoc' 'haskell-libbf' 'haskell-memotrie' 'haskell-monad-control' - 'haskell-monadlib' 'haskell-parameterized-utils' 'haskell-panic' 'haskell-random' - 'haskell-sbv' 'haskell-simple-smt' 'haskell-strict' 'haskell-tf-random' + 'haskell-cryptohash-sha1' 'haskell-exceptions' 'haskell-extra' 'haskell-gitrev' + 'haskell-graphscc' 'haskell-heredoc' 'haskell-libbf' 'haskell-memotrie' + 'haskell-monad-control' 'haskell-monadlib' 'haskell-optparse-applicative' + 'haskell-parameterized-utils' 'haskell-panic' 'haskell-random' 'haskell-sbv' + 'haskell-simple-smt' 'haskell-strict' 'haskell-temporary' 'haskell-tf-random' 'haskell-transformers-base' 'haskell-what4' 'haskell-ansi-terminal' 'haskell-blaze-html') -makedepends=('ghc' 'uusi' 'alex' 'happy') -source=("$pkgname-$pkgver.tar.gz::https://github.com/GaloisInc/cryptol/archive/$pkgver.tar.gz"; - sbv-8.8.patch - libbf-0.6.patch) -sha512sums=('efb5f048a23de2040716d210b3d59071744d97989920266206590320585850a84de989851ed94687995874d74a3e6986d2e735e636aaa9f70f8949604ab62904' - 'da4ac99c538a935eed9efd98dd6c57f24ad12d8effe328a814661ed02395445d28c8b4f43b48492171dc0bd65c6568fe7641de94e32765d51ab208a38f09d2d2' - 'b26cef81b4412b7d655376ee01a67bb531b69b2a134b08d6ee592618dee87bc70f8f1acb38db42d5b49f0e70934670f3118e07887958a262924faf469d41eb47') +makedepends=('ghc' 'alex' 'happy') +source=("$pkgname-$pkgver.tar.gz::https://github.com/GaloisInc/cryptol/archive/$pkgver.tar.gz";) +sha512sums=('4e8e9dec727c02e76043ee390b91d0a740df747a8f49b2551686ac7db3cc0c94c36e20316b59e7e50e28b838f3f9bf7202095cf6ce683d83fd47826702381649') -prepare() { - patch -d $pkgname-$pkgver -p1 < sbv-8.8.patch - patch -d $pkgname-$pkgver -p1 < libbf-0.6.patch - uusi -u sbv $pkgname-$pkgver/$pkgname.cabal -} - build() { cd "${srcdir}/${pkgname}-${pkgver}" Deleted: libbf-0.6.patch =================================================================== --- libbf-0.6.patch 2021-03-27 14:54:48 UTC (rev 905332) +++ libbf-0.6.patch 2021-03-27 14:59:11 UTC (rev 905333) @@ -1,156 +0,0 @@ -From 78855e796720cf6b96f4ccc9435d871b9474f05c Mon Sep 17 00:00:00 2001 -From: Rob Dockins <[email protected]> -Date: Thu, 28 Jan 2021 15:24:15 -0800 -Subject: [PATCH] Update to use `libBF` version 0.6, which has some bugfixes - and additional operations. - ---- - cryptol.cabal | 2 +- - src/Cryptol/Backend/Concrete.hs | 4 +- - src/Cryptol/Backend/FloatHelpers.hs | 86 +---------------------------- - 3 files changed, 5 insertions(+), 87 deletions(-) - -diff --git a/cryptol.cabal b/cryptol.cabal -index a737c0d3..dfd30a26 100644 ---- a/cryptol.cabal -+++ b/cryptol.cabal -@@ -57,7 +57,7 @@ library - GraphSCC >= 1.0.4, - heredoc >= 0.2, - integer-gmp >= 1.0 && < 1.1, -- libBF >= 0.5.1, -+ libBF >= 0.6 && < 0.7, - MemoTrie >= 0.6 && < 0.7, - monad-control >= 1.0, - monadLib >= 3.7.2, -diff --git a/src/Cryptol/Backend/Concrete.hs b/src/Cryptol/Backend/Concrete.hs -index 129c9a11..cb043b17 100644 ---- a/src/Cryptol/Backend/Concrete.hs -+++ b/src/Cryptol/Backend/Concrete.hs -@@ -338,11 +338,11 @@ instance Backend Concrete where - fpDiv = fpBinArith FP.bfDiv - fpNeg _ x = pure x { FP.bfValue = FP.bfNeg (FP.bfValue x) } - fpFromInteger sym e p r x = -- do opts <- FP.fpOpts e p <$> fpRoundMode sym r -+ do r' <- fpRoundMode sym r - pure FP.BF { FP.bfExpWidth = e - , FP.bfPrecWidth = p - , FP.bfValue = FP.fpCheckStatus $ -- FP.bfRoundInt opts (FP.bfFromInteger x) -+ FP.bfRoundInt r' (FP.bfFromInteger x) - } - fpToInteger = fpCvtToInteger - -diff --git a/src/Cryptol/Backend/FloatHelpers.hs b/src/Cryptol/Backend/FloatHelpers.hs -index 07c5113f..a622b668 100644 ---- a/src/Cryptol/Backend/FloatHelpers.hs -+++ b/src/Cryptol/Backend/FloatHelpers.hs -@@ -3,8 +3,6 @@ - module Cryptol.Backend.FloatHelpers where - - import Data.Ratio(numerator,denominator) --import Data.Int(Int64) --import Data.Bits(testBit,setBit,shiftL,shiftR,(.&.),(.|.)) - import LibBF - - import Cryptol.Utils.PP -@@ -150,97 +148,17 @@ floatToInteger fun r fp = - ["Unexpected rounding mode", show r] - - -- -- - floatFromBits :: - Integer {- ^ Exponent width -} -> - Integer {- ^ Precision widht -} -> - Integer {- ^ Raw bits -} -> - BF --floatFromBits e p bv = BF { bfValue = floatFromBits' e p bv -+floatFromBits e p bv = BF { bfValue = bfFromBits (fpOpts e p NearEven) bv - , bfExpWidth = e, bfPrecWidth = p } - - -- ---- | Make a float using "raw" bits. --floatFromBits' :: -- Integer {- ^ Exponent width -} -> -- Integer {- ^ Precision widht -} -> -- Integer {- ^ Raw bits -} -> -- BigFloat -- --floatFromBits' e p bits -- | expoBiased == 0 && mant == 0 = -- zero -- if isNeg then bfNegZero else bfPosZero -- -- | expoBiased == eMask && mant == 0 = -- infinity -- if isNeg then bfNegInf else bfPosInf -- -- | expoBiased == eMask = bfNaN -- NaN -- -- | expoBiased == 0 = -- Subnormal -- case bfMul2Exp opts (bfFromInteger mant) (expoVal + 1) of -- (num,Ok) -> if isNeg then bfNeg num else num -- (_,s) -> panic "floatFromBits" [ "Unexpected status: " ++ show s ] -- -- | otherwise = -- Normal -- case bfMul2Exp opts (bfFromInteger mantVal) expoVal of -- (num,Ok) -> if isNeg then bfNeg num else num -- (_,s) -> panic "floatFromBits" [ "Unexpected status: " ++ show s ] -- -- where -- opts = expBits e' <> precBits (p' + 1) <> allowSubnormal -- -- e' = fromInteger e :: Int -- p' = fromInteger p - 1 :: Int -- eMask = (1 `shiftL` e') - 1 :: Int64 -- pMask = (1 `shiftL` p') - 1 :: Integer -- -- isNeg = testBit bits (e' + p') -- -- mant = pMask .&. bits :: Integer -- mantVal = mant `setBit` p' :: Integer -- -- accounts for the implicit 1 bit -- -- expoBiased = eMask .&. fromInteger (bits `shiftR` p') :: Int64 -- bias = eMask `shiftR` 1 :: Int64 -- expoVal = expoBiased - bias - fromIntegral p' :: Int64 -- -- - -- | Turn a float into raw bits. - -- @NaN@ is represented as a positive "quiet" @NaN@ - -- (most significant bit in the significand is set, the rest of it is 0) - floatToBits :: Integer -> Integer -> BigFloat -> Integer --floatToBits e p bf = (isNeg `shiftL` (e' + p')) -- .|. (expBiased `shiftL` p') -- .|. (mant `shiftL` 0) -- where -- e' = fromInteger e :: Int -- p' = fromInteger p - 1 :: Int -- -- eMask = (1 `shiftL` e') - 1 :: Integer -- pMask = (1 `shiftL` p') - 1 :: Integer -- -- (isNeg, expBiased, mant) = -- case bfToRep bf of -- BFNaN -> (0, eMask, 1 `shiftL` (p' - 1)) -- BFRep s num -> (sign, be, ma) -- where -- sign = case s of -- Neg -> 1 -- Pos -> 0 -- -- (be,ma) = -- case num of -- Zero -> (0,0) -- Num i ev -- | ex == 0 -> (0, i `shiftL` (p' - m -1)) -- | otherwise -> (ex, (i `shiftL` (p' - m)) .&. pMask) -- where -- m = msb 0 i - 1 -- bias = eMask `shiftR` 1 -- ex = toInteger ev + bias + toInteger m -- -- Inf -> (eMask,0) -- -- msb !n j = if j == 0 then n else msb (n+1) (j `shiftR` 1) -+floatToBits e p bf = bfToBits (fpOpts e p NearEven) bf Deleted: sbv-8.8.patch =================================================================== --- sbv-8.8.patch 2021-03-27 14:54:48 UTC (rev 905332) +++ sbv-8.8.patch 2021-03-27 14:59:11 UTC (rev 905333) @@ -1,101 +0,0 @@ -diff --git a/cryptol.cabal b/cryptol.cabal -index 24eb2929..e65d3ed7 100644 ---- a/cryptol.cabal -+++ b/cryptol.cabal -@@ -65,7 +65,7 @@ library - pretty >= 1.1, - process >= 1.2, - random >= 1.0.1, -- sbv >= 8.6 && < 8.8, -+ sbv >= 8.6 && < 8.10, - simple-smt >= 0.7.1, - stm >= 2.4, - strict, -diff --git a/src/Cryptol/Backend/SBV.hs b/src/Cryptol/Backend/SBV.hs -index 6a4d8b00..50e4e087 100644 ---- a/src/Cryptol/Backend/SBV.hs -+++ b/src/Cryptol/Backend/SBV.hs -@@ -6,6 +6,7 @@ - -- Stability : provisional - -- Portability : portable - -+{-# LANGUAGE CPP #-} - {-# LANGUAGE DeriveFunctor #-} - {-# LANGUAGE FlexibleInstances #-} - {-# LANGUAGE GeneralizedNewtypeDeriving #-} -@@ -73,17 +74,24 @@ unpackSBV x = [ svTestBit x i | i <- reverse [0 .. intSizeOf x - 1] ] - literalSWord :: Int -> Integer -> SWord SBV - literalSWord w i = svInteger (KBounded False w) i - -+svMkSymVar_ :: Maybe Quantifier -> Kind -> Maybe String -> SBV.State -> IO SVal -+#if MIN_VERSION_sbv(8,8,0) -+svMkSymVar_ a b c = svMkSymVar (SBV.NonQueryVar a) b c -+#else -+svMkSymVar_ a b c = svMkSymVar a b c -+#endif -+ - freshBV_ :: SBV -> Int -> IO (SWord SBV) - freshBV_ (SBV stateVar _) w = -- withMVar stateVar (svMkSymVar Nothing (KBounded False w) Nothing) -+ withMVar stateVar (svMkSymVar_ Nothing (KBounded False w) Nothing) - - freshSBool_ :: SBV -> IO (SBit SBV) - freshSBool_ (SBV stateVar _) = -- withMVar stateVar (svMkSymVar Nothing KBool Nothing) -+ withMVar stateVar (svMkSymVar_ Nothing KBool Nothing) - - freshSInteger_ :: SBV -> IO (SInteger SBV) - freshSInteger_ (SBV stateVar _) = -- withMVar stateVar (svMkSymVar Nothing KUnbounded Nothing) -+ withMVar stateVar (svMkSymVar_ Nothing KUnbounded Nothing) - - - -- SBV Evaluation monad ------------------------------------------------------- -diff --git a/src/Cryptol/Symbolic/SBV.hs b/src/Cryptol/Symbolic/SBV.hs -index 2f97100e..7421db91 100644 ---- a/src/Cryptol/Symbolic/SBV.hs -+++ b/src/Cryptol/Symbolic/SBV.hs -@@ -6,6 +6,7 @@ - -- Stability : provisional - -- Portability : portable - -+{-# LANGUAGE CPP #-} - {-# LANGUAGE FlexibleContexts #-} - {-# LANGUAGE ImplicitParams #-} - {-# LANGUAGE LambdaCase #-} -@@ -124,7 +125,11 @@ proverNames = map fst proverConfigs - setupProver :: String -> IO (Either String ([String], SBVProverConfig)) - setupProver nm - | nm `elem` ["any","sbv-any"] = -+#if MIN_VERSION_sbv(8,9,0) -+ do ps <- SBV.getAvailableSolvers -+#else - do ps <- SBV.sbvAvailableSolvers -+#endif - case ps of - [] -> pure (Left "SBV could not find any provers") - _ -> let msg = "SBV found the following solvers: " ++ show (map (SBV.name . SBV.solver) ps) in -@@ -155,7 +160,11 @@ satSMTResults :: SBV.SatResult -> [SBV.SMTResult] - satSMTResults (SBV.SatResult r) = [r] - - allSatSMTResults :: SBV.AllSatResult -> [SBV.SMTResult] -+#if MIN_VERSION_sbv(8,8,0) -+allSatSMTResults (SBV.AllSatResult {allSatResults = rs}) = rs -+#else - allSatSMTResults (SBV.AllSatResult (_, _, _, rs)) = rs -+#endif - - thmSMTResults :: SBV.ThmResult -> [SBV.SMTResult] - thmSMTResults (SBV.ThmResult r) = [r] -@@ -389,7 +398,11 @@ processResults ProverCommand{..} ts results = - - -- otherwise something is wrong - _ -> return $ ProverError (rshow results) -+#if MIN_VERSION_sbv(8,8,0) -+ where rshow | isSat = show . (SBV.AllSatResult False False False False) -+#else - where rshow | isSat = show . SBV.AllSatResult . (False,False,False,) -+#endif - | otherwise = show . SBV.ThmResult . head - - where
