Documentation

Lake.Util.Log

inductive Lake.AnsiMode :

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.Ansi.chalk (colorCode text : 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
inductive Lake.OutStream :

A pure representation of output stream.

Instances For

Unicode icon for representing the log level.

Equations
Equations
  • One or more equations did not get rendered due to their size.
Equations
def Lake.LogEntry.toString (self : LogEntry) (useAnsi : Bool := false) :
Equations
  • One or more equations did not get rendered due to their size.
@[inline]
Equations
@[inline]
Equations
@[inline]
Equations
@[inline]
Equations
@[inline]
def Lake.logVerbose {m : Type u_1 → Type u_2} [Monad m] [MonadLog m] (message : String) :
Equations
@[inline]
def Lake.logInfo {m : Type u_1 → Type u_2} [Monad m] [MonadLog m] (message : String) :
Equations
@[inline]
def Lake.logWarning {m : Type u_1 → Type u_2} [MonadLog m] (message : String) :
Equations
@[inline]
def Lake.logError {m : Type u_1 → Type u_2} [MonadLog m] (message : String) :
Equations
@[specialize #[]]
def Lake.logSerialMessage {m : Type u_1 → Type u_2} (msg : Lean.SerialMessage) [MonadLog m] :
Equations
  • One or more equations did not get rendered due to their size.
@[deprecated "No deprecation message available." (since := "2024-05-18")]
Equations
  • One or more equations did not get rendered due to their size.
def Lake.logToStream (e : LogEntry) (out : IO.FS.Stream) (minLv : LogLevel) (useAnsi : Bool) :
Equations
@[reducible, inline]
abbrev Lake.MonadLog.nop {m : TypeType u_1} [Pure m] :
Equations
@[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) :
Equations
instance Lake.MonadLog.instOfMonadLift {m : Type u_1 → Type u_2} {n : Type u_1 → Type u_3} [MonadLift m n] [methods : MonadLog m] :
Equations
@[reducible, inline, deprecated "Deprecated without replacement." (since := "2024-05-18")]
abbrev Lake.MonadLog.io {m : TypeType u_1} [MonadLiftT BaseIO m] (minLv : LogLevel := LogLevel.info) :
Equations
@[reducible, inline]
abbrev Lake.MonadLog.stream {m : TypeType u_1} [MonadLiftT BaseIO m] (out : IO.FS.Stream) (minLv : LogLevel := LogLevel.info) (useAnsi : Bool := false) :
Equations
@[inline]
def Lake.MonadLog.error {m : Type u_1 → Type u_2} {α : Type u_1} [Alternative m] [MonadLog m] (msg : String) :
m α
Equations
Equations
@[reducible, inline]
abbrev Lake.OutStream.logger {m : TypeType u_1} [MonadLiftT BaseIO m] (out : OutStream) (minLv : LogLevel := LogLevel.info) (ansiMode : AnsiMode := AnsiMode.auto) :
Equations
@[reducible, inline]
abbrev Lake.MonadLog.stdout {m : TypeType u_1} [MonadLiftT BaseIO m] (minLv : LogLevel := LogLevel.info) (ansiMode : AnsiMode := AnsiMode.auto) :
Equations
@[reducible, inline]
abbrev Lake.MonadLog.stderr {m : TypeType u_1} [MonadLiftT BaseIO m] (minLv : LogLevel := LogLevel.info) (ansiMode : AnsiMode := AnsiMode.auto) :
Equations
@[inline]
Equations
@[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

Equations
Instances For
instance Lake.MonadLogT.instInhabitedOfPure {n : Type u_1 → Type u_2} {α : Type u_1} {m : Type u_3 → Type u_1} [Pure n] [Inhabited α] :
Equations
instance Lake.MonadLogT.instMonadLogOfMonadOfMonadLiftT {n : Type u_1 → Type u_2} {m : Type u_1 → Type u_1} [Monad n] [MonadLiftT m n] :
Equations
@[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 mMonadLog m') (self : MonadLogT m' n α) :
MonadLogT m n α
Equations
@[inline]
def Lake.MonadLogT.ignoreLog {m : TypeType u_1} {n : Type u_1 → Type u_2} {α : Type u_1} [Pure m] (self : MonadLogT m n α) :
n α
Equations
Equations
structure Lake.Log.Pos :

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

Instances For
Equations
Equations
Equations
Equations
@[inline]
Equations
@[inline]
def Lake.Log.size (log : Log) :
Equations
@[inline]
Equations
@[inline]
Equations
@[inline]
def Lake.Log.endPos (log : Log) :
Equations
@[inline]
def Lake.Log.push (log : Log) (e : LogEntry) :
Equations
@[inline]
def Lake.Log.append (log o : Log) :
Equations
@[inline]
def Lake.Log.extract (log : Log) (start stop : Pos) :

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

Equations
@[inline]
def Lake.Log.dropFrom (log : Log) (pos : Pos) :

Removes log entries after pos (inclusive).

Equations
@[inline]
def Lake.Log.takeFrom (log : Log) (pos : Pos) :

Takes log entries before pos (exclusive).

Equations
@[inline]
def Lake.Log.split (log : Log) (pos : Pos) :

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
Equations
@[inline]
def Lake.Log.replay {m : Type u_1 → Type u_2} [Monad m] [logger : MonadLog m] (log : Log) :
Equations
@[inline]
def Lake.Log.filter (f : LogEntryBool) (log : Log) :
Equations
@[inline]
def Lake.Log.any (f : LogEntryBool) (log : Log) :
Equations

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

Equations
@[inline]
def Lake.pushLogEntry {m : TypeType u_1} [MonadStateOf Log m] (e : LogEntry) :

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

Equations
@[reducible, inline]
Equations
@[inline]
def Lake.getLog {m : TypeType u_1} [MonadStateOf Log m] :
m Log

Returns the monad's log.

Equations
@[inline]
def Lake.getLogPos {m : TypeType u_1} [Functor m] [MonadStateOf Log m] :

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

Equations
@[inline]
def Lake.takeLog {m : TypeType u_1} [MonadStateOf Log m] :
m Log

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

Equations
@[inline]
def Lake.takeLogFrom {m : TypeType 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).

Equations
@[inline]
def Lake.dropLogFrom {m : TypeType u_1} [MonadStateOf Log m] (pos : Log.Pos) :

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

Equations
@[inline]
def Lake.extractLog {m : TypeType u_1} [Monad m] [MonadStateOf Log m] (x : m PUnit) :
m Log

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

Equations
@[inline]
def Lake.withExtractLog {m : TypeType 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.

Equations
@[inline]
def Lake.withLogErrorPos {m : TypeType 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.

Equations
@[inline]
def Lake.errorWithLog {m : TypeType 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.

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

Captures IO in x into an informational log entry.

Equations
  • One or more equations did not get rendered due to their size.
@[inline]
def Lake.ELog.error {m : TypeType u_1} {α : Type} [Monad m] [MonadLog m] [MonadStateOf Log m] [MonadExceptOf Log.Pos m] (msg : String) :
m α

Throw with the logged error message.

Equations
@[reducible, inline]

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

Equations
@[inline]
def Lake.ELog.failure {m : TypeType u_1} {α : Type} [Monad m] [MonadStateOf Log m] [MonadExceptOf Log.Pos m] :
m α

Fail without logging anything.

Equations
@[inline]
def Lake.ELog.orElse {m : TypeType u_1} {α : Type} [Monad m] [MonadStateOf Log m] [MonadExceptOf Log.Pos m] (x : m α) (y : Unitm α) :
m α

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

Equations
@[reducible, inline]

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

Equations
@[reducible, inline]
abbrev Lake.LogT (m : TypeType) (α : Type) :

A monad equipped with a log.

Equations
Instances For
@[reducible, inline]
abbrev Lake.LogT.run {m : TypeType} {α : Type} [Functor m] (self : LogT m α) (log : Log := ) :
m (α × Log)
Equations
@[reducible, inline]
abbrev Lake.LogT.run' {m : TypeType} {α : Type} [Functor m] (self : LogT m α) (log : Log := ) :
m α
Equations
@[inline]
def Lake.LogT.takeAndRun {n : TypeType u_1} {m : TypeType} {α : 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.

Equations
@[inline]
def Lake.LogT.replayLog {n : TypeType u_1} {m : TypeType} {α : 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.

Equations
@[reducible, inline]
abbrev Lake.ELogT (m : TypeType) (α : Type) :

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

Equations
Instances For
@[reducible, inline]
abbrev Lake.ELogResult (α : Type u_1) :
Type u_1
Equations
@[reducible, inline]
abbrev Lake.ELogT.run {m : TypeType} {α : Type} (self : ELogT m α) (log : Log := ) :
m (ELogResult α)
Equations
@[reducible, inline]
abbrev Lake.ELogT.run' {m : TypeType} {α : Type} [Functor m] (self : ELogT m α) (log : Log := ) :
Equations
@[reducible, inline]
abbrev Lake.ELogT.toLogT {m : TypeType} {α : Type} [Functor m] (self : ELogT m α) :
Equations
@[reducible, inline]
abbrev Lake.ELogT.toLogT? {m : TypeType} {α : Type} [Functor m] (self : ELogT m α) :
LogT m (Option α)
Equations
@[reducible, inline]
abbrev Lake.ELogT.run? {m : TypeType} {α : Type} [Functor m] (self : ELogT m α) (log : Log := ) :
m (Option α × Log)
Equations
@[reducible, inline]
abbrev Lake.ELogT.run?' {m : TypeType} {α : Type} [Functor m] (self : ELogT m α) (log : Log := ) :
m (Option α)
Equations
@[inline]
def Lake.ELogT.catchLog {m : TypeType} {α : Type} [Monad m] (f : LogLogT m α) (self : ELogT m α) :
LogT m α
Equations
@[reducible, inline, deprecated Lake.ELogT.run? (since := "2024-05-18")]
abbrev Lake.ELogT.captureLog {m : TypeType} {α : Type} [Functor m] (self : ELogT m α) (log : Log := ) :
m (Option α × Log)
Equations
@[inline]
def Lake.ELogT.takeAndRun {n : TypeType u_1} {m : TypeType} {α : 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.

Equations
  • One or more equations did not get rendered due to their size.
@[inline]
def Lake.ELogT.replayLog? {n : TypeType u_1} {m : TypeType} {α : 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.

Equations
@[inline]
def Lake.ELogT.replayLog {n : TypeType u_1} {m : TypeType} {α : 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.

Equations
@[reducible, inline]
abbrev Lake.LogIO (α : Type) :

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

Equations
Instances For
@[inline]
def Lake.LogIO.toBaseIO {α : Type} (self : LogIO α) (minLv : LogLevel := LogLevel.info) (ansiMode : AnsiMode := AnsiMode.auto) (out : OutStream := OutStream.stderr) :

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

Equations
  • One or more equations did not get rendered due to their size.
@[reducible, inline]
abbrev Lake.LogIO.captureLog {m : TypeType} {α : Type} [Functor m] (self : ELogT m α) (log : Log := ) :
m (Option α × Log)
Equations
@[reducible, inline]
abbrev Lake.LoggerIO (α : 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
Instances For
@[inline]
def Lake.LoggerIO.toBaseIO {α : Type} (self : LoggerIO α) (minLv : LogLevel := LogLevel.info) (ansiMode : AnsiMode := AnsiMode.auto) (out : OutStream := OutStream.stderr) :

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

Equations
Equations
  • One or more equations did not get rendered due to their size.
@[reducible, inline]
abbrev Lake.LoggerIO.run? {α : Type} (self : LoggerIO α) :
Equations
@[inline]
def Lake.LoggerIO.run?' {α : Type} (self : LoggerIO α) (logger : LogEntryBaseIO PUnit := fun (x : LogEntry) => pure ()) :
Equations