Zulip Chat Archive

Stream: general

Topic: Apple Silicon


view this post on Zulip Jason Rute (Oct 17 2020 at 10:46):

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

view this post on Zulip Kevin Buzzard (Oct 17 2020 at 10:49):

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

view this post on Zulip Mario Carneiro (Oct 17 2020 at 10:58):

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

view this post on Zulip Mario Carneiro (Oct 17 2020 at 10:59):

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

view this post on Zulip Gabriel Ebner (Oct 19 2020 at 07:40):

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.

view this post on Zulip Jason Rute (Oct 19 2020 at 11:58):

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.

view this post on Zulip Mario Carneiro (Oct 19 2020 at 12:02):

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

view this post on Zulip Mario Carneiro (Oct 19 2020 at 12:03):

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

view this post on Zulip Kevin Lacker (Oct 19 2020 at 17:07):

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

view this post on Zulip Jason Rute (Oct 19 2020 at 17:10):

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?

view this post on Zulip Jason Rute (Nov 03 2020 at 11:57):

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?

view this post on Zulip Alex Peattie (Nov 03 2020 at 12:03):

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)

view this post on Zulip Johan Commelin (Nov 13 2020 at 10:32):

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

view this post on Zulip Patrick Massot (Nov 13 2020 at 11:09):

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.

view this post on Zulip Filippo A. E. Nuccio (Nov 13 2020 at 11:10):

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)."

view this post on Zulip Patrick Massot (Nov 13 2020 at 11:11):

Yes, this is why I'm puzzled.

view this post on Zulip Patrick Massot (Nov 13 2020 at 11:12):

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.

view this post on Zulip Filippo A. E. Nuccio (Nov 13 2020 at 11:12):

I agree that it is very puzzling.

view this post on Zulip Riccardo Brasca (Nov 13 2020 at 11:32):

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)

view this post on Zulip Filippo A. E. Nuccio (Nov 13 2020 at 11:33):

Indeed! Never thought about it.

view this post on Zulip Jasmin Blanchette (Nov 13 2020 at 13:57):

Patrick Massot said:

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

We're lazy people with an eye for design.

view this post on Zulip Adam Topaz (Nov 13 2020 at 15:53):

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?

view this post on Zulip Johan Commelin (Nov 13 2020 at 15:54):

Yes, but will it be fast enough?

view this post on Zulip Adam Topaz (Nov 13 2020 at 15:55):

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

view this post on Zulip Adam Topaz (Nov 13 2020 at 15:55):

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

view this post on Zulip Adam Topaz (Nov 13 2020 at 15:59):

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

view this post on Zulip Adam Topaz (Nov 13 2020 at 16:00):

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

view this post on Zulip James Arthur (Nov 13 2020 at 16:09):

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.

view this post on Zulip Mario Carneiro (Nov 13 2020 at 16:10):

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

view this post on Zulip Adam Topaz (Nov 13 2020 at 16:11):

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

view this post on Zulip Adam Topaz (Nov 13 2020 at 16:11):

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

view this post on Zulip Adam Topaz (Nov 13 2020 at 16:14):

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

view this post on Zulip Mario Carneiro (Nov 13 2020 at 16:15):

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

view this post on Zulip Anne Baanen (Nov 13 2020 at 16:57):

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.

view this post on Zulip Adam Topaz (Nov 13 2020 at 23:21):

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

view this post on Zulip Chris B (Nov 14 2020 at 00:00):

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

view this post on Zulip Adam Topaz (Nov 14 2020 at 00:10):

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

view this post on Zulip Adam Topaz (Nov 14 2020 at 00:11):

But I also hear good things about system76

view this post on Zulip Kevin Lacker (Nov 14 2020 at 00:17):

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

view this post on Zulip Adam Topaz (Nov 14 2020 at 00:25):

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

view this post on Zulip Reid Barton (Nov 14 2020 at 00:28):

I have this laptop too and yes

view this post on Zulip Julian Berman (Nov 19 2020 at 23:10):

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

view this post on Zulip Kevin Lacker (Nov 19 2020 at 23:14):

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

view this post on Zulip Julian Berman (Nov 19 2020 at 23:17):

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

view this post on Zulip Jason Rute (Nov 19 2020 at 23:56):

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.

view this post on Zulip Jason Rute (Nov 19 2020 at 23:56):

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.

view this post on Zulip Jason Rute (Nov 19 2020 at 23:56):

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.

view this post on Zulip Jason Rute (Nov 20 2020 at 00:01):

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

view this post on Zulip Jason Rute (Nov 20 2020 at 00:16):

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.

view this post on Zulip Julian Berman (Nov 20 2020 at 00:33):

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.

view this post on Zulip Julian Berman (Nov 20 2020 at 00:37):

(OK yeah leanpkg test passes)

view this post on Zulip Julian Berman (Nov 20 2020 at 00:38):

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.

view this post on Zulip Yakov Pechersky (Nov 20 2020 at 01:11):

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

view this post on Zulip Jason Rute (Nov 20 2020 at 12:27):

@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?

view this post on Zulip Jason Rute (Nov 20 2020 at 12:34):

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.

view this post on Zulip Julian Berman (Nov 20 2020 at 14:33):

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

view this post on Zulip Julian Berman (Nov 20 2020 at 14:34):

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

view this post on Zulip Julian Berman (Nov 20 2020 at 14:37):

(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 :)

view this post on Zulip Julian Berman (Nov 20 2020 at 15:09):

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

view this post on Zulip Julian Berman (Nov 20 2020 at 15:11):

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

view this post on Zulip Kevin Lacker (Dec 03 2020 at 20:51):

how is M1 performance looking?

view this post on Zulip Julian Berman (Dec 03 2020 at 21:20):

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

view this post on Zulip Julian Berman (Dec 03 2020 at 21:21):

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

view this post on Zulip Julian Berman (Dec 03 2020 at 21:21):

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

view this post on Zulip Sorawee Porncharoenwase (Dec 09 2020 at 07:48):

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.

view this post on Zulip Julian Berman (Dec 09 2020 at 13:26):

Nice! Glad to hear

view this post on Zulip Brandon Brown (Dec 09 2020 at 16:21):

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.

view this post on Zulip Sorawee Porncharoenwase (Jan 22 2021 at 21:36):

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.

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

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

view this post on Zulip Julian Berman (Feb 23 2021 at 03:11):

There's no M1 support in GitHub actions yet

view this post on Zulip Julian Berman (Feb 23 2021 at 03:11):

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

view this post on Zulip Julian Berman (Feb 23 2021 at 03:12):

Unless you mean Linux ARM64

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

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

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

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


Last updated: May 17 2021 at 22:15 UTC