diff --git a/pkgs/applications/science/logic/tamarin-prover/default.nix b/pkgs/applications/science/logic/tamarin-prover/default.nix index 9056eab71ea3..40378f8c04d5 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 f93919faf54e..000000000000 --- 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 -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 f7393e37f1b2..000000000000 --- 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 -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 d6cd6d73f99e..000000000000 --- 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 -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 000000000000..6ab7e4e7594f --- /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 diff --git a/pkgs/top-level/all-packages.nix b/pkgs/top-level/all-packages.nix index 6c43ae2f354e..1da47294d08b 100644 --- a/pkgs/top-level/all-packages.nix +++ b/pkgs/top-level/all-packages.nix @@ -7081,7 +7081,7 @@ in tamarin-prover = (haskellPackages.callPackage ../applications/science/logic/tamarin-prover { # NOTE: do not use the haskell packages 'graphviz' and 'maude' - inherit maude which sapic; + inherit maude which; graphviz = graphviz-nox; });