Steps to Install lean4 (with Vscode support) on a new M1 Mac

Stream: lean4

[Alcides Fonseca]

I wrote a simple instruction list to get lean4 running on a new macOS installation with VSCode: http://wiki.alcidesfonseca.com/blog/lean4-on-m1/

This gathers information from elsewhere (Mostly https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/M1.20Macs.3A.20Installing.20the.20Lean.203.20toolchain) and also deals with permission issues.

From what I understand the issue is that GitHub actions don't support M1 for the nightly build. Is there any chance where we this M1 build crowdsourced and placing it in a central server (I wouldn't mind doing an almost-daily build and uploading it)? I wouldn't mind doing this, even if it's for my own use.

[Sebastian Ullrich]

It is far easier to install elan without homebrew: https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/M1.20Macs.3A.20Installing.20the.20Lean.203.20toolchain/near/261663503

[Gabriel Ebner]

But that will install the emulated elan, right?

[Sebastian Ullrich]

Yes, but does that matter if Lean is emulated anyway?

[Gabriel Ebner]

Alcides' question is about actual M1 builds.

[Sebastian Ullrich]

leanprover/lean4:nightly should be an x86 release

[Gabriel Ebner]

I think we're talking about different things. It's well documented that you can install the emulated lean build with the emulated elan. But we should be setting up proper M1 builds at some point.

[Sebastian Ullrich]

Ok, sure. I was only talking about the simplest way to install Lean right now.

[Sebastian Ullrich]

I'd like to come back to cross compilation before the first release, I just haven't found the time yet

[Gabriel Ebner]

For linux/aarch64 it's straightforward to buy VMs and set up a custom runner if we don't want to bother with cross-compilation. Unfortunately macos/aarch64 doesn't have any reasonable cloud hosting and even if we had an M1 build machine, the github actions runner doesn't work out of the box (apparently both M1 and the latest macos release are unsupported). Last time I looked, cross-compilation from x86_64 to aarch64 was also uncharted territory.

[Sebastian Ullrich]

It seems to work fine for Zig, but it wouldn't be the first time that their approach didn't quite work out for us

[Sebastian Ullrich]

But I dearly hope that pure compilation & linking is completely independent of the host platform for a native cross compiler like LLVM. That leaves external dependencies, which we should already have covered.

[Gabriel Ebner]

I was mostly wondering about system libraries. I thought the x86_64 version of macos didn't ship with the arm builds.

[Sebastian Ullrich]

libSystem.tbd is all we need. I don't know if it is platform-dependent, but if so, we can copy it from an M1 machine once.

[Sebastian Ullrich]

In the meantime, I added a few words to the elan readme: https://github.com/leanprover/elan/pull/61

[Patrick Stevens]

By the way, I'm still gradually chipping away at getting a working lean4 setup on M1 with Nix, and it's looking very promising - as far as I can tell, it all Just Works except that I still have some hoops to jump through to teach the Lean VSCode plugin where to look, but I have successfully built mathlib4 locally using aarch64-darwin

[Patrick Stevens]

(yeah, native Nix on Darwin M1 does Just Work modulo sometimes having to reboot the machine because some part of Nix gets stuck in some way I haven't debugged - https://github.com/leanprover-community/mathlib4/compare/master...Smaug123:flake?expand=1 and nix run .#vscode-dev, given an ambient nix-darwin setup with the appropriate link to Lean https://github.com/Smaug123/nix-dotfiles/blob/main/home.nix#L74 and a nix build of https://github.com/leanprover/lean4 having been elan toolchain linked into the right place)

[Sebastian Ullrich]

Fair note: I haven't updated the vscode-lean4 version used by vscode-dev in ages because I wasn't aware of any users of it. Feel free to update.

[Patrick Stevens]

Cheers - I don't really have the free time to do anything with this stuff at the moment, but I bumped the extension for vscode-dev in https://github.com/leanprover/lean4/pull/1003/files just in case

[Sebastian Ullrich]

Now that I think about it, the main reason I didn't expect users regardless of the popularity of the Nix setup in general is that in contrast to emacs-dev, it does not allow you to install any additional extensions.

[Patrick Stevens]

Yeah, I was literally just thinking how to shoehorn vsvim in there

[Sebastian Ullrich]

The main issue is that VS Code has no concept of multi-layered configuration - https://github.com/microsoft/vscode/issues/27972