Apple Silicon

Stream: general

[Jason Rute]

This might still be premature since it is another month or so until Apple will release its new Apple Silicon MacBooks using an ARM processor instead of an Intel processor. (I think the new OS is named Big Sur.) My question is simple: Will Lean 3 or 4 run on Apple Silicon Macs? From what I've read, the answer for other software seems to be complicated. (See here for the status of the most common homebrew formulas.) First, there is running natively vs. running in Rosetta which is something like an emulator for intel (x86_64) apps. Honestly, I'm mostly trowing out tech jargon without knowing what it means, especially what it means for Lean. It's even hard to know if VS Code (or Emacs) will be ready at launch time (but I think from Googling, they will be).

[Kevin Buzzard]

I've had lean running in a chrooted Ubuntu environment on a 2017 Android phone and it wouldn't surprise me if that had an ARM chip in, but I'm certainly no expert here

[Mario Carneiro]

I don't see any reason why not. Lean is written in C++ and there are C++ compilers for all the major ISAs and many ISAs no one cares about

[Mario Carneiro]

If the OS layer changes that might require more work, but switching from one supported ISA to another doesn't seem like a big problem

[Gabriel Ebner]

Lean 3 runs just fine on aarch64. I'm not invested in the Apple ecosystem so I don't know if "Apple silicon" is different.

[Jason Rute]

Ok. I think what I'm hearing is that if I (or someone else here) gets an Apple Silicon mac (rumored to be coming out in Nov 17), then if I compile from sources it should likely compile and run natively. And if not, it should be a relatively simple thing to support.

As for the elan binaries (which I assume are platform specific and for mac are currently for x86_64), they might work (maybe under Rosetta?) but we will have to see and compare the performance. If they don't work or there is a performance difference, then we can look into building a universal mac binary which supports both.

[Mario Carneiro]

I'm actually more worried about apple's signing conditions post-catalina. I don't think we have any signing setup, so I would assume that people have to go through some Gatekeeper (what a name!) workaround to be able to run lean today

[Mario Carneiro]

I don't really see a reason to ship fat binaries, they are basically two programs stapled together. The user only needs one of them

[Kevin Lacker]

you should be able to use software installed via homebrew without mucking around with signing, and homebrew plans on supporting apple silicon, so i would expect that to all work https://discourse.brew.sh/t/homebrew-and-apple-silicon/8837/2

[Jason Rute]

But Lean shouldn’t be installed via home brew, right? A new version comes out like event month. If elan is installed (and signed) via homebrew, will the elan installed lean binaries work?

[Jason Rute]

Just a note that the new line of macs will probably be announced next week and likely the Big Sur macOS with the code signing requirement Mario mentioned above will also be released soon. I'm mentioning because I'm considering buying a new mac (although I might wait for some reviews and discussion of what software works). Also, if anyone upgrades to Big Sur, it is not clear that Lean will work, because it's not signed. Is that what I'm understanding from the above discussion?

[Alex Peattie]

My understanding is that the new Macs will still run unsigned executables compiled for Intel processors, but won't run unsigned software compiled for Apple Silicon processors. (See the first addendum here)

[Johan Commelin]

To anyone interested in the concept Big Sur: https://sneak.berlin/20201112/your-computer-isnt-yours/

[Patrick Massot]

This is all very consistent with everything Apple has ever done. I don't see how one can have used MacOS in the past and pretend to care about this blogpost.

[Filippo A. E. Nuccio]

Well, apparently the author himself combines both options: "Now, it’s been possible up until today to block this sort of stuff on your Mac using a program called Little Snitch (really, the only thing keeping me using macOS at this point)."

[Patrick Massot]

Yes, this is why I'm puzzled.

[Patrick Massot]

But the psychology of MacOS users has always been mysterious to me. I even know someone who is a genuine anti-capitalist activist and uses a Mac.

[Filippo A. E. Nuccio]

I agree that it is very puzzling.

[Riccardo Brasca]

Yes, it's very strange... Filippo and Patrick, I am sure you too have colleagues that absolutely refuse to install stopcovid on their phone but are very happy about their mac... (my point is not to discuss pro and cons of stopcovid, just that these two different attitudes are very strange to me)

