elan installation fails

Stream: general

[John]

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]

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

[John]

@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]

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

[John]

It is Apple M1.

[Alistair Tucker]

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]

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

[John]

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

[Alistair Tucker]

https://github.com/leanprover-community/lean/blob/master/doc/make/index.md

[John]

Thanks a lot! I'll try it!

[Alistair Tucker]

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

[Patrick Stevens]

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?