Performance statistics for Mathlib

Stream: mathlib4

[Daniel Weber]

Is there any good way to obtain performance data for Mathlib? I'm interesting in more fine-grained questions than the speedcenter has, for example:

• How much time is spent in the kernel?
• How much time is spent in isDefEq?
• How much time is spent in tactics which eventually fail?
• How much time is spent on parsing?

[Kevin Buzzard]

There might be some answers in this video https://www.youtube.com/watch?v=T0M5WpnuneE but it's still on my watch list as opposed to my watched list :-/

[Kevin Buzzard]

I would expect that there is 0 time spent on tactics which eventually fail -- a tactic which fails with an error wouldn't make it into mathlib, and we have a linter which lints against tactics which do nothing.

[Henrik Böving]

Kevin Buzzard said:

I would expect that there is 0 time spent on tactics which eventually fail -- a tactic which fails with an error wouldn't make it into mathlib, and we have a linter which lints against tactics which do nothing.

That's not necessarily true, for example if you have proof automation that uses first it could happen that you run a couple of tactics before hitting the right one

[Henrik Böving]

And just doing a very basic search there is almost 100 of these in mathlib:

λ git grep "first |" | wc -l
87