inductive Lake.Verbosity : Type

• quiet: Lake.Verbosity
• normal: Lake.Verbosity
• verbose: Lake.Verbosity

instance Lake.instReprVerbosity : Repr Lake.Verbosity

Equations

• Lake.instReprVerbosity = { reprPrec := Lake.reprVerbosity✝ }

instance Lake.instDecidableEqVerbosity : DecidableEq Lake.Verbosity

Equations

• Lake.instDecidableEqVerbosity x y = if h : x.toCtorIdx = y.toCtorIdx then isTrue ⋯ else isFalse ⋯

instance Lake.instOrdVerbosity : Ord Lake.Verbosity

instance Lake.instLTVerbosity : LT Lake.Verbosity

instance Lake.instLEVerbosity : LE Lake.Verbosity

Equations

• Lake.instLEVerbosity = leOfOrd

instance Lake.instMinVerbosity : Min Lake.Verbosity

instance Lake.instMaxVerbosity : Max Lake.Verbosity

instance Lake.instInhabitedVerbosity : Inhabited Lake.Verbosity

inductive Lake.AnsiMode : Type

Whether to ANSI escape codes.

• auto: Lake.AnsiMode

  Automatically determine whether to use ANSI escape codes based on whether the stream written to is a terminal.

• ansi: Lake.AnsiMode

  Use ANSI escape codes.

• noAnsi: Lake.AnsiMode

  Do not use ANSI escape codes.

def Lake.AnsiMode.isEnabled (out : IO.FS.Stream) : Lake.AnsiMode → BaseIO Bool

Returns whether to ANSI escape codes with the stream out.

Equations

• Lake.AnsiMode.isEnabled out Lake.AnsiMode.auto = out.isTty
• Lake.AnsiMode.isEnabled out Lake.AnsiMode.ansi = pure true
• Lake.AnsiMode.isEnabled out Lake.AnsiMode.noAnsi = pure false

def Lake.Ansi.chalk (colorCode text : String) : String

Wrap text in ANSI escape sequences to make it bold and color it the ANSI colorCode. Resets all terminal font attributes at the end of the text.

Equations

• Lake.Ansi.chalk colorCode text = toString "\x1b[1;" ++ toString colorCode ++ toString "m" ++ toString text ++ toString "\x1b[m"

inductive Lake.OutStream : Type

A pure representation of output stream.

• stdout: Lake.OutStream
• stderr: Lake.OutStream
• stream: IO.FS.Stream → Lake.OutStream

def Lake.OutStream.get : Lake.OutStream → BaseIO IO.FS.Stream

Returns the real output stream associated with OutStream.

Equations

• Lake.OutStream.stdout.get = IO.getStdout
• Lake.OutStream.stderr.get = IO.getStderr
• (Lake.OutStream.stream s).get = pure s

instance Lake.instCoeStreamOutStream : Coe IO.FS.Stream Lake.OutStream

instance Lake.instCoeHandleOutStream : Coe IO.FS.Handle Lake.OutStream

Equations

• Lake.instCoeHandleOutStream = { coe := fun (h : IO.FS.Handle) => Lake.OutStream.stream (IO.FS.Stream.ofHandle h) }

inductive Lake.LogLevel : Type

• trace: Lake.LogLevel
• info: Lake.LogLevel
• warning: Lake.LogLevel
• error: Lake.LogLevel

instance Lake.instInhabitedLogLevel : Inhabited Lake.LogLevel

instance Lake.instReprLogLevel : Repr Lake.LogLevel

instance Lake.instDecidableEqLogLevel : DecidableEq Lake.LogLevel

instance Lake.instOrdLogLevel : Ord Lake.LogLevel

Equations

• Lake.instOrdLogLevel = { compare := Lake.ordLogLevel✝ }

instance Lake.instToJsonLogLevel : Lean.ToJson Lake.LogLevel

instance Lake.instFromJsonLogLevel : Lean.FromJson Lake.LogLevel

Equations

• Lake.instFromJsonLogLevel = { fromJson? := Lake.fromJsonLogLevel✝ }

instance Lake.instLTLogLevel : LT Lake.LogLevel

