Zulip Chat Archive

Stream: new members

Topic: lean3 aarch64 (apple m2) build issues

Alex Kontorovich (May 26 2023 at 22:30):

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 (May 26 2023 at 22:32):

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

Alex Kontorovich (May 26 2023 at 22:34):

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

Alex Kontorovich (May 26 2023 at 22:40):

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 (May 26 2023 at 22:41):

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 (May 27 2023 at 15:33):

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 (May 27 2023 at 15:35):

Or just stick to Lean 4 ;)

Julian Berman (May 27 2023 at 19:55):

What does type -a elan say?

Alex Kontorovich (May 30 2023 at 18:26):

It says:

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

Kevin Buzzard (May 30 2023 at 21:13):

Are they defeq?

Alex Kontorovich (May 30 2023 at 22:49):

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

Julian Berman (May 31 2023 at 13:37):

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 (Jun 07 2023 at 23:30):

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 (Jun 07 2023 at 23:32):

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

Xavier Roblot (Jun 08 2023 at 04:29):

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.

Last updated: Dec 20 2023 at 11:08 UTC