From 71408df70fd5bfbc0e5fc3776a942e2b0b93dad6 Mon Sep 17 00:00:00 2001 From: Vincent Laporte Date: Wed, 30 Oct 2024 14:13:40 +0100 Subject: [PATCH] =?UTF-8?q?tamarin-prover:=201.8.0=20=E2=86=92=201.10.0?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- .../science/logic/tamarin-prover/default.nix | 27 +- .../tamarin-prover-1.8.0-ghc-9.6.patch | 237 ------------------ 2 files changed, 10 insertions(+), 254 deletions(-) delete mode 100644 pkgs/applications/science/logic/tamarin-prover/tamarin-prover-1.8.0-ghc-9.6.patch diff --git a/pkgs/applications/science/logic/tamarin-prover/default.nix b/pkgs/applications/science/logic/tamarin-prover/default.nix index e621b36a773bb..698b4ddc47da5 100644 --- a/pkgs/applications/science/logic/tamarin-prover/default.nix +++ b/pkgs/applications/science/logic/tamarin-prover/default.nix @@ -1,20 +1,15 @@ -{ haskellPackages, mkDerivation, fetchFromGitHub, applyPatches, lib, stdenv +{ haskellPackages, mkDerivation, fetchFromGitHub, lib, stdenv # the following are non-haskell dependencies , makeWrapper, which, maude, graphviz, glibcLocales }: let - version = "1.8.0"; - src = applyPatches { - src = fetchFromGitHub { - owner = "tamarin-prover"; - repo = "tamarin-prover"; - rev = version; - sha256 = "sha256-ujnaUdbjqajmkphOS4Fs4QBCRGX4JZkQ2p1X2jripww="; - }; - patches = [ - ./tamarin-prover-1.8.0-ghc-9.6.patch - ]; + version = "1.10.0"; + src = fetchFromGitHub { + owner = "tamarin-prover"; + repo = "tamarin-prover"; + rev = version; + hash = "sha256-v1BruU2p/Sg/g7b9a+QRza46bD7PkMtsGq82qFaNhpI="; }; @@ -41,7 +36,7 @@ let postPatch = replaceSymlinks; libraryHaskellDepends = with haskellPackages; [ base64-bytestring blaze-builder list-t - dlist exceptions fclabels safe SHA syb + dlist exceptions fclabels haskellPackages.graphviz safe SHA split syb ]; }); @@ -84,9 +79,7 @@ let tamarin-prover-export = mkDerivation (common "tamarin-prover-export" (src + "/lib/export") // { postPatch = "cp --remove-destination ${src}/LICENSE ."; doHaddock = false; # broken - libraryHaskellDepends = (with haskellPackages; [ - HStringTemplate - ]) ++ [ + libraryHaskellDepends = [ tamarin-prover-utils tamarin-prover-term tamarin-prover-theory @@ -125,7 +118,7 @@ mkDerivation (common "tamarin-prover" src // { executableHaskellDepends = (with haskellPackages; [ binary-instances binary-orphans blaze-html conduit file-embed - gitrev http-types lifted-base monad-control + gitrev http-types resourcet shakespeare threads wai warp yesod-core yesod-static ]) ++ [ tamarin-prover-utils tamarin-prover-sapic diff --git a/pkgs/applications/science/logic/tamarin-prover/tamarin-prover-1.8.0-ghc-9.6.patch b/pkgs/applications/science/logic/tamarin-prover/tamarin-prover-1.8.0-ghc-9.6.patch deleted file mode 100644 index f6a07f3646cad..0000000000000 --- a/pkgs/applications/science/logic/tamarin-prover/tamarin-prover-1.8.0-ghc-9.6.patch +++ /dev/null @@ -1,237 +0,0 @@ -commit 084bd5474d9ac687656c2a3a6b2e1d507febaa98 -Author: Artur Cygan -Date: Mon Feb 26 10:04:48 2024 +0100 - - Update to GHC 9.6 (#618) - - Cherry-picked from b3e18f61e45d701d42d794bc91ccbb4c0e3834ec. - - Removing Control.Monad.List - -diff --git a/lib/sapic/src/Sapic/Exceptions.hs b/lib/sapic/src/Sapic/Exceptions.hs -index 146b721e..b9962478 100644 ---- a/lib/sapic/src/Sapic/Exceptions.hs -+++ b/lib/sapic/src/Sapic/Exceptions.hs -@@ -23,7 +23,6 @@ import Theory.Sapic - import Data.Label - import qualified Data.Maybe - import Theory.Text.Pretty --import Sapic.Annotation --toAnProcess - import Theory.Sapic.Print (prettySapic) - import qualified Theory.Text.Pretty as Pretty - -@@ -67,14 +66,14 @@ data ExportException = UnsupportedBuiltinMS - | UnsupportedTypes [String] - - instance Show ExportException where -- -+ - show (UnsupportedTypes incorrectFunctionUsages) = do - let functionsString = List.intercalate ", " incorrectFunctionUsages - (case length functionsString of - 1 -> "The function " ++ functionsString ++ ", which is declared with a user-defined type, appears in a rewrite rule. " - _ -> "The functions " ++ functionsString ++ ", which are declared with a user-defined type, appear in a rewrite rule. ") - ++ "However, the translation of rules only works with bitstrings at the moment." -- show unsuppBuiltin = -+ show unsuppBuiltin = - "The builtins bilinear-pairing and multiset are not supported for export. However, your model uses " ++ - (case unsuppBuiltin of - UnsupportedBuiltinBP -> "bilinear-pairing." -@@ -93,7 +92,7 @@ instance Show (SapicException an) where - show (InvalidPosition p) = "Invalid position:" ++ prettyPosition p - show (NotImplementedError s) = "This feature is not implemented yet. Sorry! " ++ s - show (ImplementationError s) = "You've encountered an error in the implementation: " ++ s -- show a@(ProcessNotWellformed e p) = "Process not well-formed: " ++ Pretty.render (text (show e) $-$ nest 2 (maybe emptyDoc prettySapic p)) -+ show (ProcessNotWellformed e p) = "Process not well-formed: " ++ Pretty.render (text (show e) $-$ nest 2 (maybe emptyDoc prettySapic p)) - show ReliableTransmissionButNoProcess = "The builtin support for reliable channels currently only affects the process calculus, but you have not specified a top-level process. Please remove \"builtins: reliable-channel\" to proceed." - show (CannotExpandPredicate facttag rstr) = "Undefined predicate " - ++ showFactTagArity facttag -@@ -135,7 +134,7 @@ instance Show WFerror where - ++ prettySapicFunType t2 - ++ "." - show (FunctionNotDefined sym ) = "Function not defined " ++ show sym -- -+ - - instance Exception WFerror - instance (Typeable an) => Exception (SapicException an) -diff --git a/lib/term/src/Term/Narrowing/Narrow.hs b/lib/term/src/Term/Narrowing/Narrow.hs -index 56f145d9..88f89aa1 100644 ---- a/lib/term/src/Term/Narrowing/Narrow.hs -+++ b/lib/term/src/Term/Narrowing/Narrow.hs -@@ -12,6 +12,7 @@ module Term.Narrowing.Narrow ( - import Term.Unification - import Term.Positions - -+import Control.Monad - import Control.Monad.Reader - - import Extension.Prelude -diff --git a/lib/term/src/Term/Unification.hs b/lib/term/src/Term/Unification.hs -index b5c107cd..fcf52128 100644 ---- a/lib/term/src/Term/Unification.hs -+++ b/lib/term/src/Term/Unification.hs -@@ -61,7 +61,7 @@ module Term.Unification ( - , pairDestMaudeSig - , symEncDestMaudeSig - , asymEncDestMaudeSig -- , signatureDestMaudeSig -+ , signatureDestMaudeSig - , locationReportMaudeSig - , revealSignatureMaudeSig - , hashMaudeSig -@@ -80,7 +80,7 @@ module Term.Unification ( - , module Term.Rewriting.Definitions - ) where - ---- import Control.Applicative -+import Control.Monad - import Control.Monad.RWS - import Control.Monad.Except - import Control.Monad.State -diff --git a/lib/theory/src/Theory/Constraint/System/Guarded.hs b/lib/theory/src/Theory/Constraint/System/Guarded.hs -index 99f985a8..3f0cd8d8 100644 ---- a/lib/theory/src/Theory/Constraint/System/Guarded.hs -+++ b/lib/theory/src/Theory/Constraint/System/Guarded.hs -@@ -88,6 +88,7 @@ module Theory.Constraint.System.Guarded ( - - import Control.Arrow - import Control.DeepSeq -+import Control.Monad - import Control.Monad.Except - import Control.Monad.Fresh (MonadFresh, scopeFreshness) - import qualified Control.Monad.Trans.PreciseFresh as Precise (Fresh, evalFresh, evalFreshT) -diff --git a/lib/utils/src/Control/Monad/Trans/Disj.hs b/lib/utils/src/Control/Monad/Trans/Disj.hs -index 96dae742..b3b63825 100644 ---- a/lib/utils/src/Control/Monad/Trans/Disj.hs -+++ b/lib/utils/src/Control/Monad/Trans/Disj.hs -@@ -18,10 +18,10 @@ module Control.Monad.Trans.Disj ( - , runDisjT - ) where - ---- import Control.Applicative --import Control.Monad.List --import Control.Monad.Reader -+import Control.Monad - import Control.Monad.Disj.Class -+import Control.Monad.Reader -+import ListT - - - ------------------------------------------------------------------------------ -@@ -33,12 +33,12 @@ newtype DisjT m a = DisjT { unDisjT :: ListT m a } - deriving (Functor, Applicative, MonadTrans ) - - -- | Construct a 'DisjT' action. --disjT :: m [a] -> DisjT m a --disjT = DisjT . ListT -+disjT :: (Monad m, Foldable m) => m a -> DisjT m a -+disjT = DisjT . fromFoldable - - -- | Run a 'DisjT' action. --runDisjT :: DisjT m a -> m [a] --runDisjT = runListT . unDisjT -+runDisjT :: Monad m => DisjT m a -> m [a] -+runDisjT = toList . unDisjT - - - -@@ -47,8 +47,6 @@ runDisjT = runListT . unDisjT - ------------ - - instance Monad m => Monad (DisjT m) where -- {-# INLINE return #-} -- return = DisjT . return - {-# INLINE (>>=) #-} - m >>= f = DisjT $ (unDisjT . f) =<< unDisjT m - -diff --git a/lib/utils/tamarin-prover-utils.cabal b/lib/utils/tamarin-prover-utils.cabal -index 75ed2b46..bb54d1e5 100644 ---- a/lib/utils/tamarin-prover-utils.cabal -+++ b/lib/utils/tamarin-prover-utils.cabal -@@ -47,6 +47,7 @@ library - , deepseq - , dlist - , fclabels -+ , list-t - , mtl - , pretty - , safe -diff --git a/src/Main/Mode/Batch.hs b/src/Main/Mode/Batch.hs -index e7710682..d370da85 100644 ---- a/src/Main/Mode/Batch.hs -+++ b/src/Main/Mode/Batch.hs -@@ -32,7 +32,8 @@ import Main.TheoryLoader - import Main.Utils - - import Theory.Module --import Control.Monad.Except (MonadIO(liftIO), runExceptT) -+import Control.Monad.Except (runExceptT) -+import Control.Monad.IO.Class (MonadIO(liftIO)) - import System.Exit (die) - import Theory.Tools.Wellformedness (prettyWfErrorReport) - import Text.Printf (printf) -diff --git a/src/Main/TheoryLoader.hs b/src/Main/TheoryLoader.hs -index 7fffb85b..71fba2b9 100644 ---- a/src/Main/TheoryLoader.hs -+++ b/src/Main/TheoryLoader.hs -@@ -42,8 +42,6 @@ module Main.TheoryLoader ( - - ) where - ---- import Debug.Trace -- - import Prelude hiding (id, (.)) - - import Data.Char (toLower) -@@ -58,8 +56,10 @@ import Data.Bifunctor (Bifunctor(bimap)) - import Data.Bitraversable (Bitraversable(bitraverse)) - - import Control.Category --import Control.Exception (evaluate) - import Control.DeepSeq (force) -+import Control.Exception (evaluate) -+import Control.Monad -+import Control.Monad.IO.Class (MonadIO(liftIO)) - - import System.Console.CmdArgs.Explicit - import System.Timeout (timeout) -@@ -387,10 +387,10 @@ closeTheory version thyOpts sign srcThy = do - deducThy <- bitraverse (return . addMessageDeductionRuleVariants) - (return . addMessageDeductionRuleVariantsDiff) transThy - -- derivCheckSignature <- Control.Monad.Except.liftIO $ toSignatureWithMaude (get oMaudePath thyOpts) $ maudePublicSig (toSignaturePure sign) -+ derivCheckSignature <- liftIO $ toSignatureWithMaude (get oMaudePath thyOpts) $ maudePublicSig (toSignaturePure sign) - variableReport <- case compare derivChecks 0 of - EQ -> pure $ Just [] -- _ -> Control.Monad.Except.liftIO $ timeout (1000000 * derivChecks) $ evaluate . force $ (either (\t -> checkVariableDeducability t derivCheckSignature autoSources defaultProver) -+ _ -> liftIO $ timeout (1000000 * derivChecks) $ evaluate . force $ (either (\t -> checkVariableDeducability t derivCheckSignature autoSources defaultProver) - (\t-> diffCheckVariableDeducability t derivCheckSignature autoSources defaultProver defaultDiffProver) deducThy) - - let report = wellformednessReport ++ (fromMaybe [(underlineTopic "Derivation Checks", Pretty.text "Derivation checks timed out. Use --derivcheck-timeout=INT to configure timeout, 0 to deactivate.")] variableReport) -diff --git a/stack.yaml b/stack.yaml -index 7267ba17..b53f6ff8 100644 ---- a/stack.yaml -+++ b/stack.yaml -@@ -7,7 +7,7 @@ packages: - - lib/sapic/ - - lib/export/ - - lib/accountability/ --resolver: lts-20.26 -+resolver: lts-22.11 - ghc-options: - "$everything": -Wall - nix: -diff --git a/tamarin-prover.cabal b/tamarin-prover.cabal -index 89a7e3a8..986274ea 100644 ---- a/tamarin-prover.cabal -+++ b/tamarin-prover.cabal -@@ -106,7 +106,7 @@ executable tamarin-prover - default-language: Haskell2010 - - if flag(threaded) -- ghc-options: -threaded -eventlog -+ ghc-options: -threaded - - -- -XFlexibleInstances -