lean3 aarch64 (apple m2) build issues

Stream: new members

[Alex Kontorovich]

Got a new computer (Apple M2 chip), trying to reinstall Lean3 (and Lean4); tried a bunch of things (even had ChatGPT help!...) but still can't get Lean to work; main error is: "error: binary package was not provided for 'darwin_aarch64'"... Is there an M2 version of these instructions? https://leanprover-community.github.io/install/macos.html Thanks!

[Yaël Dillies]

Run elan self update (or rather the brew version thereof). You have an outdated (by 10 months) elan.

[Alex Kontorovich]

error: self-update is disabled for this build of elan
error: you should probably use your system package manager to update elan

[Alex Kontorovich]

GPT said that the brew version might be: "brew upgrade elan". That gave the error:
"Error: Cannot install under Rosetta 2 in ARM default prefix (/opt/homebrew)!
To rerun under ARM use:
arch -arm64 brew install ..."

[Alex Kontorovich]

So I tried "arch -arm64 brew install elan". Got this:
"Warning: Treating elan as a formula. For the cask, use homebrew/cask/elan
Warning: elan-init 1.4.5 is already installed and up-to-date.
To reinstall 1.4.5, run:
brew reinstall elan-init"

[Matthew Ballard]

It looks like you are trying to use the arm-based brew since it is looking in /opt/. Check that you have another copy of brew at /usr/local/bin/brew and make sure to preface all calls to brew with the full path.

[Matthew Ballard]

Or just stick to Lean 4 ;)

[Julian Berman]

What does type -a elan say?

[Alex Kontorovich]

It says:

elan is /opt/homebrew/bin/elan
elan is /usr/local/bin/elan

[Kevin Buzzard]

Are they defeq?

[Alex Kontorovich]

...? I don't have univalence...

[Julian Berman]

Might be a Lean 5 feature.

But that's saying you have 2 Homebrews, and thereby 2 elans. Your x86_64 brew lives at /usr/local/bin/brew probably, and your ARM one at /opt/homebrew/bin/brew (you can confirm with type -a brew). It would seem also that your /usr/local/bin/ directory is probably first on your PATH -- so writing brew is finding you /usr/local/bin/brew. When you write arch -arm64 brew whatever that isn't magically making brew find the other one I don't think.

So tl;dr:

• Run /opt/homebrew/bin/brew info elan-init to see what version of ARM elan you have -- is it up to date? If not, run /opt/homebrew/bin/brew update && /opt/homebrew/bin/brew upgrade elan
• If that works and you have no reason to specifically want an x86_64 homebrew for other reasons, uninstall it entirely
• If you get some other error after doing ^^ lemme know :)

[Wojciech Nawrocki]

Hi! I am facing the same issue. elan --version shows elan 1.4.5 (b325638d9 2023-04-26), so quite new, and it is an ARM64 binary. Then elan install leanprover-community/lean:3.51.1 shows error: binary package was not provided for 'darwin_aarch64'.

[Wojciech Nawrocki]

Oh, are there actually just not binary builds of Lean 3 for this platform? That's ok, I'll build it manually.

[Xavier Roblot]

There are no Silicon binary for Lean3. You have to either build it yourself (that’s what I do) or use the Intel binary via Rosetta.