[arch-commits] Commit in haskell-tamarin-prover-theory/repos (3 files)

[Felix Yan]

    Date: Friday, August 13, 2021 @ 15:30:45
  Author: felixonmars
Revision: 998111

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 998110, haskell-tamarin-prover-theory/trunk/PKGBUILD)
  haskell-tamarin-prover-theory/repos/community-staging-x86_64/ghc9.patch
    (from rev 998110, 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 998110, haskell-tamarin-prover-theory/trunk/PKGBUILD)
===================================================================
--- community-staging-x86_64/PKGBUILD	                        (rev 0)
+++ community-staging-x86_64/PKGBUILD	2021-08-13 15:30:45 UTC (rev 998111)
@@ -0,0 +1,45 @@
+# Maintainer: Felix Yan <felixonmars at archlinux.org>
+# Contributor: Arch Haskell Team <arch-haskell at haskell.org>
+
+_hkgname=tamarin-prover-theory
+pkgname=haskell-tamarin-prover-theory
+pkgver=1.6.0
+pkgrel=112
+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 998110, haskell-tamarin-prover-theory/trunk/ghc9.patch)
===================================================================
--- community-staging-x86_64/ghc9.patch	                        (rev 0)
+++ community-staging-x86_64/ghc9.patch	2021-08-13 15:30:45 UTC (rev 998111)
@@ -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.