Zulip Chat Archive

Stream: general

Topic: Profiling mathlib


Moritz Doll (Nov 05 2022 at 14:05):

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 (Nov 05 2022 at 14:06):

-Dprofiler.threshold=2000

Moritz Doll (Nov 05 2022 at 14:24):

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

Moritz Doll (Nov 05 2022 at 15:14):

#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 (Nov 05 2022 at 16:12):

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 (Nov 05 2022 at 16:14):

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

Jireh Loreaux (Nov 05 2022 at 19:01):

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 (Nov 05 2022 at 21:57):

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 (Nov 06 2022 at 16:10):

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 (Nov 06 2022 at 16:47):

I think he meant simp vs simp only


Last updated: Dec 20 2023 at 11:08 UTC