[arch-commits] Commit in cryptol/trunk (PKGBUILD libbf-0.6.patch sbv-8.8.patch)
Felix Yan
felixonmars at archlinux.org
Sat Mar 27 14:59:11 UTC 2021
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 <felixonmars at archlinux.org>
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 <rdockins at galois.com>
-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
More information about the arch-commits
mailing list