Stream: new members
Topic: M1 macs
Jake Levinson (Feb 23 2021 at 01:44):
I just tried to install Lean after playing through the Natural Number Game, which I came across on hackernews yesterday. Compliments to Kevin and Mohammad for a very convincing introduction! (speaking as a mathematician here :smile:)
I'm on a recently-acquired M1 mac and was not able to install elan through the instructions at https://leanprover-community.github.io/get_started.html.
elan: unknown CPU type: arm64
(brew and leanproject installed just fine)
I am technically ignorant about M1 stuff and haven't yet had to use Rosetta for anything, so I'm not sure how to fix this or what to do instead. I saw some discussion up above about getting Lean to work on an M1 mac, but don't understand it. Anyone willing to help a newbie get set up?
Bryan Gin-ge Chen (Feb 23 2021 at 01:53):
Welcome! I think the issue is that
elan does not have binaries for
arm64 (yet?). Are M1 macs able to run binaries for intel macs? If so, then maybe the
apple-darwin file here will work: https://github.com/Kha/elan/releases/tag/v0.10.3
Bryan Gin-ge Chen (Feb 23 2021 at 01:55):
I haven't tried to install
elan manually before, but the instructions say just to run the file in a terminal after unpacking it.
Jake Levinson (Feb 23 2021 at 02:11):
Hi Bryan, thank you! Some progress now -- that installer seems to have worked and successfully installed elan. I've cloned the Lean tutorials.
New error message: looks like something else hasn't installed correctly (maybe
leanpkg?): VSCode appears to be running
leanpkg configure and getting this error:
dyld: Library not loaded: /usr/local/opt/gmp/lib/libgmp.10.dylib
Referenced from: /Users/jake/.elan/toolchains/leanprover-community-lean-3.26.0/bin/lean
Reason: image not found
Note -- I do have
gmp installed already via
brew install gmp.
Bryan Gin-ge Chen (Feb 23 2021 at 02:14):
leanpkg is just a
.lean script, so I think
lean is not able to find
gmp for some reason.
Bryan Gin-ge Chen (Feb 23 2021 at 02:16):
Is it possible that the
gmp you got from homebrew is an
arm64 version and not compatible with a program compiled for an intel mac? (I have no idea, just guessing wildly...)
Julian Berman (Feb 23 2021 at 02:17):
That'll be it yeah, paths to ARM things from homebrew will be in /opt/
Julian Berman (Feb 23 2021 at 02:22):
you can install an intel homebrew as well and then it'll get you an intel libgmp if you use that one instead, or you can also reasonably easily compile lean natively for ARM, there's just one
cmake arg you need which is https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/Apple.20Silicon/near/219305416
Bryan Gin-ge Chen (Feb 23 2021 at 02:34):
I suspect the former route might be easier for a new user; otherwise, if you want
leanproject to work then you'll have to make sure you compile Lean at the correct v3.26.0 commit and then recompile when we upgrade mathlib to a new version.
Jake Levinson (Feb 23 2021 at 04:22):
Your suggestions worked -- recording for posterity here in case anyone else reads this: it turned out I actually already had intel homebrew installed as well (presumably because my current macbook copied everything from my previous macbook automatically when I was first setting it up).
But, I had to actually call that version of homebrew directly to install x86 gmp, that is
/usr/local/Homebrew/bin/brew install gmp instead of
brew install gmp even though the command ran in a Rosetta terminal... I guess this makes sense but wasn't obvious to me at first!
And after fiddling a bit more, I appear to have the tutorials up and running in VSCode!
Thanks Bryan and Julian!
goals accomplished :tada:
Kevin Buzzard (Feb 23 2021 at 08:01):
Oh boy, thanks for persevering!
Bryan Gin-ge Chen (Feb 23 2021 at 16:56):
@Jake Levinson Glad you got things working! If you don't mind, can you try and recall all the steps you took so we can add some M1-specific instructions to our webpage?
Jake Levinson (Feb 23 2021 at 17:35):
This is going to be messy, haha. Maybe I should reinstall it all (homebrew, elan, lean, etc) from scratch now that I know how to get it working. The actual sequence involved a bunch of no doubt superfluous steps.
What I actually did was:
- (I had homebrew and
gitalready installed in both intel and arm64 versions, though I didn't realize I had both copies at first).
I ran the install command from [https://leanprover-community.github.io/install/macos.html] in Terminal:
/bin/bash -c "$(curl -fsSL https://raw.githubusercontent.com/leanprover-community/mathlib-tools/master/scripts/install_macos.sh)" && source ~/.profile
I followed these instructions [https://osxdaily.com/2020/11/18/how-run-homebrew-x86-terminal-apple-silicon-mac/] to make a duplicate Terminal that would run using Rosetta.
- I basically now reran a bunch of installers both terminals. Homebrew; the install command from Step 1; Bryan's suggested package for
brew install gmpand
brew install coreutils. (Some of these installers automatically declined to make a second copy of their installation.)
At this point I was able to copy the tutorial using
leanproject get tutorials. When I opened it in VSCode, it caused a bunch of "memory capacity exceeded" errors in the VSCode Infoview (I forget the exact error message, unfortunately). This stopped happening once I ran
leanproject build tutorials. I'm not sure if that was supposed to be necessary.
Still, lean was still not functional because it couldn't detect gmp.
- Finally I forced Homebrew to install the x86 gmp using Julian's suggestion. Specifically I went and found the intel Homebrew installed in
/usr/local/Homebrewand ran the gmp installer with it as
/usr/local/Homebrew/bin/brew install gmpinstead of
brew install gmp. (The latter command had been, I think, invoking
arm64Homebrew even if I ran it in the Rosetta Terminal.)
That seemed to do it!
(edit: Oh, there was more too. I think I ran some other commands like
pipx ensurepath and maybe related stuff in both terminals. Basically I was trying to do all the steps from https://leanprover-community.github.io/install/macos_details.html.)
If I have time this weekend I'll delete it all and try a fresh install.
Bryan Gin-ge Chen (Feb 23 2021 at 17:40):
Thanks Jake! This is already really helpful!
Bryan Gin-ge Chen (Feb 23 2021 at 17:41):
leanproject get tutorials should've made it unnecessary to run
leanproject build tutorials, as one of the things it does is to download the compiled files for the version of mathlib used in the tutorials. Not sure if the lack of
gmp somehow caused Lean to be unable to find them.
Last updated: May 14 2021 at 00:42 UTC