inductive System.Log.FastLogger.LogType : Type

Log output destination.

• stdout : LogType
• stderr : LogType
• file (path : String) : LogType
• callback (write : ByteArray → IO Unit) : LogType

@[reducible, inline]

abbrev System.Log.FastLogger.LogStr : Type

A log message (just a string for now).

Equations

• System.Log.FastLogger.LogStr = String

structure System.Log.FastLogger.LoggerSet : Type

An opaque handle to a running logger set.

• buffer : Std.Mutex (Array String)

  The mutex-protected buffer.

• flushAction : Array String → IO Unit

  The flush action (writes buffered content to destination).

• bufSize : Nat

  Maximum buffer size before auto-flush.

def System.Log.FastLogger.flushLogStr (logger : LoggerSet) : IO Unit

Flush all buffered messages to the destination. $$\text{flushLogStr} : \text{LoggerSet} \to \text{IO Unit}$$

Equations

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

def System.Log.FastLogger.newLoggerSet (logType : LogType) (bufSize : Nat := 4096) : IO LoggerSet

Create a new LoggerSet for the given destination. $$\text{newLoggerSet} : \text{LogType} \to \text{IO LoggerSet}$$

Equations

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

def System.Log.FastLogger.pushLogStr (logger : LoggerSet) (msg : LogStr) : IO Unit

Push a log message to the logger. May trigger an auto-flush if the buffer exceeds bufSize. $$\text{pushLogStr} : \text{LoggerSet} \to \text{LogStr} \to \text{IO Unit}$$

Equations

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

def System.Log.FastLogger.rmLoggerSet (logger : LoggerSet) : IO Unit

Close the logger: flush remaining messages. $$\text{rmLoggerSet} : \text{LoggerSet} \to \text{IO Unit}$$

Equations

• System.Log.FastLogger.rmLoggerSet logger = System.Log.FastLogger.flushLogStr logger

def System.Log.FastLogger.withTimedFastLogger {α : Type} (logType : LogType) (action : LoggerSet → IO α) : IO α

Convenience: create a timed logger that prepends timestamps. Uses AutoUpdate to cache the current time (updated once per second). $$\text{withTimedFastLogger} : \text{LogType} \to (\text{LoggerSet} \to \text{IO}\ \alpha) \to \text{IO}\ \alpha$$

Equations

• System.Log.FastLogger.withTimedFastLogger logType action = do let logger ← System.Log.FastLogger.newLoggerSet logType tryFinally (action logger) (System.Log.FastLogger.rmLoggerSet logger)