Installing mathlib on M1 Mac

Stream: general

[Xin Huajian]

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]

Maybe try brew update?

[Alexander Bentkamp]

What version of MacOS are you using?

[Xin Huajian]

I tried and it didn't work

[Xin Huajian]

macOS Monterey 12.2.1

[Eric Rodriguez]

can you put the output of the shell session?

[Xin Huajian]

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]

and this is after brew update?

[Xin Huajian]

Yes

[Eric Rodriguez]

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]

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

[Xin Huajian]

OK, I'll try it, thanks!

[Jason Rute]

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]

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

[Julian Berman]

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

[Julian Berman]

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

[Xin Huajian]

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]

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

[Patrick Stevens]

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]

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]

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

[Xin Huajian]

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]

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

[Xin Huajian]

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

3. 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]

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]

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]

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

[Dean Young]

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]

Did you try elan self update?

[Yaël Dillies]

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

[Dean Young]

I get this:

[Dean Young]

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]

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

[Mauricio Collares]

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]

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]

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]

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

[Dean Young]

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!