Documentation

Lake.Util.Log

inductive Lake.Verbosity :

Instances For

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.LogLevel :

Instances For

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.toString :

Lake.LogLevel → String

Equations

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

Instances For

def Lake.LogLevel.ofMessageSeverity :

Lean.MessageSeverity → Lake.LogLevel

Equations

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

Instances For

instance Lake.instToStringLogLevel :

ToString Lake.LogLevel

Equations

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

def Lake.LogLevel.visibleAtVerbosity (self : Lake.LogLevel) (verbosity : Lake.Verbosity) :

Equations

self.visibleAtVerbosity verbosity = match self with | Lake.LogLevel.trace => verbosity == Lake.Verbosity.verbose | Lake.LogLevel.info => verbosity != Lake.Verbosity.quiet | x => true

Instances For

structure Lake.LogEntry :

level : Lake.LogLevel
message : String

Instances For

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

Equations

self.toString = toString "" ++ toString self.level ++ toString ": " ++ toString self.message.trim ++ toString ""

Instances For

instance Lake.instToStringLogEntry :

ToString Lake.LogEntry

Equations

Lake.instToStringLogEntry = { toString := Lake.LogEntry.toString }

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

logEntry : Lake.LogEntry → m PUnit

Instances

@[inline]

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

Equations

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

Instances For

@[inline]

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

Equations

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

Instances For

@[inline]

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

Equations

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

Instances For

@[inline]

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

Equations

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

Instances For

def Lake.logToIO (e : Lake.LogEntry) (verbosity : Lake.Verbosity) :

Equations

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

Instances For

def Lake.logToStream (e : Lake.LogEntry) (h : IO.FS.Stream) (verbosity : Lake.Verbosity) :

Equations

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

Instances For

@[specialize #[]]

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

Equations

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

Instances For

@[specialize #[]]

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

Lake.MonadLog m

Equations

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

Instances For

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

Inhabited (Lake.MonadLog m)

Equations

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

@[specialize #[]]

def Lake.MonadLog.io {m : Type → Type u_1} [MonadLiftT BaseIO m] (verbosity : optParam Lake.Verbosity Lake.Verbosity.normal) :

Lake.MonadLog m

Equations

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

Instances For

@[inline]

def Lake.MonadLog.stream {m : Type → Type u_1} [MonadLiftT BaseIO m] (h : IO.FS.Stream) (verbosity : optParam Lake.Verbosity Lake.Verbosity.normal) :

Lake.MonadLog m

Equations

Lake.MonadLog.stream h verbosity = { logEntry := fun (e : Lake.LogEntry) => liftM (Lake.logToStream e h verbosity) }

Instances For

@[inline]

def Lake.MonadLog.stdout {m : Type → Type u_1} [MonadLiftT BaseIO m] (verbosity : optParam Lake.Verbosity Lake.Verbosity.normal) :

Lake.MonadLog m

Equations

Lake.MonadLog.stdout verbosity = { logEntry := fun (e : Lake.LogEntry) => liftM do let __do_lift ← IO.getStdout Lake.logToStream e __do_lift verbosity }

Instances For

@[inline]

def Lake.MonadLog.stderr {m : Type → Type u_1} [MonadLiftT BaseIO m] (verbosity : optParam Lake.Verbosity Lake.Verbosity.normal) :

Lake.MonadLog m

Equations

Lake.MonadLog.stderr verbosity = { logEntry := fun (e : Lake.LogEntry) => liftM do let __do_lift ← IO.getStderr Lake.logToStream e __do_lift verbosity }

Instances For

@[inline]

def 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) }

Instances For

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]

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

Type (max v w)

Equations

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

Instances For

