Total execution time for an entire `by` block

Stream: lean4

[Eric Wieser]

When I use set_option profiler.true, I get output like

typeclass inference of Module took 716ms
tactic execution of Std.Tactic.obtain took 133ms
typeclass inference of Module took 418ms
typeclass inference of Module took 115ms
tactic execution of Lean.Parser.Tactic.refine took 426ms
tactic execution of Lean.Parser.Tactic.rewriteSeq took 4.3s
typeclass inference of CoeFun took 206ms
typeclass inference of Module took 267ms
typeclass inference of Module took 353ms
tactic execution of Lean.Parser.Tactic.refine took 575ms
typeclass inference of Module took 166ms
typeclass inference of FiniteDimensional took 153ms
typeclass inference of StrongRankCondition took 128ms
typeclass inference of Module took 449ms
typeclass inference of Module.Finite took 512ms
tactic execution of Lean.Parser.Tactic.rewriteSeq took 2.59s
typeclass inference of Module took 404ms
typeclass inference of Module.Finite took 519ms
tactic execution of Lean.Parser.Tactic.rewriteSeq took 2.68s
typeclass inference of StrongRankCondition took 204ms
typeclass inference of Module took 548ms
tactic execution of Lean.Parser.Tactic.exact took 2.81s
type checking took 129ms

How do I get lean to give me a total time for the entire proof? I think adding up the numbers won't work because the threshold causes some tactics to be omitted from this list.

[Henrik Böving]

set_option trace.profiler true + my excellent flame tool of course!

[Eric Wieser]

Is there any reason to still have profiler? Could it be renamed to trace.profiler.basic or something to make it easier to discover one if you know about the other?

[Henrik Böving]

You'll have to ask @Sebastian Ullrich I have in fact been adding withTraceNode stuff to many of the profileItM calls so it should be close to isomorphic by now...I believe the only thing trace.profiler can not access is the C part of the old code generator

[Sebastian Ullrich]

Eric Wieser said:

Is there any reason to still have profiler?

The cumulative summary profiler outputs at the end is used by tools like the speedcenter and isn't really something that would fit into trace.profiler IMO. However, the intermediary X took Y messages could perhaps be removed in favor of trace.profiler when the old compiler is gone.

Could it be renamed to trace.profiler.basic or something to make it easier to discover one if you know about the other?

It doesn't really have to do anything with traces