Understanding trace.profiler output

Stream: lean4

[Moritz R]

Why do i seem to see everything thrice in the output of the profiler?
I wouldn't expect to see the part about cases n with 3 times and would directly want to see how long each of the cases take. The second case also seems to print a few things multiple times.
Is there any way to have less redundancy in the output, but still know the time for each tactic/line?

set_option trace.profiler true
set_option trace.profiler.threshold 1
theorem nat_case_analysis (n : Nat) : n = 0 ∨ ∃ k, n = k + 1 -> False := by
  cases n with
  | zero =>
    rw?
  | succ k =>
    right
    exists k
    sorry

image.png

[Henrik Böving]

The output of trace.profiler is not in relation to tactics or lines but in relation to semantically meaningful steps in elaboration that are chosen by the authors of the tactic and the larger Lean eco system. If that happens to print the same thing multiple times because for some situations maybe the output would change at that point while for others it doesn't that's just how it is.

[Moritz R]

I wish there was an option to not show the parent, if there is exactly one child and this child takes almost the same amount of time as it's parent.

[Moritz R]

For larger proofs, using the profiler becomes an exercise in scrolling and clicking on the triangles until one actually finds any different timings from the whole-proof timing. This is often multiple screens of scrolling to do

[Moritz R]

Also, we already have the option to threshold away small children nodes, how is this so different from thesholding small intermediate nodes

[Sebastian Ullrich]

Only one of these checks is dirt-cheap. But there may be some low-hanging fruits for removing some of the redundant nodes, please consider opening an issue

[Moritz R]

Which one of the checks is not cheap?

[Moritz R]

(I have no experience with this)

[Sebastian Ullrich]

The one that is not implemented, skipping nested nodes with identical output

[Moritz R]

Isn't it linear in the number of nodes?
If this is too much, one could hide it behind a default-false option still