lean3 on M1 chip

Stream: general

[Thorsten Altenkirch]

I am sticking to lean 3 for my course but one student just told me that he is having problem to install lean 3 on an apple M1 chip? Is this correct? If so is there a workaround?

[Jason Rute]

Here are the official directions for M1/2 macs: https://leanprover-community.github.io/install/macos.html#m1-macs--apple-silicon

[Jason Rute]

If they are stuck after following those instructions (and that is common), then it is probably best if they hop on Zulip. It isn’t that there is a “work around”, but that the setup is a bit tricky (and probably easy to get one’s system in a weird state) so it is good for them to explain exactly what they did and what errors they are seeing.

[Jason Rute]

I wonder if that Mac installation page needs to be improved. For example since all new macs are M-series, should those directions be first, or should it be a single set of directions where the first step is “determine if your Mac is an M-series as follows:”? Also I knew someone who went straight to the video tutorial without reading further. That video tutorial probably needs too be augmented with another for M1 macs.

[Xin Huajian]

There's a discussion on this topic: https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/Installing.20mathlib.20on.20M1.20Mac. Hope it could help you.

[Floris van Doorn]

clickable link: https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/Installing.20mathlib.20on.20M1.20Mac