Zulip Chat Archive

Stream: general

Topic: Lean on M1 mac

Martin C. Martin (Dec 08 2021 at 15:35):

The thread for installing Lean on M1 macs is from February; it's kind of burried; and there are follow on comments which make me think some people encountered problems and tweaked it.

What's the status of compiling native M1 Lean, as opposed to emulating x86? Is it worth creating a wiki page or script with the steps?

Huỳnh Trần Khanh (Dec 08 2021 at 15:38):

you might want to check this out https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/M1.20Macs.3A.20Installing.20the.20Lean.203.20toolchain/near/262832039

Martin C. Martin (Dec 08 2021 at 15:39):

Thanks! I got the above link from the wiki page on installing on Mac, should that be updated?

Julian Berman (Dec 08 2021 at 15:49):

Are you specifically asking about native ARM Lean?

Julian Berman (Dec 08 2021 at 15:50):

Doing so works fine, I have been using it since the M1 came out, but yeah we still need pre-compiled M1 binaries for elan.

Julian Berman (Dec 08 2021 at 15:51):

There's I believe a ticket tracking that, but there's also this one https://github.com/leanprover-community/mathlib-tools/issues/107 for automating some of the suggestions in that thread

Julian Berman (Dec 08 2021 at 15:51):

A PR would definitely be appreciated I assume if you followed the steps and they worked for you (and if you're happy with one that installs x86 lean)

Martin C. Martin (Dec 08 2021 at 15:53):

Also, this does seem to install the x86 stuff, not the native ARM Lean.

Martin C. Martin (Dec 08 2021 at 15:58):

The brew install elan mathlibtools step is failing with:

martin@Martins-MacBook-Air ~ % brew install elan mathlibtools
elan toolchain install stable
elan default stable
Warning: Treating elan as a formula. For the cask, use homebrew/cask/elan
Warning: mathlibtools 1.1.0_2 is already installed and up-to-date.
To reinstall 1.1.0_2, run:
  brew reinstall mathlibtools
Error: Cannot install under Rosetta 2 in ARM default prefix (/opt/homebrew)!
To rerun under ARM use:
    arch -arm64 brew install ...
To install under x86_64, install Homebrew into /usr/local.

Julian Berman (Dec 08 2021 at 15:58):

That's using an ARM homebrew you have installed

Julian Berman (Dec 08 2021 at 15:58):

Do you have both installed already?

Julian Berman (Dec 08 2021 at 15:58):

Try /usr/local/bin/brew ... if so

Martin C. Martin (Dec 08 2021 at 16:07):

Thanks Julian, I got further!

Now I'm on:

  1. use leanproject get to get the repositories needed.

Which repositories do I need, and what are the commands I need to get them?

Julian Berman (Dec 08 2021 at 16:09):

Nice, glad to hear! I think the intention in that message is "whichever you were hoping to work with" -- are you hoping to work on/with mathlib perhaps?

Martin C. Martin (Dec 08 2021 at 16:15):

Thanks again. At this point, I'm working through Logic and Proof. There are some basic examples in Chapter 4. I'd like to use these as a way to start using Lean in VSCode. (Eventually I hope to contribute to mathlib.)

What more do I need to get Lean up and running in VS Code on my M1 Macbook Air?

Kevin Buzzard (Dec 08 2021 at 16:21):

Does Logic and Proof come with a github repository? If so, get that! If not, then get mathlib (leanproject get mathlib) and then make a new directory in that repository called my_experiments or whatever, and create Lean files in that. This way you will have access to all the mathlib imports. But for logic and proof you might not even need mathlib, in which case you can just make a new project with leanproject new and then make your own Lean files in src.

Patrick Stevens (Dec 08 2021 at 21:14):

FWIW I eventually got my Apple Silicon setup working with Nix as the package manager, building Lean 3 from source and using elan from nixpkgs - if anyone is interested I can write that up, although it's a pretty niche set of requirements :P

Alice Wyan (Dec 12 2021 at 16:47):

@Patrick Stevens I might be tempted to try it :) is it on macOS or linux?

