Zulip Chat Archive

Stream: new members

Topic: M1 macs


view this post on Zulip Jake Levinson (Feb 23 2021 at 01:44):

Hi all,

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.

Error message: 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?

Thanks!
-JL

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Bryan Gin-ge Chen (Feb 23 2021 at 02:14):

Hmm, leanpkg is just a .lean script, so I think lean is not able to find gmp for some reason.

view this post on Zulip 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...)

view this post on Zulip Julian Berman (Feb 23 2021 at 02:17):

That'll be it yeah, paths to ARM things from homebrew will be in /opt/

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Jake Levinson (Feb 23 2021 at 04:22):

Update:

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:

view this post on Zulip Kevin Buzzard (Feb 23 2021 at 08:01):

Oh boy, thanks for persevering!

view this post on Zulip 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?

view this post on Zulip 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:

  1. (I had homebrew and git already installed in both intel and arm64 versions, though I didn't realize I had both copies at first).
  2. 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

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

  4. I basically now reran a bunch of installers both terminals. Homebrew; the install command from Step 1; Bryan's suggested package for elan; VSCode; brew install gmp and 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.

  1. 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/Homebrew and ran the gmp installer with it as /usr/local/Homebrew/bin/brew install gmp instead of brew install gmp. (The latter command had been, I think, invoking arm64 Homebrew 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.

view this post on Zulip Bryan Gin-ge Chen (Feb 23 2021 at 17:40):

Thanks Jake! This is already really helpful!

view this post on Zulip Bryan Gin-ge Chen (Feb 23 2021 at 17:41):

I believe 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