self-hosted M1 mac github actions runner

Stream: lean4

[Edward Ayers]

Hi has anyone looked into having a self-hosted github actions runner for Lean3 and Lean4 for native Apple M1 builds?

[Edward Ayers]

I guess the problem is that the architecture isn't supported by github actions runner yet https://docs.github.com/en/actions/hosting-your-own-runners/about-self-hosted-runners#supported-architectures-and-operating-systems-for-self-hosted-runners
Supporting this is tracked here https://github.com/actions/runner/issues/805

[Bryan Gin-ge Chen]

I think It was discussed a few times on Zulip (I'm only finding this thread atm though), but I don't know of anyone actually doing it yet. edit: and of course no one has done it because of the architecture not being supported, whoops.

[Sebastian Ullrich]

Good news, everyone!

[Xubai Wang]

It seems that these aarch64 builds are not packed into nightly release assets.
There are only lean-4.0.0-nightly-2022-03-26-linux.zip.
https://github.com/leanprover/lean4-nightly/releases/tag/nightly-2022-03-26

(Also I fail to install elan on android termux which is of aarch64-linux-android target due to openssl-sys issue. Does linux aarch64 build support android?)

[Sebastian Ullrich]

See https://github.com/leanprover/lean4-nightly/releases/tag/nightly-2022-03-27

[Sebastian Ullrich]

I don't know anything about Android

[Edward Ayers]

Does elan need to be updated to know about arm64? It seems that elan is installing the x86 version of nightly lean for me still.

[Julian Berman]

(@Xubai Wang FWIW I have no issues compiling Lean 4 from source in Termux, in case you haven't tried doing so.)

[Julian Berman]

Is there a plan to compile community Lean 3 for aarch64 mac now too? If so we can also send a PR to Homebrew to re-enable elan on ARM.

[Sebastian Ullrich]

Edward Ayers said:

Does elan need to be updated to know about arm64? It seems that elan is installing the x86 version of nightly lean for me still.

https://github.com/leanprover/elan/pull/67