Kevin Buzzard (Dec 12 2021 at 17:07):

The danger of having two distinct "here's how to install lean" instruction sets is that someone can try one, not get it working, give up and try the other one. Is there a danger that a novice trying both approaches and stopping at a random point in one list of instructions then switching to the other will end up with a borked system?

Julian Berman (Dec 12 2021 at 17:18):

Yes there is, in fact that's already the case with the few Zulip threads.

Julian Berman (Dec 12 2021 at 17:19):

(They have differing instructions from each other). So it's particularly good there's that PR now. And yeah personally I would definitely discourage new users from using Nix myself, but certainly sharing instructions for other Nix users wouldn't hurt.

Yaël Dillies (Dec 12 2021 at 17:21):

Nix, gets you addix.

Patrick Stevens (Dec 12 2021 at 18:06):

Alice Wyan said:

Patrick Stevens I might be tempted to try it :) is it on macOS or linux?

macOS, yep, specifically Apple Silicon. I haven't used Nix at all to do any of the building of lean3, just to get an environment.

Patrick Stevens (Dec 12 2021 at 18:07):

Any use of Nix should come with a very strong "don't try this unless you're very confident on the command line and with computers generally" :P

Alice Wyan (Dec 12 2021 at 18:19):

Patrick Stevens said:

macOS, yep, specifically Apple Silicon. I haven't used Nix at all to do any of the building of lean3, just to get an
environment.

I'm just unsure of which bits I need to get started... homebrew comes with lean and mathlibtool, would that be enough to play with the tutorials?

Patrick Stevens (Dec 12 2021 at 18:34):

(I'm just tidying up the Nix instructions and checking they reproduce now.)

To be clear, I use Nix to set up the build tools, I just don't use Nix to manage the building - that's still calling out to cmake and friends, which all live in the Nix store. If you don't already use Nix, or you're not on Apple silicon, I strongly recommend ignoring my instructions and going with the more official Homebrew-based ones instead (though you might find the Nix ones helpful if things go wrong, because they declare more precisely what needs to be true of your system to get Lean working).

Alice Wyan (Dec 12 2021 at 18:35):

Patrick Stevens said:
Then they might come in handy to check what's going on. I am on Apple Silicon and conversant in the CLI, but not familiar with nix.

Patrick Stevens (Dec 12 2021 at 19:07):

Instructions for Nix on Apple Silicon using home-manager and nix-darwin. These have gone through varying stages of readiness, so sorry if anything is in some kind of half-complete state, but I think these instructions are accurate. Hopefully they're beginner-friendly in the sense that unless you already know some Nix, the instructions will be completely impossible to even begin following.

Now you can build Mathlib! Clone it, and ~/.elan/toolchains/stable/bin/leanpkg build.

Eric Rodriguez (Dec 12 2021 at 19:11):

elan override may be a better way to do the last step, btw

Matthew Sottile (May 18 2022 at 22:56):

It looks like Github Actions now will have Apple Silicon support:

https://github.com/github/roadmap/issues/507
https://github.com/github/roadmap/issues/513

Does this mean we'll be able to get native M1 releases soon?

Julian Berman (May 19 2022 at 00:12):

For Lean 4 there already are native ARM binaries being built: https://github.com/leanprover/lean4-nightly/releases/tag/nightly-2022-05-18 I believe using some self-hosted hardware

Julian Berman (May 19 2022 at 00:14):

Probably this makes it easier to do that for Lean 3 community edition though which is obviously good

Sebastian Ullrich (May 19 2022 at 07:53):

Matthew Sottile said:

It looks like Github Actions now will have Apple Silicon support:

https://github.com/github/roadmap/issues/507
https://github.com/github/roadmap/issues/513

Does this mean we'll be able to get native M1 releases soon?

These don't seem to mention GitHub-hosted M1 runners.

I believe using some self-hosted hardware

Nope, it's cross-compiled. See https://leanprover.github.io/lean4/doc/setup.html#tier-2.

Last updated: Dec 20 2023 at 11:08 UTC