Log4Types.Async

Asynchronous logging: a background fiber drains a bounded channel
and runs the underlying `LogAction` off the application's critical
path, so a log call costs a channel write instead of backend IO.

Definitions

record AsyncConfig : Type

  Configuration for the background log worker.

Totality: total
Visibility: public export
Constructor: 

MkAsyncConfig : Nat -> AsyncConfig

Projection: 

.capacity : AsyncConfig -> Nat

  Maximum messages buffered in the channel. When full, log calls
  block the calling fiber until the worker catches up.

.capacity : AsyncConfig -> Nat

  Maximum messages buffered in the channel. When full, log calls
  block the calling fiber until the worker catches up.

Totality: total
Visibility: public export

capacity : AsyncConfig -> Nat

  Maximum messages buffered in the channel. When full, log calls
  block the calling fiber until the worker catches up.

Totality: total
Visibility: public export

defaultAsyncConfig : AsyncConfig

  Sensible default: a 1024-message buffer.

Totality: total
Visibility: public export

withAsyncLogger : AsyncConfig -> LogAction IO msg -> (LogAction (Async e []) msg -> Async e [] a) -> Async e [] a

  Run a computation with an async-backed `LogAction`.
  
  A background fiber drains a bounded channel and runs `underlying`
  on each message. The `LogAction` handed to the continuation
  enqueues in roughly constant time, blocking only when the channel
  is full. On scope exit the channel is closed and every pending
  message is flushed before returning.

Visibility: export