Zulip Chat Archive

Stream: general

Topic: elan installation fails

John (Nov 20 2022 at 09:33):

Hello! I am now trying to install elan onto my MacBook. However, after typing in "brew install elan-init" into my terminal, I got a message "elan-init: The x86_64 architecture is required for this software.
Error: elan-init: An unsatisfied requirement failed this build."
How can I solve this problem?

Scott Morrison (Nov 20 2022 at 09:35):

@John, please see https://leanprover-community.github.io/install/macos.html

John (Nov 20 2022 at 10:22):

@Scott Morrison Thank you for your reply! I followed the instructions in that link. However, when I typed in "software update --install-rosetta" and pressed "Enter", another error message appeared: "Installing Rosetta 2 on this system is not supported." Why does this happen?

Alistair Tucker (Nov 20 2022 at 10:23):

Is your Mac one of the new ones i.e. M1/M2?

John (Nov 20 2022 at 10:26):

It is Apple M1.

Alistair Tucker (Nov 20 2022 at 10:29):

Well I don't know why Rosetta doesn't work, perhaps someone else can chime in on that. But if we can't fix it then another option is to compile Lean 3 from scratch. I did it last night and it turned out to be totally straightforward.

Alistair Tucker (Nov 20 2022 at 10:29):

I assume you want Lean 3? Lean 4 would be easier still.

John (Nov 20 2022 at 10:40):

Could you please send me the link for the instructions of installing Lean 3? Thank you so much!

Alistair Tucker (Nov 20 2022 at 10:42):


John (Nov 20 2022 at 10:42):

Thanks a lot! I'll try it!

Alistair Tucker (Nov 20 2022 at 10:44):

Once it's compiled you should run elan toolchain link. At least that's what I did.

Patrick Stevens (Nov 20 2022 at 12:30):

The Internet suggests that a reboot might fix the "installing Rosetta 2 is not supported" error. Additionally it suggests that installation may fail if an organisation is managing your laptop configuration - is that the case?

Last updated: Aug 03 2023 at 10:10 UTC