Equations

• Lake.instLTLogLevel = ltOfOrd

instance Lake.instLELogLevel : LE Lake.LogLevel

Equations

• Lake.instLELogLevel = leOfOrd

instance Lake.instMinLogLevel : Min Lake.LogLevel

Equations

• Lake.instMinLogLevel = minOfLe

instance Lake.instMaxLogLevel : Max Lake.LogLevel

Equations

• Lake.instMaxLogLevel = maxOfLe

def Lake.LogLevel.icon : Lake.LogLevel → Char

Unicode icon for representing the log level.

Equations

• Lake.LogLevel.trace.icon = 'ℹ'
• Lake.LogLevel.info.icon = 'ℹ'
• Lake.LogLevel.warning.icon = '⚠'
• Lake.LogLevel.error.icon = '✖'

def Lake.LogLevel.ansiColor : Lake.LogLevel → String

ANSI escape code for coloring text of at the log level.

def Lake.LogLevel.ofString? (s : String) : Option Lake.LogLevel

def Lake.LogLevel.toString : Lake.LogLevel → String

instance Lake.instToStringLogLevel : ToString Lake.LogLevel

def Lake.LogLevel.ofMessageSeverity : Lean.MessageSeverity → Lake.LogLevel

def Lake.LogLevel.toMessageSeverity : Lake.LogLevel → Lean.MessageSeverity

Equations

• Lake.LogLevel.info.toMessageSeverity = Lean.MessageSeverity.information
• Lake.LogLevel.trace.toMessageSeverity = Lean.MessageSeverity.information
• Lake.LogLevel.warning.toMessageSeverity = Lean.MessageSeverity.warning
• Lake.LogLevel.error.toMessageSeverity = Lean.MessageSeverity.error

def Lake.Verbosity.minLogLv : Lake.Verbosity → Lake.LogLevel

structure Lake.LogEntry : Type

• level : Lake.LogLevel
• message : String

instance Lake.instInhabitedLogEntry : Inhabited Lake.LogEntry

instance Lake.instToJsonLogEntry : Lean.ToJson Lake.LogEntry

instance Lake.instFromJsonLogEntry : Lean.FromJson Lake.LogEntry

Equations

• Lake.instFromJsonLogEntry = { fromJson? := Lake.fromJsonLogEntry✝ }

def Lake.LogEntry.toString (self : Lake.LogEntry) (useAnsi : Bool := false) : String

Equations

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

instance Lake.instToStringLogEntry : ToString Lake.LogEntry

class Lake.MonadLog (m : Type u → Type v) : Type v

• logEntry : Lake.LogEntry → m PUnit

@[inline]

def Lake.logVerbose {m : Type u_1 → Type u_2} [Monad m] [Lake.MonadLog m] (message : String) : m PUnit

Equations

• Lake.logVerbose message = Lake.logEntry { level := Lake.LogLevel.trace, message := message }

@[inline]

def Lake.logInfo {m : Type u_1 → Type u_2} [Monad m] [Lake.MonadLog m] (message : String) : m PUnit

Equations

• Lake.logInfo message = Lake.logEntry { level := Lake.LogLevel.info, message := message }

@[inline]

def Lake.logWarning {m : Type u_1 → Type u_2} [Lake.MonadLog m] (message : String) : m PUnit

@[inline]

def Lake.logError {m : Type u_1 → Type u_2} [Lake.MonadLog m] (message : String) : m PUnit

Equations

• Lake.logError message = Lake.logEntry { level := Lake.LogLevel.error, message := message }

