2 × 6% mathlib build speedup (clickbait title)

Stream: mathlib4

[Joachim Breitner]

I benchmarked two small changes to lean4 using the speedcenter, and both gave a 6% build time improvement:

• http://speed.lean-fro.org/mathlib4/compare/d444b71b-0228-43f5-951d-975ddabbc565/to/77bd3441-1d67-4527-9a0c-188a17a83b8f
• http://speed.lean-fro.org/mathlib4/compare/d444b71b-0228-43f5-951d-975ddabbc565/to/f1d3f7dd-931f-4250-9a10-263dbc927957

So if I merge them both, does that mean we’ll get ~12% improvement?…

Unfortunately, this is too good to be true; the “instruction count” tells a different (and more plausible) story. It seems that this particular base line build took longer than usual, and now everything I do looks like an improvement. Oh well, it would have been so nice…

[Yaël Dillies]

Clearly that's wrong because you forgot how percentages work. The expected speedup is $100\% - 94\%^2 = 11.64\%$ :grinning:

[Joachim Breitner]

I took this into account, accounted lazily , and wrote ~ for that reason :-)

[Joachim Breitner]

Also, if they improve independent code paths, the speedup will even be more than 12%!