Merge remote-tracking branch 'upstream/staging-next' into staging

Conflicts:
	pkgs/development/python-modules/cssutils/default.nix

2 files changed, 250 insertions, 9 deletions

diff --git a/pkgs/applications/science/logic/tamarin-prover/default.nix b/pkgs/applications/science/logic/tamarin-prover/default.nix
index 09ef2d7d46372..2aa92118b03a7 100644
--- a/pkgs/applications/science/logic/tamarin-prover/default.nix
+++ b/pkgs/applications/science/logic/tamarin-prover/default.nix
@@ -1,17 +1,23 @@
-{ haskellPackages, mkDerivation, fetchFromGitHub, fetchpatch, lib, stdenv
+{ haskellPackages, mkDerivation, fetchFromGitHub, applyPatches, lib, stdenv
 # the following are non-haskell dependencies
 , makeWrapper, which, maude, graphviz, glibcLocales
 }:
 
 let
   version = "1.8.0";
-  src = fetchFromGitHub {
-    owner  = "tamarin-prover";
-    repo   = "tamarin-prover";
-    rev    = version;
-    sha256 = "sha256-ujnaUdbjqajmkphOS4Fs4QBCRGX4JZkQ2p1X2jripww=";
+  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
+    ];
   };
 
+
   # tamarin has its own dependencies, but they're kept inside the repo,
   # no submodules. this factors out the common metadata among all derivations
   common = pname: src: {
@@ -34,7 +40,7 @@ let
   tamarin-prover-utils = mkDerivation (common "tamarin-prover-utils" (src + "/lib/utils") // {
     postPatch = replaceSymlinks;
     libraryHaskellDepends = with haskellPackages; [
-      base64-bytestring blaze-builder
+      base64-bytestring blaze-builder list-t
       dlist exceptions fclabels safe SHA syb
     ];
   });
@@ -93,8 +99,6 @@ mkDerivation (common "tamarin-prover" src // {
   isLibrary = false;
   isExecutable = true;
 
-  patches = [ ];
-
   # strip out unneeded deps manually
   doHaddock = false;
   enableSharedExecutables = false;
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
new file mode 100644
index 0000000000000..f6a07f3646cad
--- /dev/null
+++ b/pkgs/applications/science/logic/tamarin-prover/tamarin-prover-1.8.0-ghc-9.6.patch
@@ -0,0 +1,237 @@
+commit 084bd5474d9ac687656c2a3a6b2e1d507febaa98
+Author: Artur Cygan <arczicygan@gmail.com>
+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
+