@[specialize #[]]

def Lake.logSerialMessage {m : Type u_1 → Type u_2} (msg : Lean.SerialMessage) [Lake.MonadLog m] : m PUnit

Equations

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

@[deprecated]

def Lake.logToIO (e : Lake.LogEntry) (minLv : Lake.LogLevel) : BaseIO PUnit

Equations

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

def Lake.logToStream (e : Lake.LogEntry) (out : IO.FS.Stream) (minLv : Lake.LogLevel) (useAnsi : Bool) : BaseIO PUnit

Equations

• Lake.logToStream e out minLv useAnsi = if e.level ≥ minLv then EIO.catchExceptions (out.putStrLn (e.toString useAnsi)) fun (x : IO.Error) => pure () else pure PUnit.unit

@[reducible, inline]

abbrev Lake.MonadLog.nop {m : Type → Type u_1} [Pure m] : Lake.MonadLog m

Equations

• Lake.MonadLog.nop = { logEntry := fun (x : Lake.LogEntry) => pure () }

instance Lake.MonadLog.instInhabitedOfPure {m : Type → Type u_1} [Pure m] : Inhabited (Lake.MonadLog m)

Equations

• Lake.MonadLog.instInhabitedOfPure = { default := Lake.MonadLog.nop }

@[reducible, inline]

abbrev Lake.MonadLog.lift {m : Type u_1 → Type u_2} {n : Type u_1 → Type u_3} [MonadLiftT m n] (self : Lake.MonadLog m) : Lake.MonadLog n

instance Lake.MonadLog.instOfMonadLift {m : Type u_1 → Type u_2} {n : Type u_1 → Type u_3} [MonadLift m n] [methods : Lake.MonadLog m] : Lake.MonadLog n

@[reducible, inline, deprecated]

abbrev Lake.MonadLog.io {m : Type → Type u_1} [MonadLiftT BaseIO m] (minLv : Lake.LogLevel := Lake.LogLevel.info) : Lake.MonadLog m

@[reducible, inline]

abbrev Lake.MonadLog.stream {m : Type → Type u_1} [MonadLiftT BaseIO m] (out : IO.FS.Stream) (minLv : Lake.LogLevel := Lake.LogLevel.info) (useAnsi : Bool := false) : Lake.MonadLog m

Equations

• Lake.MonadLog.stream out minLv useAnsi = { logEntry := fun (e : Lake.LogEntry) => liftM (Lake.logToStream e out minLv useAnsi) }

@[inline]

def Lake.MonadLog.error {m : Type u_1 → Type u_2} {α : Type u_1} [Alternative m] [Lake.MonadLog m] (msg : String) : m α

def Lake.OutStream.logEntry (self : Lake.OutStream) (e : Lake.LogEntry) (minLv : Lake.LogLevel := Lake.LogLevel.info) (ansiMode : Lake.AnsiMode := Lake.AnsiMode.auto) : BaseIO PUnit

@[reducible, inline]

abbrev Lake.OutStream.logger {m : Type → Type u_1} [MonadLiftT BaseIO m] (out : Lake.OutStream) (minLv : Lake.LogLevel := Lake.LogLevel.info) (ansiMode : Lake.AnsiMode := Lake.AnsiMode.auto) : Lake.MonadLog m

Equations

• out.logger minLv ansiMode = { logEntry := fun (e : Lake.LogEntry) => liftM (out.logEntry e minLv ansiMode) }

@[reducible, inline]

abbrev Lake.MonadLog.stdout {m : Type → Type u_1} [MonadLiftT BaseIO m] (minLv : Lake.LogLevel := Lake.LogLevel.info) (ansiMode : Lake.AnsiMode := Lake.AnsiMode.auto) : Lake.MonadLog m

Equations

• Lake.MonadLog.stdout minLv ansiMode = Lake.OutStream.stdout.logger minLv ansiMode

@[reducible, inline]

abbrev Lake.MonadLog.stderr {m : Type → Type u_1} [MonadLiftT BaseIO m] (minLv : Lake.LogLevel := Lake.LogLevel.info) (ansiMode : Lake.AnsiMode := Lake.AnsiMode.auto) : Lake.MonadLog m

Equations

• Lake.MonadLog.stderr minLv ansiMode = Lake.OutStream.stderr.logger minLv ansiMode

@[inline]

def Lake.OutStream.getLogger {m : Type → Type} [MonadLiftT BaseIO m] (out : Lake.OutStream) (minLv : Lake.LogLevel := Lake.LogLevel.info) (ansiMode : Lake.AnsiMode := Lake.AnsiMode.auto) : BaseIO (Lake.MonadLog m)

@[reducible, inline]

abbrev Lake.MonadLogT (m : Type u → Type v) (n : Type v → Type w) (α : Type v) : Type (max v w)

A monad equipped with a MonadLog instance

instance Lake.MonadLogT.instInhabitedOfPure {n : Type u_1 → Type u_2} {α : Type u_1} {m : Type u_3 → Type u_1} [Pure n] [Inhabited α] : Inhabited (Lake.MonadLogT m n α)

Equations

• Lake.MonadLogT.instInhabitedOfPure = { default := fun (x : Lake.MonadLog m) => pure default }

instance Lake.MonadLogT.instMonadLogOfMonadOfMonadLiftT {n : Type u_1 → Type u_2} {m : Type u_1 → Type u_1} [Monad n] [MonadLiftT m n] : Lake.MonadLog (Lake.MonadLogT m n)

@[inline]

def Lake.MonadLogT.adaptMethods {n : Type u_1 → Type u_2} {m : Type u_3 → Type u_1} {m' : Type u_4 → Type u_1} {α : Type u_1} [Monad n] (f : Lake.MonadLog m → Lake.MonadLog m') (self : Lake.MonadLogT m' n α) : Lake.MonadLogT m n α

Equations

• Lake.MonadLogT.adaptMethods f self = ReaderT.adapt f self

@[inline]

def Lake.MonadLogT.ignoreLog {m : Type → Type u_1} {n : Type u_1 → Type u_2} {α : Type u_1} [Pure m] (self : Lake.MonadLogT m n α) : n α

structure Lake.Log : Type

• entries : Array Lake.LogEntry

instance Lake.instToJsonLog : Lean.ToJson Lake.Log

Equations

• Lake.instToJsonLog = { toJson := fun (x : Lake.Log) => Lean.toJson x.entries }

instance Lake.instFromJsonLog : Lean.FromJson Lake.Log

structure Lake.Log.Pos : Type

A position in a Log (i.e., an array index). Can be past the log's end.

• val : Nat

instance Lake.Log.instInhabitedPos : Inhabited Lake.Log.Pos

Equations

• Lake.Log.instInhabitedPos = { default := { val := default } }

instance Lake.instOfNatPos : OfNat Lake.Log.Pos 0

@[inline]

def Lake.Log.empty : Lake.Log

Equations

• Lake.Log.empty = { entries := #[] }

instance Lake.Log.instEmptyCollection : EmptyCollection Lake.Log

Equations

• Lake.Log.instEmptyCollection = { emptyCollection := Lake.Log.empty }

@[inline]

def Lake.Log.size (log : Lake.Log) : Nat

Equations

• log.size = log.entries.size

@[inline]

def Lake.Log.isEmpty (log : Lake.Log) : Bool

@[inline]

def Lake.Log.hasEntries (log : Lake.Log) : Bool

@[inline]

def Lake.Log.endPos (log : Lake.Log) : Lake.Log.Pos

Equations

• log.endPos = { val := log.entries.size }

@[inline]

def Lake.Log.push (log : Lake.Log) (e : Lake.LogEntry) : Lake.Log

Equations

• log.push e = { entries := log.entries.push e }

@[inline]

def Lake.Log.append (log o : Lake.Log) : Lake.Log

instance Lake.Log.instAppend : Append Lake.Log

@[inline]

def Lake.Log.extract (log : Lake.Log) (start stop : Lake.Log.Pos) : Lake.Log

Takes log entries between start (inclusive) and stop (exclusive).

Equations

• log.extract start stop = { entries := log.entries.extract start.val stop.val }

@[inline]

def Lake.Log.dropFrom (log : Lake.Log) (pos : Lake.Log.Pos) : Lake.Log

Removes log entries after pos (inclusive).

@[inline]

def Lake.Log.takeFrom (log : Lake.Log) (pos : Lake.Log.Pos) : Lake.Log

Takes log entries before pos (exclusive).

@[inline]

def Lake.Log.split (log : Lake.Log) (pos : Lake.Log.Pos) : Lake.Log × Lake.Log

Splits the log into two from pos. The first log is from the start to pos (exclusive), and the second log is from pos (inclusive) to the end.

Equations

• log.split pos = (log.dropFrom pos, log.takeFrom pos)

def Lake.Log.toString (log : Lake.Log) : String

instance Lake.Log.instToString : ToString Lake.Log

Equations

• Lake.Log.instToString = { toString := Lake.Log.toString }

@[inline]

def Lake.Log.replay {m : Type u_1 → Type u_2} [Monad m] [logger : Lake.MonadLog m] (log : Lake.Log) : m PUnit

Equations

• log.replay = Array.forM (fun (e : Lake.LogEntry) => Lake.logEntry e) log.entries

@[inline]

def Lake.Log.filter (f : Lake.LogEntry → Bool) (log : Lake.Log) : Lake.Log

@[inline]

def Lake.Log.any (f : Lake.LogEntry → Bool) (log : Lake.Log) : Bool

def Lake.Log.maxLv (log : Lake.Log) : Lake.LogLevel

The max log level of entries in this log. If empty, returns trace.

Equations

• log.maxLv = Array.foldl (fun (x1 : Lake.LogLevel) (x2 : Lake.LogEntry) => max x1 x2.level) Lake.LogLevel.trace log.entries

@[inline]

def Lake.pushLogEntry {m : Type → Type u_1} [MonadStateOf Lake.Log m] (e : Lake.LogEntry) : m PUnit

Add a LogEntry to the end of the monad's Log.

Equations

• Lake.pushLogEntry e = modify fun (x : Lake.Log) => x.push e

@[reducible, inline]

abbrev Lake.MonadLog.ofMonadState {m : Type → Type u_1} [MonadStateOf Lake.Log m] : Lake.MonadLog m

Equations

• Lake.MonadLog.ofMonadState = { logEntry := Lake.pushLogEntry }

@[inline]

def Lake.getLog {m : Type → Type u_1} [MonadStateOf Lake.Log m] : m Lake.Log

Returns the monad's log.

Equations

• Lake.getLog = get

@[inline]

def Lake.getLogPos {m : Type → Type u_1} [Functor m] [MonadStateOf Lake.Log m] : m Lake.Log.Pos

Returns the current end position of the monad's log (i.e., its size).

Equations

• Lake.getLogPos = (fun (x : Lake.Log) => x.endPos) <$> Lake.getLog

@[inline]

def Lake.takeLog {m : Type → Type u_1} [MonadStateOf Lake.Log m] : m Lake.Log

Removes the section monad's log starting and returns it.

Equations

• Lake.takeLog = modifyGet fun (log : Lake.Log) => (log, ∅)

@[inline]

def Lake.takeLogFrom {m : Type → Type u_1} [MonadStateOf Lake.Log m] (pos : Lake.Log.Pos) : m Lake.Log

Removes the monad's log starting at pos and returns it. Useful for extracting logged errors after catching an error position from an ELogT (e.g., LogIO).

Equations

• Lake.takeLogFrom pos = modifyGet fun (log : Lake.Log) => (log.takeFrom pos, log.dropFrom pos)

@[inline]

def Lake.dropLogFrom {m : Type → Type u_1} [MonadStateOf Lake.Log m] (pos : Lake.Log.Pos) : m PUnit

Backtracks the monad's log to pos. Useful for discarding logged errors after catching an error position from an ELogT (e.g., LogIO).

@[inline]

def Lake.extractLog {m : Type → Type u_1} [Monad m] [MonadStateOf Lake.Log m] (x : m PUnit) : m Lake.Log

Returns the log from x while leaving it intact in the monad.

Equations

• Lake.extractLog x = do let iniPos ← Lake.getLogPos x let log ← Lake.getLog pure (log.takeFrom iniPos)

@[inline]

def Lake.withExtractLog {m : Type → Type u_1} {α : Type} [Monad m] [MonadStateOf Lake.Log m] (x : m α) : m (α × Lake.Log)

Returns the log from x and its result while leaving it intact in the monad.

@[inline]

def Lake.withLogErrorPos {m : Type → Type u_1} {α : Type} [Monad m] [MonadStateOf Lake.Log m] [MonadExceptOf Lake.Log.Pos m] (self : m α) : m α

Performs x and backtracks any error to the log position before x.

Equations

• Lake.withLogErrorPos self = do let iniPos ← Lake.getLogPos tryCatch self fun (x : Lake.Log.Pos) => throw iniPos

@[inline]

def Lake.errorWithLog {m : Type → Type u_1} {β : Type} [Monad m] [MonadStateOf Lake.Log m] [MonadExceptOf Lake.Log.Pos m] (self : m PUnit) : m β

Performs x and groups all logs generated into an error block.

@[inline]

def Lake.withLoggedIO {m : Type → Type u_1} {α : Type} [Monad m] [MonadLiftT BaseIO m] [Lake.MonadLog m] [MonadFinally m] (x : m α) : m α

Captures IO in x into an informational log entry.

@[inline]

def Lake.ELog.error {m : Type → Type u_1} {α : Type} [Monad m] [Lake.MonadLog m] [MonadStateOf Lake.Log m] [MonadExceptOf Lake.Log.Pos m] (msg : String) : m α

Throw with the logged error message.

Equations

• Lake.ELog.error msg = Lake.errorWithLog (Lake.logError msg)

@[reducible, inline]

abbrev Lake.ELog.monadError {m : Type → Type u_1} [Monad m] [Lake.MonadLog m] [MonadStateOf Lake.Log m] [MonadExceptOf Lake.Log.Pos m] : Lake.MonadError m

MonadError instance for monads with Log state and Log.Pos errors.

Equations

• Lake.ELog.monadError = { error := fun {α : Type} => Lake.ELog.error }

@[inline]

def Lake.ELog.failure {m : Type → Type u_1} {α : Type} [Monad m] [MonadStateOf Lake.Log m] [MonadExceptOf Lake.Log.Pos m] : m α

Fail without logging anything.

@[inline]

def Lake.ELog.orElse {m : Type → Type u_1} {α : Type} [Monad m] [MonadStateOf Lake.Log m] [MonadExceptOf Lake.Log.Pos m] (x : m α) (y : Unit → m α) : m α

Performs x. If it fails, drop its log and perform y.

Equations

• Lake.ELog.orElse x y = tryCatch x fun (errPos : Lake.Log.Pos) => do Lake.dropLogFrom errPos y ()

@[reducible, inline]

abbrev Lake.ELog.alternative {m : Type → Type u_1} [Monad m] [MonadStateOf Lake.Log m] [MonadExceptOf Lake.Log.Pos m] : Alternative m

Alternative instance for monads with Log state and Log.Pos errors.

Equations

• Lake.ELog.alternative = Alternative.mk (fun {α : Type} => Lake.ELog.failure) fun {α : Type} => Lake.ELog.orElse

@[reducible, inline]

abbrev Lake.LogT (m : Type → Type) (α : Type) : Type

A monad equipped with a log.

Equations

• Lake.LogT m = StateT Lake.Log m

instance Lake.instMonadLogLogTOfMonad {m : Type → Type} [Monad m] : Lake.MonadLog (Lake.LogT m)

Equations

• Lake.instMonadLogLogTOfMonad = Lake.MonadLog.ofMonadState

@[reducible, inline]

abbrev Lake.LogT.run {m : Type → Type} {α : Type} [Functor m] (self : Lake.LogT m α) (log : Lake.Log := ∅) : m (α × Lake.Log)

@[reducible, inline]

abbrev Lake.LogT.run' {m : Type → Type} {α : Type} [Functor m] (self : Lake.LogT m α) (log : Lake.Log := ∅) : m α

@[inline]

def Lake.LogT.takeAndRun {n : Type → Type u_1} {m : Type → Type} {α : Type} [Monad n] [MonadStateOf Lake.Log n] [MonadLiftT m n] [MonadFinally n] (self : Lake.LogT m α) : n α

Run self with the log taken from the state of the monad n.

Warning: If lifting self from m to n fails, the log will be lost. Thus, this is best used when the lift cannot fail.

@[inline]

def Lake.LogT.replayLog {n : Type → Type u_1} {m : Type → Type} {α : Type} [Monad n] [logger : Lake.MonadLog n] [MonadLiftT m n] (self : Lake.LogT m α) : n α

Runs self in n and then replays the entries of the resulting log using the new monad's logger.

Equations

• self.replayLog = do let __discr ← liftM (self ∅) match __discr with | (a, log) => do log.replay pure a

@[reducible, inline]

abbrev Lake.ELogT (m : Type → Type) (α : Type) : Type

A monad equipped with a log and the ability to error at some log position.

Equations

• Lake.ELogT m = Lake.EStateT Lake.Log.Pos Lake.Log m

@[reducible, inline]

abbrev Lake.ELogResult (α : Type u_1) : Type u_1

Equations

• Lake.ELogResult α = Lake.EResult Lake.Log.Pos Lake.Log α

instance Lake.instMonadLogELogTOfMonad {m : Type → Type} [Monad m] : Lake.MonadLog (Lake.ELogT m)

instance Lake.instMonadErrorELogTOfMonad {m : Type → Type} [Monad m] : Lake.MonadError (Lake.ELogT m)

Equations

• Lake.instMonadErrorELogTOfMonad = Lake.ELog.monadError

instance Lake.instAlternativeELogTOfMonad {m : Type → Type} [Monad m] : Alternative (Lake.ELogT m)

@[reducible, inline]

abbrev Lake.ELogT.run {m : Type → Type} {α : Type} (self : Lake.ELogT m α) (log : Lake.Log := ∅) : m (Lake.ELogResult α)

Equations

• self.run log = Lake.EStateT.run log self

@[reducible, inline]

abbrev Lake.ELogT.run' {m : Type → Type} {α : Type} [Functor m] (self : Lake.ELogT m α) (log : Lake.Log := ∅) : m (Except Lake.Log.Pos α)

@[reducible, inline]

abbrev Lake.ELogT.toLogT {m : Type → Type} {α : Type} [Functor m] (self : Lake.ELogT m α) : Lake.LogT m (Except Lake.Log.Pos α)

@[reducible, inline]

abbrev Lake.ELogT.toLogT? {m : Type → Type} {α : Type} [Functor m] (self : Lake.ELogT m α) : Lake.LogT m (Option α)

@[reducible, inline]

abbrev Lake.ELogT.run? {m : Type → Type} {α : Type} [Functor m] (self : Lake.ELogT m α) (log : Lake.Log := ∅) : m (Option α × Lake.Log)

@[reducible, inline]

abbrev Lake.ELogT.run?' {m : Type → Type} {α : Type} [Functor m] (self : Lake.ELogT m α) (log : Lake.Log := ∅) : m (Option α)

Equations

• self.run?' log = Lake.EStateT.run?' log self

@[inline]

def Lake.ELogT.catchLog {m : Type → Type} {α : Type} [Monad m] (f : Lake.Log → Lake.LogT m α) (self : Lake.ELogT m α) : Lake.LogT m α

@[reducible, inline, deprecated Lake.ELogT.run?]

abbrev Lake.ELogT.captureLog {m : Type → Type} {α : Type} [Functor m] (self : Lake.ELogT m α) (log : Lake.Log := ∅) : m (Option α × Lake.Log)

Equations

• @Lake.ELogT.captureLog = @Lake.ELogT.run?

@[inline]

def Lake.ELogT.takeAndRun {n : Type → Type u_1} {m : Type → Type} {α : Type} [Monad n] [MonadStateOf Lake.Log n] [MonadExceptOf Lake.Log.Pos n] [MonadLiftT m n] (self : Lake.ELogT m α) : n α

Run self with the log taken from the state of the monad n,

Warning: If lifting self from m to n fails, the log will be lost. Thus, this is best used when the lift cannot fail. This excludes the native log position failure of ELogT, which are lifted safely.

Equations

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

@[inline]

def Lake.ELogT.replayLog? {n : Type → Type u_1} {m : Type → Type} {α : Type} [Monad n] [logger : Lake.MonadLog n] [MonadLiftT m n] (self : Lake.ELogT m α) : n (Option α)

Runs self in n and then replays the entries of the resulting log using the new monad's logger. Translates an exception in this monad to a none result.

Equations

• self.replayLog? = do let __do_lift ← liftM (self ∅) match __do_lift with | Lake.EResult.ok a log => log.replay *> pure (some a) | Lake.EResult.error a log => log.replay *> pure none

@[inline]

def Lake.ELogT.replayLog {n : Type → Type u_1} {m : Type → Type} {α : Type} [Alternative n] [Monad n] [logger : Lake.MonadLog n] [MonadLiftT m n] (self : Lake.ELogT m α) : n α

Runs self in n and then replays the entries of the resulting log using the new monad's logger. Translates an exception in this monad to a failure in the new monad.

Equations

• self.replayLog = do let __do_lift ← liftM (self ∅) match __do_lift with | Lake.EResult.ok a log => log.replay *> pure a | Lake.EResult.error a log => log.replay *> failure

@[reducible, inline]

abbrev Lake.LogIO (α : Type) : Type

A monad equipped with a log, a log error position, and the ability to perform I/O.

Equations

• Lake.LogIO = Lake.ELogT BaseIO

instance Lake.instMonadLiftIOLogIO : MonadLift IO Lake.LogIO

@[inline]

def Lake.LogIO.toBaseIO {α : Type} (self : Lake.LogIO α) (minLv : Lake.LogLevel := Lake.LogLevel.info) (ansiMode : Lake.AnsiMode := Lake.AnsiMode.auto) (out : Lake.OutStream := Lake.OutStream.stderr) : BaseIO (Option α)

Runs a LogIO action in BaseIO. Prints log entries of at least minLv to out.

def Lake.LogIO.toBaseIO.replay (log : Lake.Log) (logger : Lake.MonadLog BaseIO) : BaseIO Unit

Equations

• Lake.LogIO.toBaseIO.replay log logger = log.replay

@[reducible, inline]

abbrev Lake.LogIO.captureLog {m : Type → Type} {α : Type} [Functor m] (self : Lake.ELogT m α) (log : Lake.Log := ∅) : m (Option α × Lake.Log)

Equations

• @Lake.LogIO.captureLog = @Lake.ELogT.run?

@[reducible, inline]

abbrev Lake.LoggerIO (α : Type) : Type

A monad equipped with a log function and the ability to perform I/O. Unlike LogIO, log entries are not retained by the monad but instead eagerly passed to the log function.

Equations

• Lake.LoggerIO = Lake.MonadLogT BaseIO (EIO PUnit)

instance Lake.instMonadErrorLoggerIO : Lake.MonadError Lake.LoggerIO

instance Lake.instMonadLiftIOLoggerIO : MonadLift IO Lake.LoggerIO

Equations

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

instance Lake.instMonadLiftLogIOLoggerIO : MonadLift Lake.LogIO Lake.LoggerIO

Equations

• Lake.instMonadLiftLogIOLoggerIO = { monadLift := fun {α : Type} => Lake.ELogT.replayLog }

@[inline]

def Lake.LoggerIO.toBaseIO {α : Type} (self : Lake.LoggerIO α) (minLv : Lake.LogLevel := Lake.LogLevel.info) (ansiMode : Lake.AnsiMode := Lake.AnsiMode.auto) (out : Lake.OutStream := Lake.OutStream.stderr) : BaseIO (Option α)

Runs a LoggerIO action in BaseIO. Prints log entries of at least minLv to out.

Equations

• self.toBaseIO minLv ansiMode out = do let __do_lift ← out.getLogger minLv ansiMode (fun (x : Except PUnit α) => x.toOption) <$> (ReaderT.run self __do_lift).toBaseIO

def Lake.LoggerIO.captureLog {α : Type} (self : Lake.LoggerIO α) : BaseIO (Option α × Lake.Log)

Equations

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

@[reducible, inline]

abbrev Lake.LoggerIO.run? {α : Type} (self : Lake.LoggerIO α) : BaseIO (Option α × Lake.Log)

Equations

• @Lake.LoggerIO.run? = @Lake.LoggerIO.captureLog

@[inline]

def Lake.LoggerIO.run?' {α : Type} (self : Lake.LoggerIO α) (logger : Lake.LogEntry → BaseIO PUnit := fun (x : Lake.LogEntry) => pure ()) : BaseIO (Option α)