Idris/advent
1
0
Fork 0
Code Issues Pull requests Actions Packages Projects Releases Wiki Activity

Overhaul logging

Browse source 
Provide a proper logging effect that filters messages by log level
before generating them.
This commit is contained in:
Nathan McCarty 2025-01-09 15:48:24 -05:00
parent fb2f643efa
commit e2a26d9519
4 changed files with 140 additions and 61 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

1
.gitignore vendored
View file

@ -3,3 +3,4 @@ inputs/
*.*~
support/*.o
support/advent-support
tmp/

44
src/Main.md
View file

@ -1,4 +1,3 @@
<!-- markdown-toc start - Don't edit this section. Run M-x markdown-toc-refresh-toc -->
**Table of Contents**
- [Advent of Code](#advent-of-code)
@ -16,8 +15,6 @@
- [Lower logging into the IO component of the effect](#lower-logging-into-the-io-component-of-the-effect)
- [Handle the effectful action as an IO action ](#handle-the-effectful-action-as-an-io-action)
<!-- markdown-toc end -->
# Advent of Code
This module provides a command line interface for running the solution to a specific day for a specific year, run as `advent $YEAR $DAY`.
@ -180,11 +177,9 @@ Handle the verbosity flag, if it is set, hook our logger up to stderr, otherwise
```idris
-- If the verbose flag is set, hook up the logging writer to stderr
let verbose = any (== Verbose) opts.options
let logHandler : Eff [IO, Except Error, WriterL "log" String] () -> Eff [IO, Except Error] () =
if verbose
then handleLog ePutStrLn
else handleLog (\x => pure ())
let verbosity = count (== Verbose) opts.options
let logHandler : Eff [IO, Except Error, Logger] () -> Eff [IO, Except Error] () =
handleLog (Warn >+ verbosity)
-- Add the logging writer to the effect
logHandler $ do
```
@ -244,28 +239,6 @@ Check and see if the selected `Day` has a part 2, if it does, feed the opaque co
where
```
### Print strings to stderr
Putting this in its own function makes dealing with the potential error returned by `fPutStrLn` a bit eaiser. It's reasonable to ignore this error, since if we can't write to stderr we are kinda powerless to tell anyone about it.
```idris
-- print to standard error
ePutStrLn : Lazy String -> IO ()
ePutStrLn str = do
_ <- fPutStrLn stderr str
pure ()
```
### Decompose a Writer
Having this be a function keeps the `a` somewhat opaque and helps with they type checking. Only values of `Writer $TYPE ()` can actually be constructed, but the type checker gets a little bit confused about this when you try to do this by pattern matching inline.
```idris
-- Decompose a writer, eases type inference
unwriter : WriterL "log" String a -> (a, String)
unwriter (Tell vw) = ((), vw)
```
### Lower logging into the IO component of the effect
This function uses the provided `String -> IO ()` to remove the `Writer` from the effects list by translating `tell` calls to IO actions within the effect.
@ -273,14 +246,13 @@ This function uses the provided `String -> IO ()` to remove the `Writer` from th
```idris
-- Lowers logging into IO within the effect using the given IO function
handleLog :
Has (WriterL "log" String) fs => Has IO (fs - WriterL "log" String) =>
(tell : Lazy String -> IO ()) -> Eff fs a -> Eff (fs - (WriterL "log" String)) a
handleLog tell x =
Has Logger fs => Has IO (fs - Logger) =>
(max_log : Level) -> Eff fs a -> Eff (fs - Logger) a
handleLog max_log x =
handle
(\msg, f =>
do let (val, msg) = unwriter msg
_ <- send $ tell msg
f val) x
do _ <- send $ handleLoggerIO max_log msg
f $ ignore msg) x
```
# Handle the effectful action as an IO action

7
src/Runner.md
View file

@ -1,4 +1,3 @@
<!-- markdown-toc start - Don't edit this section. Run M-x markdown-toc-refresh-toc -->
**Table of Contents**
- [Unified interface for any day from any year](#unified-interface-for-any-day-from-any-year)
@ -14,8 +13,6 @@
- [Methods](#methods)
- [locate](#locate)
<!-- markdown-toc end -->
# Unified interface for any day from any year
This module provides some basic data types for building an application containing all my solutions to all of the parts of all the days across all of the years.
@ -28,6 +25,8 @@ module Runner
import Control.Eff
import Structures.Dependent.FreshList
import public Util.Eff
%default total
```
@ -43,7 +42,7 @@ A `Writer` effect is provided for logging, and a `Reader` effect is provided to
public export
PartEff : (err : Type) -> List (Type -> Type)
PartEff err =
[IO, Except err, WriterL "log" String, ReaderL "input" String]
[IO, Except err, Logger, ReaderL "input" String]
```
# The `Day` Record

143
src/Util/Eff.md
View file

@ -8,32 +8,139 @@ module Util.Eff
import Control.Eff
import Text.ANSI
import System
import System.File
%default total
```
## Logging
Use the `WriterL "log" String` effect like a logging library. We'll provide a few "log levels" as verbs for the effect, but no filtering is done, when logging is enabled, all logs are always displayed, however the log level is indicated with a colored tag.
### Log Levels
Basic enumeration describing log levels, we define some (hidden) utility functions for working with these.
```idris
public export
data Level = Err | Warn | Info | Debug | Trace | Other Nat
```
<!-- idris
namespace Logging
export
levelToNat : Level -> Nat
levelToNat Err = 0
levelToNat Warn = 1
levelToNat Info = 2
levelToNat Debug = 3
levelToNat Trace = 4
levelToNat (Other k) = k
export
natToLevel : Nat -> Level
natToLevel 0 = Err
natToLevel 1 = Warn
natToLevel 2 = Info
natToLevel 3 = Debug
natToLevel 4 = Trace
natToLevel k = Other k
export
Eq Level where
x == y = levelToNat x == levelToNat y
export
Ord Level where
compare x y = compare (levelToNat x) (levelToNat y)
export infixl 8 >+
export
(>+) : Level -> Nat -> Level
(>+) x k = natToLevel (k + levelToNat x)
-->
Convert a `Level` into a colorized tag
```idris
export
info : Has (WriterL "log" String) fs => Lazy String -> Eff fs ()
info str =
let tag = show . bolden . show . colored Green $ "[INFO]"
in tellAt "log" (tag ++ ": " ++ str ++ "\n")
export
debug : Has (WriterL "log" String) fs => Lazy String -> Eff fs ()
debug str =
let tag = show . bolden . show . colored BrightWhite $ "[DEBUG]"
in tellAt "log" (tag ++ ": " ++ str ++ "\n")
export
warn : Has (WriterL "log" String) fs => Lazy String -> Eff fs ()
warn str =
let tag = show . bolden . show . colored Yellow $ "[WARN]"
in tellAt "log" (tag ++ ": " ++ str ++ "\n")
levelToTag : Level -> String
levelToTag Err =
show . bolden . show . colored BrightRed $ "[Error]"
levelToTag Warn =
show . bolden . show . colored BrightYellow $ "[Warning]"
levelToTag Info =
show . bolden . show . colored Green $ "[Info]"
levelToTag Debug =
show . bolden . show . colored Magenta $ "[Debug]"
levelToTag Trace =
show . bolden . show . colored Cyan $ "[Trace]"
levelToTag (Other k) =
show . bolden . show . colored BrightWhite $ "[\{show k}]"
```
### Logger effect
This is a basic data structure that captures a lazy log message (so we don't have to pay any of the costs associated with generating the log message when it is filtered)
```idris
public export
data Logger : Type -> Type where
Log : (level : Level) -> (msg : Lazy String) -> Logger ()
```
We'll also provide some basic accessors, and an `ignore` function useful for writing handlers.
```idris
export
(.level) : Logger t -> Level
(.level) (Log level msg) = level
export
(.msg) : Logger t -> Lazy String
(.msg) (Log level msg) = msg
export
ignore : Logger t -> t
ignore (Log level msg) = ()
```
#### Handler
Because we know that we will only be using `logger` in an `IO` context, we aren't currently going to provide a `runLogger` or the like, instead we'll define a function, suitable for use as a `runEff` handler, that filters log messages and prints them to `stderr` over `IO`.
In the event a log message is filtered out, it's inner message is never inspected, avoiding evaluation.
```idris
export
handleLoggerIO :
(max_level : Level) -> Logger t -> IO t
handleLoggerIO max_level x =
if x.level <= max_level
then do
_ <- fPutStrLn stderr "\{levelToTag x.level}: \{x.msg}"
pure . ignore $ x
else pure . ignore $ x
```
Use the `WriterL "log" String` effect like a logging library. We'll provide a few "log levels" as verbs for the effect, but no filtering is done, when logging is enabled, all logs are always displayed, however the log level is indicated with a colored tag.
```idris
export
error : Has Logger fs => Lazy String -> Eff fs ()
error x = send $ Log Err x
export
warn : Has Logger fs => Lazy String -> Eff fs ()
warn x = send $ Log Warn x
export
info : Has Logger fs => Lazy String -> Eff fs ()
info x = send $ Log Info x
export
debug : Has Logger fs => Lazy String -> Eff fs ()
debug x = send $ Log Debug x
export
trace : Has Logger fs => Lazy String -> Eff fs ()
trace x = send $ Log Trace x
```