Zulip Chat Archive

Stream: general

Topic: Installing mathlib on M1 Mac


Xin Huajian (Feb 25 2022 at 08:45):

I tried to install lean and mathlib on m1 mac as the guide from the community, when I used 'brew install mathlibtools' the terminal warned that No available formula with the name "mathlibtools". Can anyone figure out this problem?

Alexander Bentkamp (Feb 25 2022 at 09:23):

Maybe try brew update?

Alexander Bentkamp (Feb 25 2022 at 09:23):

What version of MacOS are you using?

Xin Huajian (Feb 25 2022 at 10:12):

I tried and it didn't work

Xin Huajian (Feb 25 2022 at 10:12):

macOS Monterey 12.2.1

Eric Rodriguez (Feb 25 2022 at 10:18):

can you put the output of the shell session?

Xin Huajian (Feb 25 2022 at 10:23):

Warning: No available formula with the name "mathlibtools".
==> Searching for similarly named formulae...
Error: No similarly named formulae found.
==> Searching for a previously deleted formula (in the last month)...
Error: No previously deleted formula found.
==> Searching taps on GitHub...
Error: No formulae found in taps.

Eric Rodriguez (Feb 25 2022 at 10:25):

and this is after brew update?

Xin Huajian (Feb 25 2022 at 10:26):

Yes

Eric Rodriguez (Feb 25 2022 at 10:27):

I mean, I guess you can install it using pip, but I really don't get it; it's clearly there, on all hoembrew versions too

Eric Rodriguez (Feb 25 2022 at 10:28):

pip3 install mathlibtools should work similarly well (on some python 3.10 install)? worth trying if you can :/

Xin Huajian (Feb 25 2022 at 10:28):

OK, I'll try it, thanks!

Jason Rute (Feb 25 2022 at 11:51):

First, I think you have to use a special Brew for Rosetta2 as per the M1 specific guide https://leanprover-community.github.io/install/macos.html#m1-macs--apple-silicon

Jason Rute (Feb 25 2022 at 11:54):

Also, I would look at #new members > M1 Macs: Installing the Lean 3 toolchain if you haven't already.

Julian Berman (Feb 25 2022 at 16:17):

For mathlibtools you don't need Intel brew (I use mathlibtools from normal ARM homebrew), so the above is.. quite odd

Julian Berman (Feb 25 2022 at 16:18):

Can you maybe try brew install homebrew/core/mathlibtools just to be sure?

Xin Huajian (Feb 27 2022 at 06:55):

