tamarin-prover: 1.4.0 -> 1.4.1, bundled sapic

With this, we can drop the old 1.4.0 patches for 8.4 support, since
those are now upstream.

Furthermore, SAPIC Is now bundled inside Tamarin, so we can drop the
external dependency. (This includes a patch that compiles SAPIC to
native code, much like the original, to reduce closure size.)

Signed-off-by: Austin Seipp <aseipp@pobox.com>

5 files changed, 91 insertions, 388 deletions

diff --git a/pkgs/applications/science/logic/tamarin-prover/default.nix b/pkgs/applications/science/logic/tamarin-prover/default.nix
index 9056eab71ea3f..40378f8c04d5d 100644
--- a/pkgs/applications/science/logic/tamarin-prover/default.nix
+++ b/pkgs/applications/science/logic/tamarin-prover/default.nix
@@ -1,15 +1,15 @@
 { haskellPackages, mkDerivation, fetchFromGitHub, lib
 # the following are non-haskell dependencies
-, makeWrapper, which, maude, graphviz, sapic
+, makeWrapper, which, maude, graphviz, ocaml
 }:
 
 let
-  version = "1.4.0";
+  version = "1.4.1";
   src = fetchFromGitHub {
     owner  = "tamarin-prover";
     repo   = "tamarin-prover";
-    rev    = "7ced07a69f8e93178f9a95797479277a736ae572";
-    sha256 = "02pyw22h90228g6qybjpdvpcm9d5lh96f5qwmy2hv2bylz05z3nn";
+    rev    = "d2e1c57311ce4ed0ef46d0372c4995b8fdc25323";
+    sha256 = "1bf2qvb646jg3qxd6jgp9ja3wlr888wchxi9mfr3kg7hfn63vxbq";
   };
 
   # tamarin has its own dependencies, but they're kept inside the repo,
