Cross-compiled build for macOS/aarch64

[Kha]

This is our first platform released using USE_GMP=OFF, as sourcing libraries for foreign platforms from Homebrew is not nearly as simple as with Nix.

I haven't tested the artifact yet as the SSH connection to the Mac Mini in my office intermittently freezes even with caffeinate 😶 .

[alcides]

I report that the darwin arm64 works in my machine (mbp m1 max) for simple files. If you'd like, I can run more specific tests.

[Kha]

@alcides Thanks! The other interesting part would be native compilation, e.g. lake init hello; lake build; ./build/bin/hello

[alcides]

Yes, that small example also works, despite the (scary for beginners) warnings bellow:

 alcides@PowerBook.local  /Users/alcides/Desktop/TestArm   master ✘ ✭  lake build                             11:34:16 
> LEAN_PATH=./build/lib /Users/alcides/.elan/toolchains/leanprover--lean4---nightly-2022-03-27/bin/lean ././TestARm.lean -R ./. -o ./build/lib/TestARm.olean -i ./build/lib/TestARm.ilean -c ./build/ir/TestARm.c
> /Users/alcides/.elan/toolchains/leanprover--lean4---nightly-2022-03-27/bin/leanc -c -o ./build/ir/TestARm.o ./build/ir/TestARm.c -O3 -DNDEBUG
> LEAN_PATH=./build/lib /Users/alcides/.elan/toolchains/leanprover--lean4---nightly-2022-03-27/bin/lean ././Main.lean -R ./. -o ./build/lib/Main.olean -i ./build/lib/Main.ilean -c ./build/ir/Main.c
> /Users/alcides/.elan/toolchains/leanprover--lean4---nightly-2022-03-27/bin/leanc -c -o ./build/ir/Main.o ./build/ir/Main.c -O3 -DNDEBUG
> /Users/alcides/.elan/toolchains/leanprover--lean4---nightly-2022-03-27/bin/leanc -o ./build/bin/TestARm ./build/ir/Main.o ./build/ir/TestARm.o
error: ld64.lld: warning: /usr/lib/system/libsystem_kernel.dylib has version 12.3.0, which is newer than target minimum of 12.0.0
ld64.lld: warning: /usr/lib/system/libsystem_platform.dylib has version 12.3.0, which is newer than target minimum of 12.0.0
ld64.lld: warning: /usr/lib/system/libsystem_pthread.dylib has version 12.3.0, which is newer than target minimum of 12.0.0
``

I'm available to run other tests (and I'm around the zulip if that reduces noise around here).

[Kha]

Thanks, looks good then! I haven't really investigated where these warnings are coming from yet.