JakeHillion/nixpkgs
1
0
Fork 0
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity

tamarin-prover: fix ghc 8.4 build (#46597)

Browse Source 
See https://hydra.nixos.org/build/81125645

`tamarin-prover' upstream has a patch to fix GHC 8.4 compilation (and
uses stack lts-12.1 now), but it's not released yet:

a08f6e4007

The build is divided in several derivations, therefore the patch had to
be splitted and rebased for `lib/term', `lib/theory' and `lib/utils' to
ensure that the patch applies properly during the `patchPhase'.

Addresses #45960
This commit is contained in:
Maximilian Bosch 2018-09-13 14:11:09 +02:00 committed by xeji
parent e2df8e7c0f
commit 2cfc0bb7ee
4 changed files with 385 additions and 3 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

9
pkgs/applications/science/logic/tamarin-prover/default.nix
View File

@ -31,7 +31,8 @@ let
'';
tamarin-prover-utils = mkDerivation (common "tamarin-prover-utils" (src + "/lib/utils") // {
patchPhase = replaceSymlinks;
postPatch = replaceSymlinks;
patches = [ ./ghc-8.4-support-utils.patch ];
libraryHaskellDepends = with haskellPackages; [
base base64-bytestring binary blaze-builder bytestring containers
deepseq dlist fclabels mtl pretty safe SHA syb time transformers
@ -39,7 +40,8 @@ let
});
tamarin-prover-term = mkDerivation (common "tamarin-prover-term" (src + "/lib/term") // {
patchPhase = replaceSymlinks;
postPatch = replaceSymlinks;
patches = [ ./ghc-8.4-support-term.patch ];
libraryHaskellDepends = (with haskellPackages; [
attoparsec base binary bytestring containers deepseq dlist HUnit
mtl process safe
@ -47,7 +49,8 @@ let
});
tamarin-prover-theory = mkDerivation (common "tamarin-prover-theory" (src + "/lib/theory") // {
patchPhase = replaceSymlinks;
postPatch = replaceSymlinks;
patches = [ ./ghc-8.4-support-theory.patch ];
doHaddock = false; # broken
libraryHaskellDepends = (with haskellPackages; [
aeson aeson-pretty base binary bytestring containers deepseq dlist

109
pkgs/applications/science/logic/tamarin-prover/ghc-8.4-support-term.patch Normal file
View File

@ -0,0 +1,109 @@
From a08f6e400772899b9b0fc16befc50391cd70696b Mon Sep 17 00:00:00 2001
From: Felix Yan <felixonmars@archlinux.org>
Date: Fri, 18 May 2018 16:24:41 +0800
Subject: [PATCH] GHC 8.4 support
---
src/Term/Maude/Signature.hs | 8 ++--
src/Term/Rewriting/Definitions.hs | 23 ++++++----
src/Term/Unification.hs | 4 +-
11 files changed, 79 insertions(+), 48 deletions(-)
diff --git a/src/Term/Maude/Signature.hs b/src/Term/Maude/Signature.hs
index 98c25d9f..1a4ce82f 100644
--- a/src/Term/Maude/Signature.hs
+++ b/src/Term/Maude/Signature.hs
@@ -104,9 +104,9 @@ maudeSig msig@(MaudeSig {enableDH,enableBP,enableMSet,enableXor,enableDiff=_,stF
`S.union` dhReducibleFunSig `S.union` bpReducibleFunSig `S.union` xorReducibleFunSig
-- | A monoid instance to combine maude signatures.
-instance Monoid MaudeSig where
- (MaudeSig dh1 bp1 mset1 xor1 diff1 stFunSyms1 stRules1 _ _) `mappend`
- (MaudeSig dh2 bp2 mset2 xor2 diff2 stFunSyms2 stRules2 _ _) =
+instance Semigroup MaudeSig where
+ MaudeSig dh1 bp1 mset1 xor1 diff1 stFunSyms1 stRules1 _ _ <>
+ MaudeSig dh2 bp2 mset2 xor2 diff2 stFunSyms2 stRules2 _ _ =
maudeSig (mempty {enableDH=dh1||dh2
,enableBP=bp1||bp2
,enableMSet=mset1||mset2
@@ -114,6 +114,8 @@ instance Monoid MaudeSig where
,enableDiff=diff1||diff2
,stFunSyms=S.union stFunSyms1 stFunSyms2
,stRules=S.union stRules1 stRules2})
+
+instance Monoid MaudeSig where
mempty = MaudeSig False False False False False S.empty S.empty S.empty S.empty
-- | Non-AC function symbols.
diff --git a/src/Term/Rewriting/Definitions.hs b/src/Term/Rewriting/Definitions.hs
index bd942b6a..18562e4e 100644
--- a/src/Term/Rewriting/Definitions.hs
+++ b/src/Term/Rewriting/Definitions.hs
@@ -44,10 +44,12 @@ evalEqual (Equal l r) = l == r
instance Functor Equal where
fmap f (Equal lhs rhs) = Equal (f lhs) (f rhs)
+instance Semigroup a => Semigroup (Equal a) where
+ (Equal l1 r1) <> (Equal l2 r2) =
+ Equal (l1 <> l2) (r1 <> r2)
+
instance Monoid a => Monoid (Equal a) where
mempty = Equal mempty mempty
- (Equal l1 r1) `mappend` (Equal l2 r2) =
- Equal (l1 `mappend` l2) (r1 `mappend` r2)
instance Foldable Equal where
foldMap f (Equal l r) = f l `mappend` f r
@@ -104,14 +106,15 @@ instance Functor Match where
fmap _ NoMatch = NoMatch
fmap f (DelayedMatches ms) = DelayedMatches (fmap (f *** f) ms)
+instance Semigroup (Match a) where
+ NoMatch <> _ = NoMatch
+ _ <> NoMatch = NoMatch
+ DelayedMatches ms1 <> DelayedMatches ms2 =
+ DelayedMatches (ms1 <> ms2)
+
instance Monoid (Match a) where
mempty = DelayedMatches []
- NoMatch `mappend` _ = NoMatch
- _ `mappend` NoMatch = NoMatch
- DelayedMatches ms1 `mappend` DelayedMatches ms2 =
- DelayedMatches (ms1 `mappend` ms2)
-
instance Foldable Match where
foldMap _ NoMatch = mempty
@@ -136,10 +139,12 @@ data RRule a = RRule a a
instance Functor RRule where
fmap f (RRule lhs rhs) = RRule (f lhs) (f rhs)
+instance Monoid a => Semigroup (RRule a) where
+ (RRule l1 r1) <> (RRule l2 r2) =
+ RRule (l1 <> l2) (r1 <> r2)
+
instance Monoid a => Monoid (RRule a) where
mempty = RRule mempty mempty
- (RRule l1 r1) `mappend` (RRule l2 r2) =
- RRule (l1 `mappend` l2) (r1 `mappend` r2)
instance Foldable RRule where
foldMap f (RRule l r) = f l `mappend` f r
diff --git a/src/Term/Unification.hs b/src/Term/Unification.hs
index e1de0163..7ce6bb41 100644
--- a/src/Term/Unification.hs
+++ b/src/Term/Unification.hs
@@ -265,9 +265,11 @@ unifyRaw l0 r0 = do
data MatchFailure = NoMatcher | ACProblem
+instance Semigroup MatchFailure where
+ _ <> _ = NoMatcher
+
instance Monoid MatchFailure where
mempty = NoMatcher
- mappend _ _ = NoMatcher
-- | Ensure that the computed substitution @sigma@ satisfies
-- @t ==_AC apply sigma p@ after the delayed equations are solved.

130
pkgs/applications/science/logic/tamarin-prover/ghc-8.4-support-theory.patch Normal file
View File

@ -0,0 +1,130 @@
From a08f6e400772899b9b0fc16befc50391cd70696b Mon Sep 17 00:00:00 2001
From: Felix Yan <felixonmars@archlinux.org>
Date: Fri, 18 May 2018 16:24:41 +0800
Subject: [PATCH] GHC 8.4 support
---
src/Theory/Proof.hs | 43 +++++++++++--------
11 files changed, 79 insertions(+), 48 deletions(-)
diff --git a/src/Theory/Constraint/Solver/Reduction.hs b/src/Theory/Constraint/Solver/Reduction.hs
index ddbc965a..6daadd0d 100644
--- a/src/Theory/Constraint/Solver/Reduction.hs
+++ b/src/Theory/Constraint/Solver/Reduction.hs
@@ -139,13 +139,14 @@ execReduction m ctxt se fs =
data ChangeIndicator = Unchanged | Changed
deriving( Eq, Ord, Show )
+instance Semigroup ChangeIndicator where
+ Changed <> _ = Changed
+ _ <> Changed = Changed
+ Unchanged <> Unchanged = Unchanged
+
instance Monoid ChangeIndicator where
mempty = Unchanged
- Changed `mappend` _ = Changed
- _ `mappend` Changed = Changed
- Unchanged `mappend` Unchanged = Unchanged
-
-- | Return 'True' iff there was a change.
wasChanged :: ChangeIndicator -> Bool
wasChanged Changed = True
diff --git a/src/Theory/Constraint/System/Guarded.hs b/src/Theory/Constraint/System/Guarded.hs
index f98fc7c2..2aac8ce2 100644
--- a/src/Theory/Constraint/System/Guarded.hs
+++ b/src/Theory/Constraint/System/Guarded.hs
@@ -435,7 +435,7 @@ gall ss atos gf = GGuarded All ss atos gf
-- | Local newtype to avoid orphan instance.
newtype ErrorDoc d = ErrorDoc { unErrorDoc :: d }
- deriving( Monoid, NFData, Document, HighlightDocument )
+ deriving( Monoid, Semigroup, NFData, Document, HighlightDocument )
-- | @formulaToGuarded fm@ returns a guarded formula @gf@ that is
-- equivalent to @fm@ under the assumption that this is possible.
diff --git a/src/Theory/Proof.hs b/src/Theory/Proof.hs
index 74fb77b1..7971b9fc 100644
--- a/src/Theory/Proof.hs
+++ b/src/Theory/Proof.hs
@@ -388,17 +388,19 @@ data ProofStatus =
| TraceFound -- ^ There is an annotated solved step
deriving ( Show, Generic, NFData, Binary )
+instance Semigroup ProofStatus where
+ TraceFound <> _ = TraceFound
+ _ <> TraceFound = TraceFound
+ IncompleteProof <> _ = IncompleteProof
+ _ <> IncompleteProof = IncompleteProof
+ _ <> CompleteProof = CompleteProof
+ CompleteProof <> _ = CompleteProof
+ UndeterminedProof <> UndeterminedProof = UndeterminedProof
+
+
instance Monoid ProofStatus where
mempty = CompleteProof
- mappend TraceFound _ = TraceFound
- mappend _ TraceFound = TraceFound
- mappend IncompleteProof _ = IncompleteProof
- mappend _ IncompleteProof = IncompleteProof
- mappend _ CompleteProof = CompleteProof
- mappend CompleteProof _ = CompleteProof
- mappend UndeterminedProof UndeterminedProof = UndeterminedProof
-
-- | The status of a 'ProofStep'.
proofStepStatus :: ProofStep (Maybe a) -> ProofStatus
proofStepStatus (ProofStep _ Nothing ) = UndeterminedProof
@@ -560,10 +562,12 @@ newtype Prover = Prover
-> Maybe IncrementalProof -- resulting proof
}
+instance Semigroup Prover where
+ p1 <> p2 = Prover $ \ctxt d se ->
+ runProver p1 ctxt d se >=> runProver p2 ctxt d se
+
instance Monoid Prover where
mempty = Prover $ \_ _ _ -> Just
- p1 `mappend` p2 = Prover $ \ctxt d se ->
- runProver p1 ctxt d se >=> runProver p2 ctxt d se
-- | Provers whose sequencing is handled via the 'Monoid' instance.
--
@@ -579,10 +583,12 @@ newtype DiffProver = DiffProver
-> Maybe IncrementalDiffProof -- resulting proof
}
+instance Semigroup DiffProver where
+ p1 <> p2 = DiffProver $ \ctxt d se ->
+ runDiffProver p1 ctxt d se >=> runDiffProver p2 ctxt d se
+
instance Monoid DiffProver where
mempty = DiffProver $ \_ _ _ -> Just
- p1 `mappend` p2 = DiffProver $ \ctxt d se ->
- runDiffProver p1 ctxt d se >=> runDiffProver p2 ctxt d se
-- | Map the proof generated by the prover.
mapProverProof :: (IncrementalProof -> IncrementalProof) -> Prover -> Prover
@@ -784,15 +790,16 @@ runAutoDiffProver (AutoProver heuristic bound cut) =
-- | The result of one pass of iterative deepening.
data IterDeepRes = NoSolution | MaybeNoSolution | Solution ProofPath
+instance Semigroup IterDeepRes where
+ x@(Solution _) <> _ = x
+ _ <> y@(Solution _) = y
+ MaybeNoSolution <> _ = MaybeNoSolution
+ _ <> MaybeNoSolution = MaybeNoSolution
+ NoSolution <> NoSolution = NoSolution
+
instance Monoid IterDeepRes where
mempty = NoSolution
- x@(Solution _) `mappend` _ = x
- _ `mappend` y@(Solution _) = y
- MaybeNoSolution `mappend` _ = MaybeNoSolution
- _ `mappend` MaybeNoSolution = MaybeNoSolution
- NoSolution `mappend` NoSolution = NoSolution
-
-- | @cutOnSolvedDFS prf@ removes all other cases if an attack is found. The
-- attack search is performed using a parallel DFS traversal with iterative
-- deepening.

140
pkgs/applications/science/logic/tamarin-prover/ghc-8.4-support-utils.patch Normal file
View File

@ -0,0 +1,140 @@
From a08f6e400772899b9b0fc16befc50391cd70696b Mon Sep 17 00:00:00 2001
From: Felix Yan <felixonmars@archlinux.org>
Date: Fri, 18 May 2018 16:24:41 +0800
Subject: [PATCH] GHC 8.4 support
---
src/Extension/Data/Bounded.hs | 10 ++++-
src/Extension/Data/Monoid.hs | 14 +++---
src/Logic/Connectives.hs | 4 +-
src/Text/PrettyPrint/Class.hs | 4 +-
src/Text/PrettyPrint/Html.hs | 6 ++-
11 files changed, 79 insertions(+), 48 deletions(-)
diff --git a/src/Extension/Data/Bounded.hs b/src/Extension/Data/Bounded.hs
index 5f166006..f416a44c 100644
--- a/src/Extension/Data/Bounded.hs
+++ b/src/Extension/Data/Bounded.hs
@@ -11,19 +11,25 @@ module Extension.Data.Bounded (
) where
-- import Data.Monoid
+import Data.Semigroup
-- | A newtype wrapper for a monoid of the maximum of a bounded type.
newtype BoundedMax a = BoundedMax {getBoundedMax :: a}
deriving( Eq, Ord, Show )
+instance (Ord a, Bounded a) => Semigroup (BoundedMax a) where
+ BoundedMax x <> BoundedMax y = BoundedMax (max x y)
+
instance (Ord a, Bounded a) => Monoid (BoundedMax a) where
mempty = BoundedMax minBound
- (BoundedMax x) `mappend` (BoundedMax y) = BoundedMax (max x y)
+ mappend = (<>)
-- | A newtype wrapper for a monoid of the minimum of a bounded type.
newtype BoundedMin a = BoundedMin {getBoundedMin :: a}
deriving( Eq, Ord, Show )
+instance (Ord a, Bounded a) => Semigroup (BoundedMin a) where
+ BoundedMin x <> BoundedMin y = BoundedMin (min x y)
+
instance (Ord a, Bounded a) => Monoid (BoundedMin a) where
mempty = BoundedMin maxBound
- (BoundedMin x) `mappend` (BoundedMin y) = BoundedMin (min x y)
\ No newline at end of file
diff --git a/src/Extension/Data/Monoid.hs b/src/Extension/Data/Monoid.hs
index 83655c34..9ce2f91b 100644
--- a/src/Extension/Data/Monoid.hs
+++ b/src/Extension/Data/Monoid.hs
@@ -18,6 +18,7 @@ module Extension.Data.Monoid (
) where
import Data.Monoid
+import Data.Semigroup
#if __GLASGOW_HASKELL__ < 704
@@ -38,10 +39,13 @@ newtype MinMax a = MinMax { getMinMax :: Maybe (a, a) }
minMaxSingleton :: a -> MinMax a
minMaxSingleton x = MinMax (Just (x, x))
+instance Ord a => Semigroup (MinMax a) where
+ MinMax Nothing <> y = y
+ x <> MinMax Nothing = x
+ MinMax (Just (xMin, xMax)) <> MinMax (Just (yMin, yMax)) =
+ MinMax (Just (min xMin yMin, max xMax yMax))
+
+
instance Ord a => Monoid (MinMax a) where
mempty = MinMax Nothing
-
- MinMax Nothing `mappend` y = y
- x `mappend` MinMax Nothing = x
- MinMax (Just (xMin, xMax)) `mappend` MinMax (Just (yMin, yMax)) =
- MinMax (Just (min xMin yMin, max xMax yMax))
+ mappend = (<>)
diff --git a/src/Logic/Connectives.hs b/src/Logic/Connectives.hs
index 2e441172..7206cc2c 100644
--- a/src/Logic/Connectives.hs
+++ b/src/Logic/Connectives.hs
@@ -23,12 +23,12 @@ import Control.DeepSeq
-- | A conjunction of atoms of type a.
newtype Conj a = Conj { getConj :: [a] }
- deriving (Monoid, Foldable, Traversable, Eq, Ord, Show, Binary,
+ deriving (Monoid, Semigroup, Foldable, Traversable, Eq, Ord, Show, Binary,
Functor, Applicative, Monad, Alternative, MonadPlus, Typeable, Data, NFData)
-- | A disjunction of atoms of type a.
newtype Disj a = Disj { getDisj :: [a] }
- deriving (Monoid, Foldable, Traversable, Eq, Ord, Show, Binary,
+ deriving (Monoid, Semigroup, Foldable, Traversable, Eq, Ord, Show, Binary,
Functor, Applicative, Monad, Alternative, MonadPlus, Typeable, Data, NFData)
instance MonadDisj Disj where
diff --git a/src/Text/PrettyPrint/Class.hs b/src/Text/PrettyPrint/Class.hs
index f5eb42fe..13be6515 100644
--- a/src/Text/PrettyPrint/Class.hs
+++ b/src/Text/PrettyPrint/Class.hs
@@ -187,9 +187,11 @@ instance Document Doc where
nest i (Doc d) = Doc $ P.nest i d
caseEmptyDoc yes no (Doc d) = if P.isEmpty d then yes else no
+instance Semigroup Doc where
+ Doc d1 <> Doc d2 = Doc $ (P.<>) d1 d2
+
instance Monoid Doc where
mempty = Doc $ P.empty
- mappend (Doc d1) (Doc d2) = Doc $ (P.<>) d1 d2
------------------------------------------------------------------------------
-- Additional combinators
diff --git a/src/Text/PrettyPrint/Html.hs b/src/Text/PrettyPrint/Html.hs
index 3de5e307..10103eb7 100644
--- a/src/Text/PrettyPrint/Html.hs
+++ b/src/Text/PrettyPrint/Html.hs
@@ -90,7 +90,7 @@ attribute (key,value) = " " ++ key ++ "=\"" ++ escapeHtmlEntities value ++ "\""
-- | A 'Document' transformer that adds proper HTML escaping.
newtype HtmlDoc d = HtmlDoc { getHtmlDoc :: d }
- deriving( Monoid )
+ deriving( Monoid, Semigroup )
-- | Wrap a document such that HTML markup can be added without disturbing the
-- layout.
@@ -182,9 +182,11 @@ getNoHtmlDoc = runIdentity . unNoHtmlDoc
instance NFData d => NFData (NoHtmlDoc d) where
rnf = rnf . getNoHtmlDoc
+instance Semigroup d => Semigroup (NoHtmlDoc d) where
+ (<>) = liftA2 (<>)
+
instance Monoid d => Monoid (NoHtmlDoc d) where
mempty = pure mempty
- mappend = liftA2 mappend
instance Document d => Document (NoHtmlDoc d) where
char = pure . char