@@ -32,7 +32,6 @@ let
 
   tamarin-prover-utils = mkDerivation (common "tamarin-prover-utils" (src + "/lib/utils") // {
     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
@@ -41,7 +40,6 @@ let
 
   tamarin-prover-term = mkDerivation (common "tamarin-prover-term" (src + "/lib/term") // {
     postPatch = replaceSymlinks;
-    patches = [ ./ghc-8.4-support-term.patch ];
     libraryHaskellDepends = (with haskellPackages; [
       attoparsec base binary bytestring containers deepseq dlist HUnit
       mtl process safe
@@ -50,7 +48,6 @@ let
 
   tamarin-prover-theory = mkDerivation (common "tamarin-prover-theory" (src + "/lib/theory") // {
     postPatch = replaceSymlinks;
-    patches = [ ./ghc-8.4-support-theory.patch ];
     doHaddock = false; # broken
     libraryHaskellDepends = (with haskellPackages; [
       aeson aeson-pretty base binary bytestring containers deepseq dlist
@@ -75,20 +72,28 @@ mkDerivation (common "tamarin-prover" src // {
 
     sed -ie 's~\( *, \)mtl~&\
     \1monad-control~' tamarin-prover.cabal
+
+    patch -p1 < ${./sapic-native.patch}
+  '';
+
+  postBuild = ''
+    cd plugins/sapic && make sapic && cd ../..
   '';
 
   # wrap the prover to be sure it can find maude, sapic, etc
-  executableToolDepends = [ makeWrapper which maude graphviz sapic ];
+  executableToolDepends = [ makeWrapper which maude graphviz ];
   postInstall = ''
     wrapProgram $out/bin/tamarin-prover \
-      --prefix PATH : ${lib.makeBinPath [ which maude graphviz sapic ]}
+      --prefix PATH : ${lib.makeBinPath [ which maude graphviz ]}
     # so that the package can be used as a vim plugin to install syntax coloration
     install -Dt $out/share/vim-plugins/tamarin-prover/syntax/ etc/{spthy,sapic}.vim
     install etc/filetype.vim -D $out/share/vim-plugins/tamarin-prover/ftdetect/tamarin.vim
+    install -m0755 ./plugins/sapic/sapic $out/bin/sapic
   '';
 
   checkPhase = "./dist/build/tamarin-prover/tamarin-prover test";
 
+  executableSystemDepends = [ ocaml ];
   executableHaskellDepends = (with haskellPackages; [
     base binary binary-orphans blaze-builder blaze-html bytestring
     cmdargs conduit containers monad-control deepseq directory fclabels file-embed
diff --git a/pkgs/applications/science/logic/tamarin-prover/ghc-8.4-support-term.patch b/pkgs/applications/science/logic/tamarin-prover/ghc-8.4-support-term.patch
deleted file mode 100644
index f93919faf54ed..0000000000000
--- a/pkgs/applications/science/logic/tamarin-prover/ghc-8.4-support-term.patch
+++ /dev/null
@@ -1,109 +0,0 @@
-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.
diff --git a/pkgs/applications/science/logic/tamarin-prover/ghc-8.4-support-theory.patch b/pkgs/applications/science/logic/tamarin-prover/ghc-8.4-support-theory.patch
deleted file mode 100644
index f7393e37f1b2f..0000000000000
--- a/pkgs/applications/science/logic/tamarin-prover/ghc-8.4-support-theory.patch
+++ /dev/null
@@ -1,130 +0,0 @@
-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.
diff --git a/pkgs/applications/science/logic/tamarin-prover/ghc-8.4-support-utils.patch b/pkgs/applications/science/logic/tamarin-prover/ghc-8.4-support-utils.patch
deleted file mode 100644
index d6cd6d73f99e9..0000000000000
--- a/pkgs/applications/science/logic/tamarin-prover/ghc-8.4-support-utils.patch
+++ /dev/null
@@ -1,140 +0,0 @@
-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
diff --git a/pkgs/applications/science/logic/tamarin-prover/sapic-native.patch b/pkgs/applications/science/logic/tamarin-prover/sapic-native.patch
new file mode 100644
index 0000000000000..6ab7e4e7594fe
--- /dev/null
+++ b/pkgs/applications/science/logic/tamarin-prover/sapic-native.patch
@@ -0,0 +1,77 @@
+diff --git a/plugins/sapic/Makefile b/plugins/sapic/Makefile
+index 8f1b1866..678accbe 100644
+--- a/plugins/sapic/Makefile
++++ b/plugins/sapic/Makefile
+@@ -1,18 +1,18 @@
+ TARGET = sapic
+-OBJS= color.cmo exceptions.cmo btree.cmo position.cmo positionplusinit.cmo var.cmo term.cmo fact.cmo atomformulaaction.cmo action.cmo atom.cmo formula.cmo tamarin.cmo sapicterm.cmo sapicvar.cmo sapicaction.cmo lexer.cmo  sapic.cmo annotatedsapicaction.cmo annotatedsapictree.cmo progressfunction.cmo restrictions.cmo annotatedrule.cmo translationhelper.cmo basetranslation.cmo firsttranslation.cmo main.cmo 
++OBJS= color.cmx exceptions.cmx btree.cmx position.cmx positionplusinit.cmx var.cmx term.cmx fact.cmx atomformulaaction.cmx action.cmx atom.cmx formula.cmx tamarin.cmx sapicterm.cmx sapicvar.cmx sapicaction.cmx lexer.cmx  sapic.cmx annotatedsapicaction.cmx annotatedsapictree.cmx progressfunction.cmx restrictions.cmx annotatedrule.cmx translationhelper.cmx basetranslation.cmx firsttranslation.cmx main.cmx
+ FLAGS=-g
+ 
+-OCAMLC    := $(shell command -v ocamlc    2> /dev/null)
++OCAMLOPT  := $(shell command -v ocamlopt  2> /dev/null)
+ OCAMLLEX  := $(shell command -v ocamllex  2> /dev/null)
+ OCAMLYACC := $(shell command -v ocamlyacc 2> /dev/null)
+ OCAMLDEP  := $(shell command -v ocamldep  2> /dev/null)
+-OCAMLC_GTEQ_402 := $(shell expr `ocamlc -version | sed -e 's/\.\([0-9][0-9]\)/\1/g' -e 's/\.\([0-9]\)/0\1/g' -e 's/^[0-9]\{3,4\}$$/&00/'` \>= 40200)
++OCAMLC_GTEQ_402 := $(shell expr `ocamlopt -version | sed -e 's/\.\([0-9][0-9]\)/\1/g' -e 's/\.\([0-9]\)/0\1/g' -e 's/^[0-9]\{3,4\}$$/&00/'` \>= 40200)
+ 
+ default: sapic
+ 
+ sapic:
+-ifdef OCAMLC
+-	@echo "Found ocamlc."
++ifdef OCAMLOPT
++	@echo "Found ocamlopt."
+ ifdef OCAMLLEX
+ 	@echo "Found ocamllex."
+ ifdef OCAMLYACC
+@@ -22,9 +22,9 @@ ifdef OCAMLDEP
+ ifeq "$(OCAMLC_GTEQ_402)" "1"
+ 	@echo "Building SAPIC."
+ 	$(MAKE) $(OBJS)
+-	ocamlc $(FLAGS) -o $@ str.cma $(OBJS)
+-	@echo "Installing SAPIC into ~/.local/bin/"
+-	cp sapic ~/.local/bin
++	ocamlopt $(FLAGS) -o $@ str.cmxa $(OBJS)
++#	@echo "Installing SAPIC into ~/.local/bin/"
++#	cp sapic ~/.local/bin
+ else
+ 	@echo "Found OCAML version < 4.02. SAPIC will not be installed."
+ endif
+@@ -38,7 +38,7 @@ else
+ 	@echo "ocamllex not found. SAPIC will not be installed."
+ endif
+ else
+-	@echo "ocamlc not found. SAPIC will not be installed."
++	@echo "ocamlopt not found. SAPIC will not be installed."
+ endif
+ 
+ depend:
+@@ -48,20 +48,20 @@ lexer.ml: sapic.cmi
+ 
+ .PHONY: clean
+ clean:
+-	rm -rf *.cmi *.cmo $(TARGET)
++	rm -rf *.cmi **.cmx $(TARGET)
+ 	rm -rf sapic.ml sapic.mli lexer.ml lexer.mli
+ 
+-.SUFFIXES: .ml .mli .mll .mly .cmo .cmi
++.SUFFIXES: .ml .mli .mll .mly .cmx .cmi
+ 
+-.ml.cmo:
+-	ocamlc $(FLAGS) -c $<
++.ml.cmx:
++	ocamlopt $(FLAGS) -c $<
+ .mli.cmi:
+-	ocamlc $(FLAGS) -c $<
++	ocamlopt $(FLAGS) -c $<
+ .mll.ml:
+ 	ocamllex $<
+ .mly.ml:
+ 	ocamlyacc $<
+ .ml.mli:
+-	ocamlc -i $< > $@
++	ocamlopt -i $< > $@
+ 
+ -include .depend