Time to compile Mathlib on M3 ?

Stream: mathlib4

[Nicolas Rolland]

On my M1 with 16G of ram, time lake build mathlib from scratch gives :

lake build 21723.19s user 160.15s system 629% cpu 1:01:57.48 total

How long does it take on M2/ M3 (Max ?)?

(obviously one should lake exe cache get in projects, this is just to know performance )

[Scott Morrison]

M2 Ultra 24 core:

lake build  17971.65s user 1741.70s system 1373% cpu 23:55.61 total

(that was in mid-sept, but according to the speed center Mathlib wall-clock has dropped significantly since then)

[Nicolas Rolland]

this can be useful for people thinking of buying a new mac to know what's the improvement

[Scott Morrison]

Fresh run says:

lake build  17060.14s user 2162.88s system 1688% cpu 18:58.57 total

Nice parallelism boost!

[Julian Berman]

On my M2 MB Air (8GB RAM) it usually takes around 5 hours. On my Mac Mini it takes around 3.5. EDIT: no this is me not properly running the build via caffeinate

[Arthur Paulino]

[offtopic] how long did it take to compile mathlib in Lean 3 again? 3 hours?

[Julian Berman]

Longer than that here. Though now I'm doing fresh runs (first of Lean 4 on each then maybe I'll try mathlib3.)

[Julian Berman]

OK it's indeed faster than I said -- not sure if I plain misremembered or whether it's due to speedups, but on that Mac Mini (also 8GB by the way, although the build never seems memory constrained), it just took 50 minutes -- so at least somewhat closer to Scott's beefier machine :).

[Mauricio Collares]

It's impossible to compile mathlib3 with 8GB of RAM, I think, even if you disable parallelism entirely. I guess you can technically use swap/virtual memory, but I can't imagine it will be tolerable.

[Oliver Nash]

Scott Morrison said:

Fresh run says:

lake build  17060.14s user 2162.88s system 1688% cpu 18:58.57 total

Nice parallelism boost!

On an M3 Max, using commit b1febe509882bc82b2a57889876c87b23243547d I see:

lake build  14469.76s user 1279.94s system 1255% cpu 20:54.64 total

[Nicolas Rolland]

Going from 1h to 20' from M1 to m2ultra/m3 max, that's quite a bit of a difference ! Good to know. (I guess it's also the architecture (memory/ssd etc..))