Date: Tuesday, August 17, 2021 @ 19:24:33 Author: felixonmars Revision: 1002483
archrelease: copy trunk to community-staging-x86_64 Added: haskell-tamarin-prover-theory/repos/community-staging-x86_64/ haskell-tamarin-prover-theory/repos/community-staging-x86_64/PKGBUILD (from rev 1002482, haskell-tamarin-prover-theory/trunk/PKGBUILD) haskell-tamarin-prover-theory/repos/community-staging-x86_64/ghc9.patch (from rev 1002482, haskell-tamarin-prover-theory/trunk/ghc9.patch) ------------+ PKGBUILD | 45 ++++++++++++++++++++++++++++++ ghc9.patch | 87 +++++++++++++++++++++++++++++++++++++++++++++++++++++++++++ 2 files changed, 132 insertions(+) Copied: haskell-tamarin-prover-theory/repos/community-staging-x86_64/PKGBUILD (from rev 1002482, haskell-tamarin-prover-theory/trunk/PKGBUILD) =================================================================== --- community-staging-x86_64/PKGBUILD (rev 0) +++ community-staging-x86_64/PKGBUILD 2021-08-17 19:24:33 UTC (rev 1002483) @@ -0,0 +1,45 @@ +# Maintainer: Felix Yan <felixonm...@archlinux.org> +# Contributor: Arch Haskell Team <arch-hask...@haskell.org> + +_hkgname=tamarin-prover-theory +pkgname=haskell-tamarin-prover-theory +pkgver=1.6.0 +pkgrel=114 +pkgdesc="Security protocol types and constraint solver library for the tamarin prover" +url="http://www.infsec.ethz.ch/research/software/tamarin" +license=("GPL") +arch=('x86_64') +depends=('ghc-libs' 'haskell-aeson' 'haskell-aeson-pretty' 'haskell-dlist' 'haskell-fclabels' + 'haskell-parallel' 'haskell-safe' 'haskell-uniplate' 'haskell-tamarin-prover-utils' + 'haskell-tamarin-prover-term') +makedepends=('ghc') +source=("tamarin-prover-$pkgver.tar.gz::https://github.com/tamarin-prover/tamarin-prover/archive/$pkgver.tar.gz" + ghc9.patch) +sha512sums=('7f3569f740d63d715b92a8f073eaecb8b32efe59b910b246977d36bb9e873765440e72feb6e76c7cbafab0495b88cfc666bb1dd12f685627c60d5cbd97b2973e' + '6248791aea411e04de0f2227aeaac85d7ce5519808998b01751db5ede18cb6056dd216dac91e17d5867a24fb3101dd5d1d4c90abc83c68d26f144ae187313361') + +prepare() { + patch -d tamarin-prover-$pkgver -p1 < ghc9.patch +} + +build() { + cd tamarin-prover-$pkgver/lib/theory + + runhaskell Setup configure -O --enable-shared --enable-executable-dynamic --disable-library-vanilla \ + --prefix=/usr --docdir=/usr/share/doc/$pkgname \ + --dynlibdir=/usr/lib --libsubdir=\$compiler/site-local/\$pkgid + runhaskell Setup build $MAKEFLAGS + runhaskell Setup register --gen-script + runhaskell Setup unregister --gen-script + sed -i -r -e "s|ghc-pkg.*update[^ ]* |&'--force' |" register.sh + sed -i -r -e "s|ghc-pkg.*unregister[^ ]* |&'--force' |" unregister.sh +} + +package() { + cd tamarin-prover-$pkgver/lib/theory + + install -D -m744 register.sh "$pkgdir"/usr/share/haskell/register/$pkgname.sh + install -D -m744 unregister.sh "$pkgdir"/usr/share/haskell/unregister/$pkgname.sh + runhaskell Setup copy --destdir="$pkgdir" + rm -f "$pkgdir"/usr/share/doc/$pkgname/LICENSE +} Copied: haskell-tamarin-prover-theory/repos/community-staging-x86_64/ghc9.patch (from rev 1002482, haskell-tamarin-prover-theory/trunk/ghc9.patch) =================================================================== --- community-staging-x86_64/ghc9.patch (rev 0) +++ community-staging-x86_64/ghc9.patch 2021-08-17 19:24:33 UTC (rev 1002483) @@ -0,0 +1,87 @@ +diff --git a/lib/theory/src/Theory/Constraint/System.hs b/lib/theory/src/Theory/Constraint/System.hs +index 30b1589e..b7c5d56a 100644 +--- a/lib/theory/src/Theory/Constraint/System.hs ++++ b/lib/theory/src/Theory/Constraint/System.hs +@@ -415,16 +415,6 @@ eitherProofContext ctxt s = if s==LHS then L.get dpcPCLeft ctxt else L.get dpcPC + -- Instances + ------------ + +-instance HasFrees Source where +- foldFrees f th = +- foldFrees f (L.get cdGoal th) `mappend` +- foldFrees f (L.get cdCases th) +- +- foldFreesOcc _ _ = const mempty +- +- mapFrees f th = Source <$> mapFrees f (L.get cdGoal th) +- <*> mapFrees f (L.get cdCases th) +- + data DiffProofType = RuleEquivalence | None + deriving( Eq, Ord, Show, Generic, NFData, Binary ) + +@@ -1483,6 +1473,15 @@ instance HasFrees System where + <*> mapFrees fun k + <*> mapFrees fun l + ++instance HasFrees Source where ++ foldFrees f th = ++ foldFrees f (L.get cdGoal th) `mappend` ++ foldFrees f (L.get cdCases th) ++ ++ foldFreesOcc _ _ = const mempty ++ ++ mapFrees f th = Source <$> mapFrees f (L.get cdGoal th) ++ <*> mapFrees f (L.get cdCases th) + + -- Special comparison functions to ignore new var instantiations + ---------------------------------------------------------------- +diff --git a/lib/theory/src/Theory/Constraint/System/JSON.hs b/lib/theory/src/Theory/Constraint/System/JSON.hs +index 57ff7501..62a0b379 100644 +--- a/lib/theory/src/Theory/Constraint/System/JSON.hs ++++ b/lib/theory/src/Theory/Constraint/System/JSON.hs +@@ -101,22 +101,6 @@ data JSONGraphNode = JSONGraphNode + , jgnMetadata :: Maybe JSONGraphNodeMetadata + } deriving (Show) + +--- | Optional fields are not handled correctly with automatically derived instances +--- hence, we have our own here. +-instance FromJSON JSONGraphNode where +- parseJSON = withObject "JSONGraphNode" $ \o -> JSONGraphNode +- <$> o .: "jgnId" +- <*> o .: "jgnType" +- <*> o .: "jgnLabel" +- <*> o .:? "jgnMetadata" +- +-instance ToJSON JSONGraphNode where +- toJSON (JSONGraphNode jgnId' jgnType' jgnLabel' jgnMetadata') = object $ catMaybes +- [ ("jgnId" .=) <$> pure jgnId' +- , ("jgnType" .=) <$> pure jgnType' +- , ("jgnLabel" .=) <$> pure jgnLabel' +- , ("jgnMetadata" .=) <$> jgnMetadata' ] +- + -- | Representation of an edge of a JSON graph. + data JSONGraphEdge = JSONGraphEdge + { +@@ -147,6 +131,22 @@ data JSONGraphs = JSONGraphs + -- | Derive ToJSON and FromJSON. + concat <$> mapM (deriveJSON defaultOptions) [''JSONGraphNodeFact, ''JSONGraphNodeMetadata, ''JSONGraphEdge, ''JSONGraph, ''JSONGraphs] + ++-- | Optional fields are not handled correctly with automatically derived instances ++-- hence, we have our own here. ++instance FromJSON JSONGraphNode where ++ parseJSON = withObject "JSONGraphNode" $ \o -> JSONGraphNode ++ <$> o .: "jgnId" ++ <*> o .: "jgnType" ++ <*> o .: "jgnLabel" ++ <*> o .:? "jgnMetadata" ++ ++instance ToJSON JSONGraphNode where ++ toJSON (JSONGraphNode jgnId' jgnType' jgnLabel' jgnMetadata') = object $ catMaybes ++ [ ("jgnId" .=) <$> pure jgnId' ++ , ("jgnType" .=) <$> pure jgnType' ++ , ("jgnLabel" .=) <$> pure jgnLabel' ++ , ("jgnMetadata" .=) <$> jgnMetadata' ] ++ + -- | Generation of JSON text from JSON graphs. + + -- | Flatten out pretty printed facts from prettyLNFact etc.