instance Lake.instInhabitedMonadLogTOfPure {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.instInhabitedMonadLogTOfPure = { default := fun (x : Lake.MonadLog m) => pure default }

instance Lake.instMonadLogMonadLogTOfMonadOfMonadLiftT {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.instMonadLogMonadLogTOfMonadOfMonadLiftT = { 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

Instances For

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

Instances For

structure Lake.Log :

entries : Array Lake.LogEntry

Instances For

@[inline]

def Lake.Log.empty :

Equations

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

Instances For

instance Lake.Log.instEmptyCollection :

EmptyCollection Lake.Log

Equations

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

@[inline]

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

Equations

log.isEmpty = log.entries.isEmpty

Instances For

@[inline]

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

Equations

log.size = log.entries.size

Instances For

@[inline]

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

Equations

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

Instances For

@[inline]

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

Equations

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

Instances For

instance Lake.Log.instAppend :

Append Lake.Log

Equations

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

@[inline]

def Lake.Log.shrink (log : Lake.Log) (n : Nat) :

Equations

log.shrink n = { entries := log.entries.shrink n }

Instances For

@[inline]

def Lake.Log.split (log : Lake.Log) (n : Nat) :

Lake.Log × Lake.Log

Equations

log.split n = ({ entries := log.entries.extract 0 n }, log.shrink n)

Instances For

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

Equations

log.toString = Array.foldl (fun (x : String) (x_1 : Lake.LogEntry) => x ++ x_1.toString ++ "\n") "" log.entries 0

Instances For

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

Equations

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

Instances For

@[inline]

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

Equations

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

Instances For

def Lake.Log.filterByVerbosity (log : Lake.Log) (verbosity : optParam Lake.Verbosity Lake.Verbosity.normal) :

Equations

log.filterByVerbosity verbosity = Lake.Log.filter (fun (x : Lake.LogEntry) => x.level.visibleAtVerbosity verbosity) log

Instances For

@[inline]

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

Equations

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

Instances For

def Lake.Log.hasVisibleEntries (log : Lake.Log) (verbosity : optParam Lake.Verbosity Lake.Verbosity.normal) :

Equations

log.hasVisibleEntries verbosity = Lake.Log.any (fun (x : Lake.LogEntry) => x.level.visibleAtVerbosity verbosity) log

Instances For

class Lake.MonadGetLog (m : Type → Type v) :

getLog : m Lake.Log

Instances

@[inline]

def Lake.MonadGetLog.getLogSize {m : Type → Type u_1} [Functor m] [Lake.MonadGetLog m] :

Equations

Lake.getLogSize = (fun (x : Lake.Log) => x.size) <$> Lake.getLog

Instances For

instance Lake.instMonadGetLogOfMonadLift {m : Type → Type u_1} {n : Type → Type u_2} [MonadLift m n] [Lake.MonadGetLog m] :

Lake.MonadGetLog n

Equations

Lake.instMonadGetLogOfMonadLift = { getLog := liftM Lake.getLog }

@[reducible, inline]

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

Equations

Lake.LogT m = StateT Lake.Log m

Instances For

instance Lake.LogT.instMonadGetLogOfMonad {m : Type → Type} [Monad m] :

Lake.MonadGetLog (Lake.LogT m)

Equations

Lake.LogT.instMonadGetLogOfMonad = { getLog := get }

@[inline]

def Lake.LogT.log {m : Type → Type} [Monad m] (e : Lake.LogEntry) :

Lake.LogT m PUnit

Equations

Lake.LogT.log e = modify fun (x : Lake.Log) => x.push e

Instances For

instance Lake.LogT.instMonadLogOfMonad {m : Type → Type} [Monad m] :

Lake.MonadLog (Lake.LogT m)

Equations

Lake.LogT.instMonadLogOfMonad = { logEntry := Lake.LogT.log }

@[reducible, inline]

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

Equations

Lake.ELogT m = Lake.EStateT Nat Lake.Log m

Instances For

instance Lake.ELogT.instMonadGetLogOfPure {m : Type → Type} [Pure m] :

Lake.MonadGetLog (Lake.ELogT m)

Equations

Lake.ELogT.instMonadGetLogOfPure = { getLog := get }

@[inline]

def Lake.ELogT.log {m : Type → Type} [Monad m] (e : Lake.LogEntry) :

Lake.ELogT m PUnit

Equations

Lake.ELogT.log e = modify fun (x : Lake.Log) => x.push e

Instances For

instance Lake.ELogT.instMonadLogOfMonad {m : Type → Type} [Monad m] :

Lake.MonadLog (Lake.ELogT m)

Equations

Lake.ELogT.instMonadLogOfMonad = { logEntry := Lake.ELogT.log }

@[inline]

def Lake.ELogT.errorWithLog {m : Type → Type} {α : Type} {β : Type} [Monad m] (x : Lake.ELogT m α) :

Lake.ELogT m β

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

Equations

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

Instances For

@[inline]

def Lake.ELogT.error {m : Type → Type} {α : Type} [Monad m] (msg : String) :

Lake.ELogT m α

Equations

Lake.ELogT.error msg = (Lake.logError msg).errorWithLog

Instances For

instance Lake.ELogT.instMonadErrorOfMonad {m : Type → Type} [Monad m] :

Lake.MonadError (Lake.ELogT m)

Equations

Lake.ELogT.instMonadErrorOfMonad = { error := fun {α : Type} => Lake.ELogT.error }

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

Equations

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

Instances For

@[inline]

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

Equations

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

Instances For

@[inline]

def Lake.ELogT.captureLog {m : Type → Type} {α : Type} [Monad m] (self : Lake.ELogT m α) :

m (Option α × Lake.Log)

Equations

self.captureLog = do let __do_lift ← self ∅ match __do_lift with | Lake.EResult.ok a log => pure (some a, log) | Lake.EResult.error a log => pure (none, log)

Instances For

@[reducible, inline]

abbrev Lake.LogIO (α : Type) :

Equations

Lake.LogIO = Lake.ELogT BaseIO

Instances For

instance Lake.instMonadLiftIOLogIO :

MonadLift IO Lake.LogIO

Equations

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