Optionally include a measure of work size in -ddump-timings.
Currently -ddump-timings is quite handy to measure the time/allocations for certain phases.
However it's hard to judge if a growth in time/allocations stems from the compiler processing a larger work load or from us processing it less efficiently.
So I would like to have a flag like -ddump-timings-extra
which produces a bit more information.
In particular instead of emitting this info:
Simplifier [Agda.Syntax.Parser.Lexer]: alloc=124670096 time=52.135
Simplifier [Agda.Syntax.Parser.Lexer]: alloc=122955936 time=51.450
I would like to include info about the core size. For example emit something like:
Simplifier [Agda.Syntax.Parser.Lexer]: alloc=124670096 time=52.135 size={total=50, terms=20, types=30, coercions=0}
Simplifier [Agda.Syntax.Parser.Lexer]: alloc=122955936 time=51.450 size={total=60, terms=20, types=30, coercions=10}
We could do so by changing withTiming to something like:
withTiming :: MonadIO m
=> Logger
-> SDoc -- ^ The name of the phase
-> (a -> ()) -- ^ A function to force the result
-- (often either @const ()@ or 'rnf')
-> (a -> SDoc) -- ^ A function to output a representation of the size of the result (e.g. core size)
-> m a -- ^ The body of the phase to be timed
-> m a