What does "tactic execution" measure in the speedcenter?

Stream: lean4

[Eric Wieser]

In #9422, the benchmarking script is reporting that a change to a tactic that seems to be used 2-3 times in all of mathlib has increased the tactic runtime by 7.5%. This is pretty strange to me, because the test file that exercises this tactic shows a 4% speed boost.

Is this measuring the sum of the runtimes of all tactics, or just the longest tactic runtime?

[Jeremy Tan]

It's the former. The metric has gone from 1298 seconds to 1395 seconds

[Jeremy Tan]

Also note that Tactic.CancelDenoms.Core is imported by Tactic.Linarith.Preprocessing, and linarith has a ton of uses in mathlib4

[Eric Wieser]

Somehow I missed that import

[Eric Wieser]

It's still strange that the test is faster but mathlib is slower

[Eric Wieser]

But I guess I should profile the linarith tests too

[Eric Wieser]

The linarith test also got marginally faster

[Eric Wieser]

So maybe this is bogus? The total build time only increased by 5s