set_option profiler

Stream: general

[Damiano Testa]

Dear All,

in the context of trying to speed up a tactic (related to #15691, if it is relevant), I am using set_option profiler true to see what consumes time. However, I do not really understand how to read the results.

My understanding is that the tactic flags every time that one function call moves on to the next one.

Should I be looking at large differences between percentages? Are these differences really measuring how much time is spent on one of the computations?

Is there some other funcionality that I can use to help understand where Lean is spending most of its time?

Thanks!

[Anne Baanen]

I understand that the percentages count how often the call shows up in the call stack. So if you have something like:

def g (x : ℕ) := something_slow x - another_slow_thing x

def f (x : ℕ) := g (x + x)

then the profiler might show something like:

f 100%
g 98%
something_slow 49%
another_slow_thing 49%
has_add.add 2%