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

Equations

• Lake.instOrdVerbosity = { compare := Lake.ordVerbosity✝ }

instance Lake.instLTVerbosity : LT Lake.Verbosity

Equations

• Lake.instLTVerbosity = ltOfOrd

instance Lake.instLEVerbosity : LE Lake.Verbosity

Equations

• Lake.instLEVerbosity = leOfOrd

instance Lake.instMinVerbosity : Min Lake.Verbosity

Equations

• Lake.instMinVerbosity = minOfLe

instance Lake.instMaxVerbosity : Max Lake.Verbosity

Equations

• Lake.instMaxVerbosity = maxOfLe

instance Lake.instInhabitedVerbosity : Inhabited Lake.Verbosity

Equations

• Lake.instInhabitedVerbosity = { default := Lake.Verbosity.normal }

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 (s : 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

Equations

• Lake.instCoeStreamOutStream = { coe := Lake.OutStream.stream }

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

Equations

• Lake.instInhabitedLogLevel = { default := Lake.LogLevel.trace }

instance Lake.instReprLogLevel : Repr Lake.LogLevel

Equations

• Lake.instReprLogLevel = { reprPrec := Lake.reprLogLevel✝ }

instance Lake.instDecidableEqLogLevel : DecidableEq Lake.LogLevel

Equations

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

instance Lake.instOrdLogLevel : Ord Lake.LogLevel

Equations

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

instance Lake.instToJsonLogLevel : Lean.ToJson Lake.LogLevel

Equations

• Lake.instToJsonLogLevel = { toJson := Lake.toJsonLogLevel✝ }

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.

Equations

• Lake.LogLevel.trace.ansiColor = "34"
• Lake.LogLevel.info.ansiColor = "34"
• Lake.LogLevel.warning.ansiColor = "33"
• Lake.LogLevel.error.ansiColor = "31"

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

Equations

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

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

Equations

• Lake.LogLevel.trace.toString = "trace"
• Lake.LogLevel.info.toString = "info"
• Lake.LogLevel.warning.toString = "warning"
• Lake.LogLevel.error.toString = "error"

instance Lake.instToStringLogLevel : ToString Lake.LogLevel

Equations

• Lake.instToStringLogLevel = { toString := Lake.LogLevel.toString }

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

Equations

• Lake.LogLevel.ofMessageSeverity Lean.MessageSeverity.information = Lake.LogLevel.info
• Lake.LogLevel.ofMessageSeverity Lean.MessageSeverity.warning = Lake.LogLevel.warning
• Lake.LogLevel.ofMessageSeverity Lean.MessageSeverity.error = Lake.LogLevel.error

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

Equations

• Lake.Verbosity.quiet.minLogLv = Lake.LogLevel.warning
• Lake.Verbosity.normal.minLogLv = Lake.LogLevel.info
• Lake.Verbosity.verbose.minLogLv = Lake.LogLevel.trace

structure Lake.LogEntry : Type

• level : Lake.LogLevel
• message : String

instance Lake.instInhabitedLogEntry : Inhabited Lake.LogEntry

Equations

• Lake.instInhabitedLogEntry = { default := { level := default, message := default } }

instance Lake.instToJsonLogEntry : Lean.ToJson Lake.LogEntry

Equations

• Lake.instToJsonLogEntry = { toJson := Lake.toJsonLogEntry✝ }

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

Equations

• Lake.instToStringLogEntry = { toString := fun (self : Lake.LogEntry) => self.toString }

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

• logEntry (e : 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

Equations

• Lake.logWarning message = Lake.logEntry { level := Lake.LogLevel.warning, message := message }

@[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 "No deprecation message available." (since := "2024-05-18")]

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

Equations

• self.lift = { logEntry := fun (e : Lake.LogEntry) => liftM (Lake.logEntry e) }

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

Equations

• Lake.MonadLog.instOfMonadLift = methods.lift

@[reducible, inline, deprecated "Deprecated without replacement." (since := "2024-05-18")]

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

Equations

• Lake.MonadLog.io minLv = { logEntry := fun (e : Lake.LogEntry) => liftM (Lake.logToIO e minLv) }

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

Equations

• Lake.MonadLog.error msg = Lake.logError msg *> failure

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

Equations

• self.logEntry e minLv ansiMode = do let out ← self.get let useAnsi ← Lake.AnsiMode.isEnabled out ansiMode Lake.logToStream e out minLv useAnsi

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

Equations

• out.getLogger minLv ansiMode = do let out ← out.get let useAnsi ← Lake.AnsiMode.isEnabled out ansiMode pure (Lake.MonadLog.stream out minLv useAnsi)

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

• Lake.MonadLogT m n = ReaderT (Lake.MonadLog m) n

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)

Equations

• Lake.MonadLogT.instMonadLogOfMonadOfMonadLiftT = { logEntry := fun (e : Lake.LogEntry) => do let __do_lift ← read liftM (Lake.logEntry e) }

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

Equations

• self.ignoreLog = self Lake.MonadLog.nop

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

Equations

• Lake.instFromJsonLog = { fromJson? := fun (x : Lean.Json) => Lake.Log.mk <$> Lean.fromJson? x }

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.Log.instDecidableEqPos : DecidableEq Lake.Log.Pos

Equations

• Lake.Log.instDecidableEqPos = Lake.Log.decEqPos✝

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

Equations

• Lake.instOfNatPos = { ofNat := { val := 0 } }

instance Lake.instOrdPos : Ord Lake.Log.Pos

Equations

• Lake.instOrdPos = { compare := fun (x1 x2 : Lake.Log.Pos) => compare x1.val x2.val }

instance Lake.instLTPos : LT Lake.Log.Pos

Equations

• Lake.instLTPos = { lt := fun (x1 x2 : Lake.Log.Pos) => x1.val < x2.val }

instance Lake.instDecidableRelPosLt : DecidableRel LT.lt

Equations

• Lake.instDecidableRelPosLt = inferInstanceAs (DecidableRel fun (x1 x2 : Lake.Log.Pos) => x1.val < x2.val)

instance Lake.instLEPos : LE Lake.Log.Pos

Equations

• Lake.instLEPos = { le := fun (x1 x2 : Lake.Log.Pos) => x1.val ≤ x2.val }

instance Lake.instDecidableRelPosLe : DecidableRel LE.le

Equations

• Lake.instDecidableRelPosLe = inferInstanceAs (DecidableRel fun (x1 x2 : Lake.Log.Pos) => x1.val ≤ x2.val)

instance Lake.instMinPos : Min Lake.Log.Pos

Equations

• Lake.instMinPos = minOfLe

instance Lake.instMaxPos : Max Lake.Log.Pos

Equations

• Lake.instMaxPos = maxOfLe

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

Equations

• log.isEmpty = decide (log.size = 0)

@[inline]

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

Equations

• log.hasEntries = decide (log.size ≠ 0)

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

Equations

• log.append o = { entries := log.entries.append o.entries }

instance Lake.Log.instAppend : Append Lake.Log

Equations

• Lake.Log.instAppend = { append := Lake.Log.append }

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

Equations

• log.dropFrom pos = { entries := log.entries.take pos.val }

@[inline]

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

Takes log entries before pos (exclusive).

Equations

• log.takeFrom pos = log.extract pos log.endPos

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

Equations

• log.toString = Array.foldl (fun (x1 : String) (x2 : Lake.LogEntry) => x1 ++ x2.toString ++ "\n") "" log.entries

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

Equations

• Lake.Log.filter f log = { entries := Array.filter f log.entries }

@[inline]

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

Equations

• Lake.Log.any f log = log.entries.any f

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).