Hi, I installed usingpip3 install mathlibtools successfully, but when I tried to start lean in VS Code it outputted that dyld[46350]: Library not loaded: /usr/local/opt/gmp/lib/libgmp.10.dylib. Something seems still undone : (

Xin Huajian (Feb 27 2022 at 06:57):

Yes, I used the Brew for Rosetta2 as the guide but still received that problem.

Patrick Stevens (Feb 27 2022 at 08:15):

Xin Huajian said:

Hi, I installed usingpip3 install mathlibtools successfully, but when I tried to start lean in VS Code it outputted that dyld[46350]: Library not loaded: /usr/local/opt/gmp/lib/libgmp.10.dylib. Something seems still undone : (

Did you brew install gmp?

Xin Huajian (Jun 03 2022 at 13:11):

Finally I found the solution: https://leanprover-community.github.io/archive/stream/113489-new-members/topic/M1.20Macs.3A.20Installing.20the.20Lean.203.20toolchain.html

Julian Berman (Jun 03 2022 at 14:13):

Can you share what there helped solve your issue in the end?

Xin Huajian (Jun 05 2022 at 03:02):

Julian Berman said:

Can you share what there helped solve your issue in the end?

Now homebrew sopports the M1 chips, and the installing guide on "using Rosetta" seems to be not necessary. The problem that happened when I followed the guide was that the homebrew can't find mathlibtools, I guess it was caused by the incompatibility between x86-running window and the homebrew. Now I directly install homebrew without Rosetta and then I install elan and mathlibtools successfully.
However, there are also some new problems. Although homebrew, elan and mathlibtools support M1 chips, when I use leanproject command, it shows "error: binary package was not provided for 'darwin_aarch64'".
Still suffering.

Sebastian Ullrich (Jun 05 2022 at 11:42):

This is documented in the elan readme https://github.com/leanprover/elan#manual-installation

Xin Huajian (Jul 13 2022 at 00:58):

Sebastian Ullrich said:

This is documented in the elan readme https://github.com/leanprover/elan#manual-installation

Thanks! I finally find the way to install elan and mathlibtools:

  1. follow https://github.com/leanprover/elan#manual-installation to install elan
  2. install mathlibtools by elan:
elan toolchain install stable
elan default stable
  1. try to use leanproject new myproject, then I found the error Library not loaded: /usr/local/opt/gmp/lib/libgmp.10.dylib. My solution is that: within arch -x86_64 zsh, following https://stackoverflow.com/questions/12852228/installing-gmp-on-macos-x-with-xcode to install gmp in /usr/local/bin instead of /opt/local/bin(where the gmp is if install directly). Then try leanproject new myproject again and then the new project is created. In VSCode, there are no "leanpkg path" error.

Bolton Bailey (Jul 29 2022 at 18:53):

My fried is trying to install lean on M1 mac, following the instructions, he gets this error:

paulgafni@Pauls-MacBook-Air ~ % xcode-select --install
xcode-select: error: command line tools are already installed, use "Software Update" to install updates
paulgafni@Pauls-MacBook-Air ~ % softwareupdate --install-rosetta
I have read and agree to the terms of the software license agreement. A list of Apple SLAs may be found here: http://www.apple.com/legal/sla/
Type A and press return to agree: A
2022-07-29 11:50:49.025 softwareupdate[5082:2868074] Package Authoring Error: 002-42534: Package reference com.apple.pkg.RosettaUpdateAuto is missing installKBytes attribute
Install of Rosetta 2 finished successfully
paulgafni@Pauls-MacBook-Air ~ % arch -x86_64 zsh
arch: posix_spawnp: zsh: Bad CPU type in executable

What is going on?

Julian Berman (Jul 29 2022 at 19:30):

If that's succeeded and/or /usr/sbin/softwareupdate --install-rosetta --agree-to-license says Rosetta is installed already, Google seems to suggest that may mean the Rosetta install is corrupt and you'll have some fun deleting and reinstalling it: https://www.reddit.com/r/MacOS/comments/rq89is/rosetta_2_issues/i2zwy07/

Bolton Bailey (Sep 12 2022 at 21:33):

Just another question here, when he runs arch -x86_64 bash it seems to work fine. Should this work for the installation?

Dean Young (Sep 29 2022 at 22:03):

I've got an M1 mac and I'm trying to install mathlib, using the instructions here:

leanprover-community.github.io/get_started.html

Unfortunately, on steps 3 and 4 I get "error: binary package was not provided for 'darwin'".

https://leanprover-community.github.io/archive/stream/113488-general/topic/mathlib.20branches.html

Yaël Dillies (Sep 29 2022 at 22:04):

Did you try elan self update?

Yaël Dillies (Sep 29 2022 at 22:05):

If it doesn't work, try uninstalling elan (elan self uninstall) and reinstalling it.

Dean Young (Sep 29 2022 at 22:09):

I get this:

Dean Young (Sep 29 2022 at 22:09):

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

Yaël Dillies (Sep 29 2022 at 22:10):

Ah then try uninstalling it from brew, or whichever package manager you're using.

Mauricio Collares (Sep 29 2022 at 22:12):

Since you're on M1, remember to use /usr/local/bin/brew instead of just brew: /usr/local/bin/brew update and /usr/local/bin/brew install elan-init

Dean Young (Sep 29 2022 at 22:16):

Thanks very much for your time guys.

Yes I used brew for this.

Following Mauricio's suggestion still produces an error. Here's what I get:

Warning: Treating elan as a formula. For the cask, use homebrew/cask/elan
elan-init 1.4.1 is already installed but outdated (so it will be upgraded).
Error: Cannot install in Homebrew on ARM processor in Intel default prefix (/usr/local)!
Please create a new installation in /opt/homebrew using one of the
"Alternative Installs" from:
https://docs.brew.sh/Installation
You can migrate your previously installed formula list with:
brew bundle dump

I guess I'm going to create a new installation. Do you know the relevant commands?

Mauricio Collares (Sep 29 2022 at 22:18):

Can you try the same command I mentioned but inside a Rosetta shell? That is, do arch -x86_64 zsh then use the resulting shell to update elan

Mauricio Collares (Sep 29 2022 at 22:18):

If that doesn't work, the installation instructions for M1 Mac are available at https://leanprover-community.github.io/install/macos.html

Dean Young (Sep 30 2022 at 23:11):

Mauricio Collares said:

Can you try the same command I mentioned but inside a Rosetta shell? That is, do arch -x86_64 zsh then use the resulting shell to update elan

Oh this worked, thanks so much Mauricio!


Last updated: Dec 20 2023 at 11:08 UTC