Merge pull request #296524 from NixOS/haskell-updates

 )

import System.Directory (XdgDirectory (XdgCache), getXdgDirectory)

import System.Environment (getArgs)

import System.Exit (die)

import System.Process (readProcess)

import Prelude hiding (id)

import Data.List (sortOn)

data HydraSlownessWorkaroundFlag = HydraSlownessWorkaround | NoHydraSlownessWorkaround

data RequestLogsFlag = RequestLogs | NoRequestLogs

usage :: IO a

usage = die "Usage: get-report [--slow] [EVAL-ID] | ping-maintainers | mark-broken-list [--no-request-logs] | eval-info"

main :: IO ()

main = do

   args <- getArgs

   case args of

      ["get-report", "--slow"] -> getBuildReports HydraSlownessWorkaround

      ["get-report"] -> getBuildReports NoHydraSlownessWorkaround

      "get-report":"--slow":id -> getBuildReports HydraSlownessWorkaround id

      "get-report":id -> getBuildReports NoHydraSlownessWorkaround id

      ["ping-maintainers"] -> printMaintainerPing

      ["mark-broken-list", "--no-request-logs"] -> printMarkBrokenList NoRequestLogs

      ["mark-broken-list"] -> printMarkBrokenList RequestLogs

      ["eval-info"] -> printEvalInfo

      _ -> putStrLn "Usage: get-report [--slow] | ping-maintainers | mark-broken-list [--no-request-logs] | eval-info"

      _ -> usage

reportFileName :: IO FilePath

reportFileName = getXdgDirectory XdgCache "haskell-updates-build-report.json"

showT :: Show a => a -> Text

showT = Text.pack . show

getBuildReports :: HydraSlownessWorkaroundFlag -> IO ()

getBuildReports opt = runReq defaultHttpConfig do

getBuildReports :: HydraSlownessWorkaroundFlag -> [String] -> IO ()

getBuildReports opt args = runReq defaultHttpConfig do

   eval@Eval{id} <- case args of

      [id] -> hydraJSONQuery mempty ["eval", Text.pack id]

      [] -> do

         evalMay <- Seq.lookup 0 . evals <$> hydraJSONQuery mempty ["jobset", "nixpkgs", "haskell-updates", "evals"]

   eval@Eval{id} <- maybe (liftIO $ fail "No Evaluation found") pure evalMay

         maybe (liftIO $ fail "No Evaluation found") pure evalMay

      _ -> liftIO usage

   liftIO . putStrLn $ "Fetching evaluation " <> show id <> " from Hydra. This might take a few minutes..."

   buildReports <- getEvalBuilds opt id

   buildReports <- getEvalBuilds opt eval

   liftIO do

      fileName <- reportFileName

      putStrLn $ "Finished fetching all builds from Hydra, saving report as " <> fileName

      now <- getCurrentTime

      encodeFile fileName (eval, now, buildReports)

getEvalBuilds :: HydraSlownessWorkaroundFlag -> Int -> Req (Seq Build)

getEvalBuilds NoHydraSlownessWorkaround id =

getEvalBuilds :: HydraSlownessWorkaroundFlag -> Eval -> Req (Seq Build)

getEvalBuilds NoHydraSlownessWorkaround Eval{id} =

  hydraJSONQuery mempty ["eval", showT id, "builds"]

getEvalBuilds HydraSlownessWorkaround id = do

  Eval{builds} <- hydraJSONQuery mempty [ "eval", showT id ]

getEvalBuilds HydraSlownessWorkaround Eval{builds} = do

  forM builds $ \buildId -> do

    liftIO $ putStrLn $ "Querying build " <> show buildId

    hydraJSONQuery mempty [ "build", showT buildId ]

  };

  testScript = ''

    assert (

        "${pkgs.agdaPackages.lib.interfaceFile "Everything.agda"}" == "Everything.agdai"

    ), "wrong interface file for Everything.agda"

    assert (

        "${pkgs.agdaPackages.lib.interfaceFile "tmp/Everything.agda.md"}" == "tmp/Everything.agdai"

    ), "wrong interface file for tmp/Everything.agda.md"

    # Minimal script that typechecks

    machine.succeed("touch TestEmpty.agda")

    machine.succeed("agda TestEmpty.agda")

{ 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 = 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

  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

    ];

  });

  isLibrary = false;

  isExecutable = true;

  patches = [ ];

  # strip out unneeded deps manually

  doHaddock = false;

  enableSharedExecutables = false;

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

    mkdir -p $out/bin

    makeWrapper ${Agda}/bin/agda $out/bin/agda \

      --add-flags "--with-compiler=${ghc}/bin/ghc" \

      --add-flags "--library-file=${library-file}" \

      --add-flags "--local-interfaces"

      --add-flags "--library-file=${library-file}"

    ln -s ${Agda}/bin/agda-mode $out/bin/agda-mode

    ''; # Local interfaces has been added for now: See https://github.com/agda/agda/issues/4526

    '';

  withPackages = arg: if builtins.isAttrs arg then withPackages' arg else withPackages' { pkgs = arg; };

        buildPhase = if buildPhase != null then buildPhase else ''

          runHook preBuild

          agda ${includePathArgs} ${everythingFile}

          rm ${everythingFile} ${lib.interfaceFile Agda.version everythingFile}

          runHook postBuild

        '';

        installPhase = if installPhase != null then installPhase else ''

          runHook preInstall

          mkdir -p $out

          find -not \( -path ${everythingFile} -or -path ${lib.interfaceFile everythingFile} \) -and \( ${concatMapStringsSep " -or " (p: "-name '*.${p}'") (extensions ++ extraExtensions)} \) -exec cp -p --parents -t "$out" {} +

          find \( ${concatMapStringsSep " -or " (p: "-name '*.${p}'") (extensions ++ extraExtensions)} \) -exec cp -p --parents -t "$out" {} +

          runHook postInstall

        '';