Equations

• Lake.dropLogFrom pos = modify fun (x : Lake.Log) => x.dropFrom pos

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

• Lake.ELog.failure = do let __do_lift ← Lake.getLogPos throw __do_lift

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

Equations

• self.run log = StateT.run self log

@[reducible, inline]

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

Equations

• self.run' log = StateT.run' self log

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

Equations

• self.takeAndRun = do let __do_lift ← Lake.takeLog let __discr ← liftM (self __do_lift) match __discr with | (a, log) => do set log pure a

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

Equations

• Lake.instMonadLogELogTOfMonad = Lake.MonadLog.ofMonadState

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)

Equations

• Lake.instAlternativeELogTOfMonad = Lake.ELog.alternative

@[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 α)

Equations

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

@[reducible, inline]

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

Equations

• self.toLogT = Lake.EStateT.toStateT self

@[reducible, inline]

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

Equations

• self.toLogT? = Lake.EStateT.toStateT? self

@[reducible, inline]

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

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 (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 α

Equations

• Lake.ELogT.catchLog f self = Lake.EStateT.catchExceptions self fun (errPos : Lake.Log.Pos) => do let __do_lift ← Lake.takeLogFrom errPos f __do_lift

@[reducible, inline, deprecated Lake.ELogT.run? (since := "2024-05-18")]

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

Equations

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

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

Equations

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

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

Equations

• Lake.instMonadErrorLoggerIO = { error := fun {α : Type} => Lake.MonadLog.error }

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 α)

Equations

• self.run?' logger = (fun (x : Except PUnit α) => x.toOption) <$> (ReaderT.run self { logEntry := logger }).toBaseIO