[Filippo A. E. Nuccio]

Indeed! Never thought about it.

[Jasmin Blanchette]

Patrick Massot said:

But the psychology of MacOS users has always been mysterious to me.

We're lazy people with an eye for design.

[Adam Topaz]

Johan Commelin said:

To anyone interested in the concept Big Sur: https://sneak.berlin/20201112/your-computer-isnt-yours/

Can lean run on a raspberry pi?

[Johan Commelin]

Yes, but will it be fast enough?

[Adam Topaz]

Maybe the new raspberry pi 4? (I don't have one, just wondering)

[Adam Topaz]

I mean, the raspberry pi 4 is supposed to be just as fast as the old thinkpad X220 I have somewhere in my desk drawer

[Adam Topaz]

I guess you won't even be able to install linux on the macs with the apple arm chips, right?

[Adam Topaz]

Man, that article is depressing. I thought apple was supposed to be the "pro privacy" company. What happened?!

[James Arthur]

Adam Topaz said:

Johan Commelin said:

To anyone interested in the concept Big Sur: https://sneak.berlin/20201112/your-computer-isnt-yours/

Can lean run on a raspberry pi?

Slowly, I tried this the other day. It's possible, but in comparison to my i7 laptop.

[Mario Carneiro]

Adam Topaz said:

Man, that article is depressing. I thought apple was supposed to be the "pro privacy" company. What happened?!

What? I've never seen anything from Apple that was pro-privacy

[Adam Topaz]

Well, at least ios is supposed to be more "private" than android, no?

[Adam Topaz]

Apple is supposedly anonymizing all the tracking data they collect on you, unlike google

[Adam Topaz]

But @Mario Carneiro , I agree, being more privacy conscious than google isn't saying too much.

[Mario Carneiro]

lol that's a funny way to spin "privacy"

[Anne Baanen]

Let's not forget that Google's most important business model is tracking user data, so promoting "privacy" is a good way for Apple to deny resources to their competition.

[Adam Topaz]

https://news.ycombinator.com/item?id=25086845

[Chris B]

Incredible. I hear system76 is making pretty good laptops nowadays, I might roll the dice when my macbook dies.

[Adam Topaz]

I have a not too fancy ThinkPad, running linux with perfect compatibility

[Adam Topaz]

But I also hear good things about system76

[Kevin Lacker]

i recommend the huawei matebook x pro, works great with ubuntu with a standard dual boot install process, no custom anything required

[Adam Topaz]

Is that the laptop with the pop-up webcam in the keyboard?

[Reid Barton]

I have this laptop too and yes

[Julian Berman]

Well, I'm now on ARM macOS. Do I win the lucky first prize to attempt to compile lean on ARM

[Kevin Lacker]

you win the prize once you paste a screen shot of either the error message you received, or a success message, into chat

[Julian Berman]

Hopefully the latter. (First need to install a bunch of deps.)

[Jason Rute]

Actually, I'd love if you try both with manually compiling natively AND using the usual MacOS install instructions via Rosetta 2 (elan+vscode+leanproject). My understanding is that you have to use either all Rosetta or all native apps in a tool chain so they play well together. It seems to me that if you did the Rosetta 2 install then everything would play together (python, git, vs code, and lean/elan) and lean would be sufficiently fast. Now, I don't have such a Mac, so you can tell me if I am wrong on that understanding and it is possible to mix and match.

[Jason Rute]

If you do the native install, is vs code (or emacs) ready for native apple silicon yet? Also if you get both a native and Rosetta install, I'd love to see the differences in times it takes to compile Mathlib.

[Jason Rute]

Of course, feel free to ignore all my requests, but we should think about how to handle the mac os instructions for users who are not as tech savvy as you.

[Jason Rute]

Also you probably know this already, but here is one way to install and run x86 apps in Rosetta 2.

[Jason Rute]

Also, this is probably the most insightful post I've found yet on data science tools (conda, tensorflow, etc) for Apple Silicon Macs. Unfortunately, the follow up article with the installation instructions got deleted. Hopefully he reposts it. I think the main point is that most everything works fine or more than fine under Rosetta 2 and many some things are ready for native while many things are quickly becoming ready. Obviously, this isn't about Lean, but might be useful to you.

[Julian Berman]

Thanks. I went (first) for the route of pain, as I tend to, so I've set up only a native-compiling homebrew to start. Which... lean works with! After brew install coreutils gmp and cmake -DCMAKE_PREFIX_PATH=/opt/homebrew/ ../../src in a lean repo checkout, I've got a working shell/lean which I just confirmed is at least functional enough to begin compiling my toy project, will give an all green when leanpkg test passes on it after it finishes compiling mathlib, since I haven't yet set up Python enough to run leanproject. But yeah seems promising so far.

[Julian Berman]

(OK yeah leanpkg test passes)

[Julian Berman]

That was quite a speedy mathlib compilation too though I just jumped 8 years forward to the future I guess, I was previously compiling on a 2012 MacBook Air.

[Yakov Pechersky]

It's going to turn out that really the M1 chip was optimized for M(athlib)

[Jason Rute]

@Julian Berman Thank you for posting these updates. I’m sure it will help whomever comes along next. As for vs code, are you going to run the current x86 version or the native insider build? If the current x86 version (through Rosetta 2), does it interact with a native Lean server without issue?

[Jason Rute]

Or did you compile Lean as a universal app? If so, would it then run fine under both native and x86 vs code? There are a lot of things I’m still trying to understand here.

[Julian Berman]

Of course! Happy to keep poking at things and sharing some results. I'll give vscode a shot after some coffee.

[Julian Berman]

I did not compile a universal app, just a pure ARM one.

[Julian Berman]

(I also have to finish attempting to compile PyPy today, which will likely be a 5-6 hour endeavor considering I don't have an ARM thing to bootstrap it with, so I may be splitting my attention/resources with that but yeah obviously happy to try Lean things that'd be helpful to report on :)

[Julian Berman]

OK yup vscode is working too (communicating with my arm64 lean)

[Julian Berman]

(Using a vscode gotten via brew cask install visual-studio-code, which looks like it's just the stable version from the vscode site)

[Kevin Lacker]

how is M1 performance looking?

[Julian Berman]

I haven't tested anything scientific. I'm happy to if you have anything you think is worthwhile.

[Julian Berman]

I guess I could say compile lean for rosetta and benchmark how long it takes to build mathlib on each

[Julian Berman]

Anecdotally I'd say I'm still quite happy overall.

[Sorawee Porncharoenwase]

I just got it working too! Thanks @Julian Berman for the "cmake -DCMAKE_PREFIX_PATH=/opt/homebrew/ ../../src" instruction. I would never have figured that out on my own.

[Julian Berman]

Nice! Glad to hear

[Brandon Brown]

Kevin Lacker said:

how is M1 performance looking?

I just got my Macbook Air M1 and I haven't yet attempted to use Lean on it yet but in general I'm very happy with it. All the intel-based apps work very smoothly through the Rosetta translation layer and noticeably faster than my previous intel Macbook Air.

[Sorawee Porncharoenwase]

FWIW, I attempted to upgrade Lean today, and somehow I now get an error ld: library not found for -lc++. Apparently I have to execute export LIBRARY_PATH="$LIBRARY_PATH:/Library/Developer/CommandLineTools/SDKs/MacOSX.sdk/usr/lib" before calling cmake.

[Bryan Gin-ge Chen]

If someone wants to help add an arm64 section to our compile and release scripts, that'd be greatly appreciated!

[Julian Berman]

There's no M1 support in GitHub actions yet

[Julian Berman]

Which is https://github.com/actions/virtual-environments/issues/2187

[Julian Berman]

Unless you mean Linux ARM64

[Bryan Gin-ge Chen]

Ah, OK. It's not possible to cross-compile for M1 Macs either then?

[Bryan Gin-ge Chen]

I guess we wouldn't be able to test the binary in CI, so maybe we should just wait.

[Jason Rute]

Apple is going to come out with the M1X MacBook Pros on Monday (or so it is widely believed). After that, almost all new Macs will be on the M-series/Apple Silicon/arm processors. I think as of right now, the current Apple Silicon instructions are basically "install from source and good luck" :smile:. I understand this has to do with technical issues with GitHub actions mentioned above (which I don't claim to understand). There is now a very detailed set of instructions in #new members > M1 Macs: Installing the Lean 3 toolchain. I wonder what incremental progress can be made here to make this easier for M1 and M1X users. I imaging a few lean users like me plan to buy an M1X MacBook Pro in the coming month. For example, if those instructions in #new members > M1 Macs: Installing the Lean 3 toolchain are solid, then we could put them on the website, no?

[Gabriel Ebner]

I think the proper solution would be to add ARM releases. Lean builds just fine on ARM, but github actions doesn't have free ARM build bots.

[Gabriel Ebner]

This would also be useful to our subcommunity of Raspberry Pi users.

[Jason Rute]

I've never quite understood this. Would an arm release (that say works on a Raspberry Pi) also work on an M1 mac?

[Gabriel Ebner]

There's Linux on ARM and then there's MacOS on ARM, the binaries are just as compatible as Linux/MacOS binaries are on AMD64. :smile: So no, they are not interchangeable. But it's the same kind of problem. And a problem that I think we should solve.

[Gabriel Ebner]

Does anybody know what the commercially available options are for build VMs on ARM? I know Amazon has Linux VMs. Can we rent a Mac build VM somewhere?

[Matthew Ballard]

In the meantime, I just ran through install instructions on M1 with Big Sur with elan v1.1.3-pre and can confirm I get the lean, leanpkg, and leanchecker installed.

[Jason Rute]

Another silly question: As for renting a "Mac build VM", do you need to rent an Apple Silicon mac in the cloud (e.g. a physical mac mini), or are there VMs for MacOS which run on (non-mac) ARM machines. (I for some reason thought it was the former, although I think I saw it is theoretically possible to build an Apple Silicon binary from an intel mac if it is running the newest MacOS.)

[Julian Berman]

MacStadium has them: https://www.macstadium.com/mac-mini -- but IIRC from having this discussion a few months ago with a different project, you can rent them, but the $$ might be pretty silly relative to buying one and putting it somewhere unless it's super mission critical that it be up 24/7, which for a buildbot just for releases may not be the case.

[Julian Berman]

Jason Rute said:

Another silly question: As for renting a "Mac build VM", do you need to rent an Apple Silicon mac in the cloud (e.g. a physical mac mini), or are there VMs for MacOS which run on (non-mac) ARM machines. (I for some reason thought it was the former, although I think I saw it is theoretically possible to build an Apple Silicon binary from an intel mac if it is running the newest MacOS.)

there aren't for non-mac, I think (but haven't looked recently) it's still against the Apple TOS to run macOS on non-mac hardware, so this tends to make commercial people scared.

[Matthew Ballard]

I think AWS has macos vms

[Julian Berman]

They're intel macs AFAIK: https://aws.amazon.com/ec2/instance-types/

[Matthew Ballard]

Ah shoot

[Jason Rute]

You can currently buy a refurbished 8GB Mac mini from Apple for $750. It might even be cheaper next week.

[Julian Berman]

Cheaper than that I think, the baseline one is $649 new

[Julian Berman]

Oh no that's the education store, the regular one for me says $699 -- https://www.apple.com/shop/buy-mac/mac-mini/apple-m1-chip-with-8-core-cpu-and-8-core-gpu-256gb -- which yeah if someone buys and runs in their basement obviously can be connected to GHA

[Matthew Ballard]

I think you can find someone who can purchase through that here

[Julian Berman]

Yeah, I'm sure most of us hah

[Matthew Ballard]

I also wonder if any institution has M1 hardware for general computing use?

[Julian Berman]

That might be a decent idea. Also it looks like MacStadium has an open source section: https://www.macstadium.com/opensource/members

[Julian Berman]

Which seems to include Haskell GHC and some other academic-y things

[Julian Berman]

Seems like it'd be worth a shot to ask them for access for free under that for Lean.

[Gabriel Ebner]

$130/month?!? That's quite steep, and buying it outright is cheaper after only a year or so. The Amazon VMs are $15/mo for comparison.

[Gabriel Ebner]

I think we could easily rent an ARM Linux VM from Amazon and hook it up as a runner for the lean/lean4 repos. @Sebastian Ullrich I believe you experimented with cross-compilation at some point. Did that work out, or should we get native build machines?

[Gabriel Ebner]

I have no idea what the best approach for the mac builds is.

[Sebastian Ullrich]

I will give it another try after landing the self-contained Zig/LLVM build, which is basically the same problem. I might take some dependencies from ARM Nixpkgs.

[Julian Berman]

Do you want me to look into contacting the open source part there? I'm happy to do so and CC one of you.

[Gabriel Ebner]

I'll defer to Sebastian if cross-compilation is possible instead, but if it isn't then please go ahead.

[Gabriel Ebner]

@Sebastian Ullrich What is your preferred way to support arm releases in elan? Elan currently appends only -linux.tar.gz, but not any architecture information. Should this be -linux-aarch64.tar.gz for arm and -linux.tar.gz for amd64?

[Sebastian Ullrich]

I think that makes the most sense, yes

[Gabriel Ebner]

Lean 3.34 now comes with Linux/aarch64 builds (cross-compiled on github actions). These work out of the box with elan (which also has a Linux/aarch64 release now).

[Gabriel Ebner]

The situation with Darwin/aarch64 is a bit more hairy because we can't cross compile them so we need an actual aarch64 machine. Of course, the github actions runner doesn't work on aarch64 macs yet: https://github.com/actions/runner/issues/805 But the issues describes some workarounds that we could use if we had such a machine.

[Gabriel Ebner]

I've tried the "cross compile on github actions" approach for Lean 4 as well. The tests pass, but it takes 90 minutes to build: https://github.com/gebner/lean4/runs/3941840303?check_suite_focus=true
(It's so slow because it's running the stage0 compiler is compiled for aaarch64 and running via CPU emulation. Otherwise the compiled Lean executable wouldn't recognize unicode syntax like ≤...)

[Gabriel Ebner]

So for Lean 4 we either need to set up a self-hosted runner for Linux/aarch64 (no technical issues) or get the zig cross-compilation PR working (and hope that it is faster).

[Sebastian Ullrich]

Gabriel Ebner said:

Otherwise the compiled Lean executable wouldn't recognize unicode syntax like ≤...

Wait, why is that?

[Sebastian Ullrich]

Are the .oleans different after all?

[Gabriel Ebner]

I have no idea. You can look at the build here: https://github.com/gebner/lean4/actions/runs/1359921109

[Sebastian Ullrich]

They do differ in a handful of bytes, very interesting

[Sebastian Ullrich]

Now how am I supposed to debug that :laughter_tears:

[Sebastian Ullrich]

@Gabriel Ebner Could you try running the working binary with the other olean files just to make sure?

[Gabriel Ebner]

All tests pass so it should work (except for tests involving leanc, which isn't set up for cross compilation). I've just tested it on an aarch64 vm, and the 3941840303 build compiles a working lake binary.

[Gabriel Ebner]

Oh sorry, I misunderstood you. I've now copied the oleans from the bad build the good build, and got this:

build@ip-172-30-0-147:~/lake$ ./build.sh
lean  -o "build/lib/Lake/Async.olean" --c="build/ir/Lake/Async.c.tmp" Lake/Async.lean
Lake/Async.lean:116:7: error: elaboration function for '«term_≤_»' has not been implemented

[Sebastian Ullrich]

Thanks, that narrows it down at the very least

[Gabriel Ebner]

I think I have solved (part of) the puzzle.

[Gabriel Ebner]

The String.hash function gives different results on aarch64 and amd64.

[Gabriel Ebner]

#eval "α".hash
-- 1281896824 on amd64
-- 3220031286 on aarch64

[Gabriel Ebner]

α contains characters whose byte value is greater than 128. :smile:

[Gabriel Ebner]

This was pretty obvious once I wrote an olean parser:

 diff -u (~/oleanparser/build/bin/oleanparser good/lib/lean/Init/Classical.olean | psub) (~/oleanparser/build/bin/oleanparser bad/lib/lean/Init/Classical.olean | psub)
--- /tmp/.psub.UC8YpPL3fz       2021-10-20 19:12:41.126207464 +0200
+++ /tmp/.psub.NKZ5f7HRrb       2021-10-20 19:12:41.148207390 +0200
@@ -554,7 +554,7 @@
 let x554 := Obj.constructor 1 #[x553, "proof_1"] [97, 226, 97, 203, 47, 251, 113, 117]
 let x555 := Obj.constructor 1 #[0, "u_1"] [237, 16, 194, 56, 135, 176, 85, 203]
 let x556 := Obj.constructor 1 #[x555, 0] []
-let x557 := Obj.constructor 1 #[0, "α"] [59, 122, 173, 22, 213, 44, 93, 185]
+let x557 := Obj.constructor 1 #[0, "α"] [191, 78, 70, 42, 51, 137, 215, 74]
 let x558 := Obj.constructor 4 #[x555] [157, 7, 234, 105, 2, 0, 0, 0]
 let x559 := Obj.constructor 3 #[x558] [25, 15, 82, 84, 8, 0, 0, 0]
 let x560 := Obj.constructor 1 #[0, "p"] [185, 187, 25, 190, 51, 234, 3, 115]
@@ -1476,7 +1476,7 @@
 let x1476 := Obj.constructor 5 #[x43, x1381] [36, 111, 226, 248, 0, 2, 0, 0]
 let x1477 := Obj.constructor 5 #[x1476, x924] [19, 101, 95, 177, 0, 3, 10, 0]
 let x1478 := Obj.constructor 5 #[x1477, x802] [110, 161, 111, 244, 0, 4, 10, 0]
-let x1479 := Obj.constructor 1 #[0, "h₀"] [249, 94, 105, 59, 215, 135, 180, 130]
+let x1479 := Obj.constructor 1 #[0, "h₀"] [149, 227, 157, 165, 5, 11, 91, 222]
 let x1480 := Obj.constructor 5 #[x1443, x32] [163, 255, 221, 250, 0, 1, 12, 0]
 let x1481 := Obj.constructor 6 #[x18, x567, x1480] [48, 151, 219, 119, 0, 2, 11, 0]
 let x1482 := Obj.constructor 5 #[x1403, x1481] [45, 65, 72, 178, 0, 3, 11, 0]
@@ -3420,7 +3420,7 @@
 let x3420 := Obj.constructor 0 #[x3419, 0, x484] []
 let x3421 := Obj.constructor 0 #[x3420, x333, 0] [0, 0, 0, 0, 0, 0, 0, 0]
 let x3422 := Obj.constructor 1 #[x3421] []
-let x3423 := Obj.constructor 1 #[0, "β"] [57, 91, 110, 179, 207, 81, 176, 247]
+let x3423 := Obj.constructor 1 #[0, "β"] [17, 104, 126, 98, 217, 137, 147, 75]
 let x3424 := Obj.constructor 2 #[x565, 876] [83, 146, 246, 209, 131, 147, 125, 157]
 let x3425 := Obj.constructor 7 #[x3424, x32, x675] [255, 14, 17, 220, 8, 1, 1, 0]
 let x3426 := Obj.constructor 1 #[0, "r"] [151, 224, 143, 155, 147, 185, 82, 85]

[Gabriel Ebner]

Apparently this was the only issue with stage0 as a cross-compiler. Is it ok if I make PR? @Sebastian Ullrich

[Sebastian Ullrich]

OMG, please do

[Sebastian Ullrich]

The parser sounds amazing

[Sebastian Ullrich]

Gabriel Ebner said:

Sebastian Ullrich What is your preferred way to support arm releases in elan? Elan currently appends only -linux.tar.gz, but not any architecture information. Should this be -linux-aarch64.tar.gz for arm and -linux.tar.gz for amd64?

For the future, we could avoid these issues by enforcing an elan self update before attempting to download a toolchain.

[Gabriel Ebner]

This won't work if you install elan via homebrew or nix.

[Johan Commelin]

Maybe it can output a warning whenever there is a new (major) release available?

[Johan Commelin]

Then people know that they should update their package