Lean M1 Performance Tests

Stream: general

[Bolton Bailey]

I just installed lean on my Mom's new 2021 Macbook Pro with Apple M1 Pro chip. For us Mac users thinking of a hardware upgrade, I intend to run some lean code on both this and my own 2017 Macbook Pro with 2.9 GHz Quad-Core Intel Core i7 to see the performance difference.

[Bolton Bailey]

Building the tutorials project with leanproject clean ; time lean --make src/ a few times each, I get on the M1:
lean --make src/ 107.44s user 1.18s system 564% cpu 19.250 total
lean --make src/ 108.29s user 1.21s system 559% cpu 19.572 total
lean --make src/ 107.44s user 1.34s system 549% cpu 19.795 total
And on the Intel
lean --make src/ 143.49s user 3.61s system 497% cpu 29.572 total
lean --make src/ 164.34s user 4.24s system 527% cpu 31.966 total
lean --make src/ 167.17s user 4.24s system 520% cpu 32.922 total

[Bolton Bailey]

I'll try building some bigger projects later when I have more time.

[Eric Rodriguez]

is this the m1 or m1 pro?

[Bolton Bailey]

"Apple M1 Pro" is what the About This Mac infobox said.

[Kevin Buzzard]

Is your mom on the Zulip? Does she need some good first projects?

[Kevin Buzzard]

More seriously I guess you could pull a project like the liquid tensor experiment and compile that, that takes about 20 minutes to compile on a good machine IIRC (get a mathlib cache first)

[Kevin Buzzard]

Maybe the tutorials project doesn't have enough files to force all your cores to work at the same time?

[Patrick Stevens]

For me, M1 Max 16-inch with lean built from source targeting darwin-aarch64 (version 3.35.1, commit 4887d8a30621, Release ), leanproject clean then leanproject get-mathlib-cache then lean --make src in lean-liquid 890de421fb successfully maxes out the CPU and is making the machine noticeably warmer, which is unusual; will report timings when I wake up tomorrow unless it's really fast

[Patrick Stevens]

A big chunk in the middle of compilation where CPU usage dropped down as low as 50% - there's definitely some bottlenecks here. Final output (on battery power, which I guess might make a difference):
~/.elan/toolchains/stable/bin/lean --make src 7786.48s user 31.84s system 733% cpu 17:46.21 total

[Bolton Bailey]

I get a similar
lean --make src/ 6135.28s user 18.85s system 632% cpu 16:12.31 total
For lean-liquid on M1, with
lean --make src 10643.33s user 159.04s system 604% cpu 29:47.20 total
For intel.

[Eric Rodriguez]

These macbooks don't seem to care about being on battery power, they're impressive...