inductive Lake.Verbosity : Type

• quiet : Verbosity
• normal : Verbosity
• verbose : Verbosity

instance Lake.instReprVerbosity : Repr Verbosity

instance Lake.instDecidableEqVerbosity : DecidableEq Verbosity

instance Lake.instOrdVerbosity : Ord Verbosity

instance Lake.instLTVerbosity : LT Verbosity

instance Lake.instLEVerbosity : LE Verbosity

instance Lake.instMinVerbosity : Min Verbosity

instance Lake.instMaxVerbosity : Max Verbosity

instance Lake.instInhabitedVerbosity : Inhabited Verbosity

inductive Lake.AnsiMode : Type

Whether to ANSI escape codes.

• auto : AnsiMode

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

• ansi : AnsiMode

  Use ANSI escape codes.

• noAnsi : AnsiMode

  Do not use ANSI escape codes.

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

Returns whether to ANSI escape codes with the stream out.

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.

inductive Lake.OutStream : Type

A pure representation of output stream.

• stdout : OutStream
• stderr : OutStream
• stream (s : IO.FS.Stream) : OutStream

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

Returns the real output stream associated with OutStream.

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

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

inductive Lake.LogLevel : Type

• trace : LogLevel
• info : LogLevel
• warning : LogLevel
• error : LogLevel

instance Lake.instInhabitedLogLevel : Inhabited LogLevel

instance Lake.instReprLogLevel : Repr LogLevel

instance Lake.instDecidableEqLogLevel : DecidableEq LogLevel

instance Lake.instOrdLogLevel : Ord LogLevel

instance Lake.instToJsonLogLevel : Lean.ToJson LogLevel

instance Lake.instFromJsonLogLevel : Lean.FromJson LogLevel

instance Lake.instLTLogLevel : LT LogLevel

instance Lake.instLELogLevel : LE LogLevel

instance Lake.instMinLogLevel : Min LogLevel

instance Lake.instMaxLogLevel : Max LogLevel

def Lake.LogLevel.icon : LogLevel → Char

Unicode icon for representing the log level.

def Lake.LogLevel.ansiColor : LogLevel → String

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

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

def Lake.LogLevel.toString : LogLevel → String

instance Lake.instToStringLogLevel : ToString LogLevel

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

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

def Lake.Verbosity.minLogLv : Verbosity → LogLevel

structure Lake.LogEntry : Type

• level : LogLevel
• message : String

instance Lake.instInhabitedLogEntry : Inhabited LogEntry

instance Lake.instToJsonLogEntry : Lean.ToJson LogEntry

instance Lake.instFromJsonLogEntry : Lean.FromJson LogEntry

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

instance Lake.instToStringLogEntry : ToString LogEntry

@[inline]

def Lake.LogEntry.trace (message : String) : LogEntry

@[inline]

def Lake.LogEntry.info (message : String) : LogEntry

@[inline]

def Lake.LogEntry.warning (message : String) : LogEntry

@[inline]

def Lake.LogEntry.error (message : String) : LogEntry

def Lake.LogEntry.ofSerialMessage (msg : Lean.SerialMessage) : LogEntry

def Lake.LogEntry.ofMessage (msg : Lean.Message) : BaseIO LogEntry

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

• logEntry (e : LogEntry) : m PUnit

@[inline]

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

@[inline]

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

@[inline]

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

@[inline]

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

@[inline]

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

@[inline]

def Lake.logMessage {m : Type → Type u_1} (msg : Lean.Message) [Monad m] [MonadLog m] [MonadLiftT BaseIO m] : m PUnit

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

@[reducible, inline]

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

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

@[reducible, inline]

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

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

@[reducible, inline]

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

@[inline]

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

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

@[reducible, inline]

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

@[reducible, inline]

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

@[reducible, inline]

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

@[inline]

