Log4Types.File.Rotation

(source)

Size-based rotation for file-backed loggers.

`withRotatingLogFile` is a continuation-style entry point that gives
the user a `LogAction` writing to a file. When the file's size exceeds
a configured limit, the action rotates the file (renaming
`app.log` to `app.log.1`, shifting older files up, and deleting
anything beyond a count limit), then continues writing to a fresh
file at the original path.

Definitions

renameFile : HasIO io => String -> String -> io (Either FileError ())

  Rename a file. Returns `Left` on failure (most often: source missing or
  permission denied). The `FileError` is `GenericFileError` carrying the
  platform's raw return code, since structured errnos are not available
  across all backends.

Totality: total
Visibility: export

record RotationConfig : Type

  Configuration for size-based file rotation.

Totality: total
Visibility: public export
Constructor:

MkRotationConfig : Integer -> Nat -> RotationConfig

Projections:

.maxBytes : RotationConfig -> Integer

  Maximum bytes in the current file before rotation triggers.

.maxFiles : RotationConfig -> Nat

  Maximum number of rotated files to keep (file.1, file.2, ...).
  Files beyond this are deleted after rotation.

.maxBytes : RotationConfig -> Integer

  Maximum bytes in the current file before rotation triggers.

Totality: total
Visibility: public export

maxBytes : RotationConfig -> Integer

  Maximum bytes in the current file before rotation triggers.

Totality: total
Visibility: public export

.maxFiles : RotationConfig -> Nat

  Maximum number of rotated files to keep (file.1, file.2, ...).
  Files beyond this are deleted after rotation.

Totality: total
Visibility: public export

maxFiles : RotationConfig -> Nat

  Maximum number of rotated files to keep (file.1, file.2, ...).
  Files beyond this are deleted after rotation.

Totality: total
Visibility: public export

defaultRotation : RotationConfig

  Default rotation: 10 MB per file, keep 5 rotated copies.

Totality: total
Visibility: public export

withRotatingLogFile : HasIO io => String -> RotationConfig -> (LogAction io String -> io a) -> io (Either FileError a)

  Run a computation with a rotating file-backed `LogAction`.
  
  Writes go to `basePath`. When size exceeds `config.maxBytes`,
  `basePath` is renamed to `basePath.1`, previous `.1` becomes `.2`,
  and so on up to `config.maxFiles`. Files beyond that count are
  deleted on rotation.
  
  Returns `Left FileError` if the initial open failed, otherwise
  `Right` with the callback's result.

Totality: total
Visibility: export