def Lake.MainM : Type → Type

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

Equations

• Lake.MainM = EIO Lake.ExitCode

instance Lake.instMonadMainM : Monad MainM

Equations

• Lake.instMonadMainM = inferInstanceAs (Monad (EIO Lake.ExitCode))

instance Lake.instMonadFinallyMainM : MonadFinally MainM

Equations

• Lake.instMonadFinallyMainM = inferInstanceAs (MonadFinally (EIO Lake.ExitCode))

instance Lake.instMonadLiftBaseIOMainM : MonadLift BaseIO MainM

Equations

• Lake.instMonadLiftBaseIOMainM = inferInstanceAs (MonadLift BaseIO (EIO Lake.ExitCode))

Basics

@[inline]

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

Equations

• Lake.MainM.mk x = x

@[inline]

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

Equations

• self.toEIO = self

@[inline]

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

Equations

• self.toBaseIO = self.toEIO.toBaseIO

@[inline]

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

Equations

• self.run = EStateM.map (fun (x : Except Lake.ExitCode α) => match x with | Except.ok a => 0 | Except.error rc => rc) self.toBaseIO

Exits

@[inline]

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

Exit with given return code.

Equations

• Lake.MainM.exit rc = Lake.MainM.mk (throw rc)

instance Lake.MainM.instMonadExit : MonadExit MainM

Equations

• Lake.MainM.instMonadExit = { exit := fun {α : Type} => Lake.MainM.exit }

@[inline]

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

Try this and catch exits.

Equations

• Lake.MainM.tryCatchExit f self = EStateM.tryCatch self.toEIO f

@[inline]

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

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

Equations

• Lake.MainM.tryCatchError f self = Lake.MainM.tryCatchExit (fun (rc : Lake.ExitCode) => if rc = 0 then Lake.exit 0 else f rc) self

@[inline]

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

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

Equations

• Lake.MainM.failure = Lake.exit 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.

Equations

• self.orElse other = Lake.MainM.tryCatchExit (fun (rc : Lake.ExitCode) => if rc = 0 then Lake.exit 0 else other ()) self

Logging and IO

instance Lake.MainM.instMonadLog : MonadLog MainM

Equations

• Lake.MainM.instMonadLog = Lake.MonadLog.stderr

@[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.

Equations

• Lake.MainM.error msg rc = do Lake.logError msg Lake.exit rc

instance Lake.MainM.instMonadError : MonadError MainM

Equations

• Lake.MainM.instMonadError = { error := fun {α : Type} (msg : String) => Lake.MainM.error msg }

instance Lake.MainM.instMonadLiftIO : MonadLift IO MainM

Equations

• Lake.MainM.instMonadLiftIO = { monadLift := fun {α : Type} => Lake.MonadError.runIO }

@[inline]

def Lake.MainM.runLogIO {α : Type} (x : LogIO α) (minLv : LogLevel := LogLevel.info) (ansiMode : AnsiMode := AnsiMode.auto) (out : OutStream := OutStream.stderr) : MainM α

Equations

• One or more equations did not get rendered due to their size.

@[instance 100]

instance Lake.MainM.instMonadLiftLogIO : MonadLift LogIO MainM

Equations

• Lake.MainM.instMonadLiftLogIO = { monadLift := fun {α : Type} (x : Lake.LogIO α) => Lake.MainM.runLogIO x }

@[inline]

def Lake.MainM.runLoggerIO {α : Type} (x : LoggerIO α) (minLv : LogLevel := LogLevel.info) (ansiMode : AnsiMode := AnsiMode.auto) (out : OutStream := OutStream.stderr) : MainM α

Equations

• One or more equations did not get rendered due to their size.

@[instance 100]

instance Lake.MainM.instMonadLiftLoggerIO : MonadLift LoggerIO MainM

Equations

• Lake.MainM.instMonadLiftLoggerIO = { monadLift := fun {α : Type} (x : Lake.LoggerIO α) => Lake.MainM.runLoggerIO x }