Cost of tactics

Stream: mathlib4

[Antoine Chambert-Loir]

What is the energy/time cost of the tactics that leave some uninteresting and automatizable work to the computer?
More precisely, assume we end a proof by

• rw [blah,…]
• simp only [blah,…]
• simp [blah]
• some more elaborate tactic such as group or ring,

where blah is some sequence of explicit lemmas, and … is some other simp-lemmas.

If I understand things correctly, each time the file is compiled, the compiler has to elaborate by itself a way out to the proof. Most of the time, unless some things have changed, this is the same way as before. So isn't it a waste of computer power to have the computer recompute this? Or is this waste definitely negligible in comparison with the rest of the compilation?

[Kyle Miller]

Let's say you have a 100W CPU with 8 threads of execution, electricity is 34 cents per kWh, mathlib is recompiled 100 times per day, and you have a tactic that takes 0.5 seconds to complete. That costs 2.2 cents of electricity per year.

[Kyle Miller]

Much more expensive is engineering time. If not using a more elaborate tactic means a maintainer needs to look at it for maintenance, then they can't spend more than a couple seconds fixing it.

[Kyle Miller]

There's a tradeoff though, since long compilation times aren't efficient for development either.

[Antoine Chambert-Loir]

Does one know how many times mathlib is recompiled every day?

[Damiano Testa]

This page contains usage statistics.

[Damiano Testa]

The actions build and bors are the main ones that, among other things, build mathlib.

[Edward van de Meent]

Those don't count local (possibly partial) builds tho

[Ruben Van de Velde]

Note that the cache saves a lot too

[Damiano Testa]

Estimating how many times users of mathlib build mathlib will be hard.

[Ruben Van de Velde]

Though then you need to look at the cost of storing and fetching and verifying the cache

[Kent Van Vels]

I have been interested in this too. Has there been any benchmarking done in this area? Is there evidence that term-based proofs compile faster than tactic based proofs?

[Damiano Testa]

I seem to remember that there is no correlation between term-mode vs tactic-mode for compile speed.

[Damiano Testa]

Or, rather, it can go both ways: I'm not actually sure about correlations.

[Kyle Miller]

There's not really any inherent overhead to using tactics vs terms in Lean's architecture. They're both roughly at the same level of abstraction.

Tactics can take advantage of global information when constructing terms that term elaborators can only infer in a piecewise way for example. I wouldn't be surprised if intro x y z were marginally faster than refine fun x y z => ?_ for example.