Profiling mathlib

Stream: general

[Moritz Doll]

Motivated by performance gains coming from squeezing (non)-terminal simps (#17344), I've looked a bit into profiling. It seems however that profiling whole files (or even folders) is not very nice since the output of lean --profile $file is rather verbose. What I would be interested in would be a list of say the 10 worst performing proofs or all proofs that take longer than 2s (on my machine this indicates long simps). Is there a quick&dirty way to do that?

[Sebastian Ullrich]

-Dprofiler.threshold=2000

[Moritz Doll]

Thanks. This seems to be suited to find non-terminal simps: in linear_algebra/basic: equiv_map_of_injective 7.85s -> 490ms

[Moritz Doll]

#17367
even with -Dprofiler.threshold=5 (5sec) there are still false negatives, but they can be found together with the (pretty bad) regex I wrote.

[Moritz Doll]

and the winner of the "worst performance in analysis/normed_space"-award is is_bounded_bilinear_map.is_bounded_linear_map_deriv with 33.7s followed by homeomorph_unit_ball with 32s.
It is impossible to find non-terminal simps with the profiler, there are so many badly performing proofs/declarations..

[Moritz Doll]

but hey is_bounded_bilinear_map.is_bounded_linear_map_deriv does have non-terminal simps :joy:

[Jireh Loreaux]

Sometimes the culprit is hidden behind some slow defeq check. In these cases it can be hard to find it, but it's sometimes possible to do a single rewrite before the defeq check to make it fast.

[Kevin Buzzard]

Yeah there is a real art to something like this. There are all sorts of subtle reasons why things could be slow, and one of the hardest to debug is a refl which is taking forever because of one unfortunate unfold taking the elaborator on a 10 second detour. Sometimes a rewrite fixes it, sometimes making something irreducible fixes it etc etc.

[Yaël Dillies]

Moritz Doll said:

It is impossible to find non-terminal simps with the profiler, there are so many badly performing proofs/declarations..

Surely there's no/little correlation between non-terminal simps and compilation time?

[Jireh Loreaux]

I think he meant simp vs simp only