Zulip Chat Archive

Stream: general

Topic: lean3 on M1 chip

Thorsten Altenkirch (Oct 04 2022 at 10:29):

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 (Oct 04 2022 at 10:39):

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

Jason Rute (Oct 04 2022 at 10:46):

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 (Oct 04 2022 at 10:57):

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 (Oct 04 2022 at 11:32):

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 (Oct 04 2022 at 11:40):

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

Last updated: Dec 20 2023 at 11:08 UTC