def Lake.OutStream.getLogger {m : Type → Type} [MonadLiftT BaseIO m] (out : OutStream) (minLv : LogLevel := LogLevel.info) (ansiMode : AnsiMode := AnsiMode.auto) : BaseIO (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 (MonadLogT m n α)

instance Lake.MonadLogT.instMonadLogOfMonadOfMonadLiftT {n : Type u_1 → Type u_2} {m : Type u_1 → Type u_1} [Monad n] [MonadLiftT m n] : MonadLog (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 : MonadLog m → MonadLog m') (self : MonadLogT m' n α) : MonadLogT m n α

@[inline]

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

structure Lake.Log : Type

• entries : Array LogEntry

instance Lake.instInhabitedLog : Inhabited Log

instance Lake.instToJsonLog : Lean.ToJson Log

instance Lake.instFromJsonLog : Lean.FromJson 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 Pos

instance Lake.Log.instDecidableEqPos : DecidableEq Pos

instance Lake.instOfNatPos : OfNat Log.Pos 0

instance Lake.instOrdPos : Ord Log.Pos

instance Lake.instLTPos : LT Log.Pos

instance Lake.instDecidableRelPosLt : DecidableRel LT.lt

instance Lake.instLEPos : LE Log.Pos

instance Lake.instDecidableRelPosLe : DecidableRel LE.le

instance Lake.instMinPos : Min Log.Pos

instance Lake.instMaxPos : Max Log.Pos

@[inline]

def Lake.Log.empty : Log

instance Lake.Log.instEmptyCollection : EmptyCollection Log

@[inline]

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

@[inline]

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

@[inline]

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

@[inline]

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

@[inline]

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

@[inline]

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

instance Lake.Log.instAppend : Append Log

@[inline]

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

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

@[inline]

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

Removes log entries after pos (inclusive).

@[inline]

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

Takes log entries before pos (exclusive).

@[inline]

def Lake.Log.split (log : Log) (pos : Pos) : Log × 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.

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

instance Lake.Log.instToString : ToString Log

@[inline]

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

@[inline]

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

@[inline]

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

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

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

@[inline]

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

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

@[reducible, inline]

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

@[inline]

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

Returns the monad's log.

@[inline]

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

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

@[inline]

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

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

@[inline]

def Lake.takeLogFrom {m : Type → Type u_1} [MonadStateOf Log m] (pos : Log.Pos) : m 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).

@[inline]

def Lake.dropLogFrom {m : Type → Type u_1} [MonadStateOf Log m] (pos : 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 Log m] (x : m PUnit) : m Log

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

@[inline]

def Lake.withExtractLog {m : Type → Type u_1} {α : Type} [Monad m] [MonadStateOf Log m] (x : m α) : m (α × 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 Log m] [MonadExceptOf Log.Pos m] (self : m α) : m α

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

@[inline]

def Lake.errorWithLog {m : Type → Type u_1} {β : Type} [Monad m] [MonadStateOf Log m] [MonadExceptOf 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] [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] [MonadLog m] [MonadStateOf Log m] [MonadExceptOf Log.Pos m] (msg : String) : m α

Throw with the logged error message.

@[reducible, inline]

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

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

@[inline]

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

Fail without logging anything.

@[inline]

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

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

@[reducible, inline]

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

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

@[reducible, inline]

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

A monad equipped with a log.

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

@[reducible, inline]

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

@[reducible, inline]

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

@[inline]

def Lake.LogT.takeAndRun {n : Type → Type u_1} {m : Type → Type} {α : Type} [Monad n] [MonadStateOf Log n] [MonadLiftT m n] [MonadFinally n] (self : 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 : MonadLog n] [MonadLiftT m n] (self : LogT m α) : n α

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

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

@[reducible, inline]

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

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

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

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

@[reducible, inline]

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

@[reducible, inline]

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

@[reducible, inline]

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

@[reducible, inline]

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

@[reducible, inline]

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

@[reducible, inline]

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

@[inline]

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

@[inline]

def Lake.ELogT.takeAndRun {n : Type → Type u_1} {m : Type → Type} {α : Type} [Monad n] [MonadStateOf Log n] [MonadExceptOf Log.Pos n] [MonadLiftT m n] (self : 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.

@[inline]

def Lake.ELogT.replayLog? {n : Type → Type u_1} {m : Type → Type} {α : Type} [Monad n] [logger : MonadLog n] [MonadLiftT m n] (self : 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.

@[inline]

def Lake.ELogT.replayLog {n : Type → Type u_1} {m : Type → Type} {α : Type} [Alternative n] [Monad n] [logger : MonadLog n] [MonadLiftT m n] (self : 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.

@[reducible, inline]

abbrev Lake.LogIO (α : Type) : Type

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

instance Lake.instMonadLiftIOLogIO : MonadLift IO LogIO

@[inline]

def Lake.LogIO.toBaseIO {α : Type} (self : LogIO α) (minLv : LogLevel := LogLevel.info) (ansiMode : AnsiMode := AnsiMode.auto) (out : OutStream := 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 : Log) (logger : MonadLog BaseIO) : BaseIO Unit

@[reducible, inline]

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

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

instance Lake.instMonadErrorLoggerIO : MonadError LoggerIO

instance Lake.instMonadLiftIOLoggerIO : MonadLift IO LoggerIO

instance Lake.instMonadLiftLogIOLoggerIO : MonadLift LogIO LoggerIO

@[inline]

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

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

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

@[reducible, inline]

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

@[inline]

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