def Lake.MainM (α : Type) : Type

The monad in Lake for main-like functions. Supports IO, logging, and exit.

instance Lake.instMonadMainM : Monad MainM

instance Lake.instMonadFinallyMainM : MonadFinally MainM

instance Lake.instMonadLiftBaseIOMainM : MonadLift BaseIO MainM

Basics

@[inline]

def Lake.MainM.mk {α : Type} (x : EIO ExitCode α) : MainM α

@[inline]

def Lake.MainM.toEIO {α : Type} (self : MainM α) : EIO ExitCode α

@[inline]

def Lake.MainM.toBaseIO {α : Type} (self : MainM α) : BaseIO (Except ExitCode α)

@[inline]

def Lake.MainM.run {α : Type} (self : MainM α) : BaseIO ExitCode

Exits

@[inline]

def Lake.MainM.exit {α : Type} (rc : ExitCode) : MainM α

Exit with given return code.

instance Lake.MainM.instMonadExit : MonadExit MainM

@[inline]

def Lake.MainM.tryCatchExit {α : Type} (f : ExitCode → MainM α) (self : MainM α) : MainM α

Try this and catch exits.

@[inline]

def Lake.MainM.tryCatchError {α : Type} (f : ExitCode → MainM α) (self : MainM α) : MainM α

Try this and catch error codes (i.e., non-zero exits).

@[inline]

def Lake.MainM.failure {α : Type} : MainM α

Exit with a generic error code (i.e., 1).

@[inline]

def Lake.MainM.orElse {α : Type} (self : MainM α) (other : Unit → MainM α) : MainM α

If this exits with an error code (i.e., not 0), perform other.

Logging and IO

instance Lake.MainM.instMonadLog : MonadLog MainM

@[inline]

def Lake.MainM.error {α : Type} (msg : String) (rc : ExitCode := 1) : MainM α

Print out a error line with the given message and then exit with an error code.

instance Lake.MainM.instMonadError : MonadError MainM

instance Lake.MainM.instMonadLiftIO : MonadLift IO MainM

@[inline]

def Lake.MainM.runLogIO {α : Type} (x : LogIO α) (cfg : LogConfig := { }) : MainM α

def Lake.MainM.liftLogIO {α : Type} (x : LogIO α) : MainM α

@[instance 100]

instance Lake.MainM.instMonadLiftLogIO : MonadLift LogIO MainM

@[inline]

def Lake.MainM.runLoggerIO {α : Type} (x : LoggerIO α) (cfg : LogConfig := { }) : MainM α

def Lake.MainM.liftLoggerIO {α : Type} (x : LoggerIO α) : MainM α

@[instance 100]

instance Lake.MainM.instMonadLiftLoggerIO : MonadLift LoggerIO MainM