profiling / timing only the top-level commands?

Stream: lean4

[Jason Gross]

Is there a way to get lean to tell me how long each line takes to run/elaborate (Elab.command), without spending a bunch of time (a) printing the line, and (b) tracing/printing children? I have a file that takes 100x longer to run with the profiler on than with it off.

[Aaron Liu]

Maybe #time?

[Sebastian Ullrich]

You can set the trace profiler threshold very high but then enable Elab.command specifically

[Jason Gross]

Thank you both! Is there a way to set the output format of #time?

[Jason Gross]

Actually, @Sebastian Ullrich , if I do

set_option trace.profiler true
set_option trace.profiler.threshold 1000
set_option trace.Elab.command true

then I see the trace for [Elab.command], but I don't see the timing for it. I want to see the profile on everything that's enabled / to disable the trace on everything but Elab.command.

[Sebastian Ullrich]

If I open that code in the playground and add another command, I do get timings. Maybe some old Lean version?

[Jason Gross]

I'm running Lean (version 4.18.0, arm64-apple-darwin23.6.0, commit 11ccbced7964, Release)

[Jason Gross]

But indeed switching to nightly seems to show timings