feat: CI: build darwin_aarch64

.github/workflows/ci.yml

@@ -73,6 +73,15 @@ jobs:
             llvm-url: https://github.com/leanprover/lean-llvm/releases/download/14.0.0/lean-llvm-x86_64-apple-darwin.tar.zst
             prepare-llvm: ../script/prepare-llvm-macos.sh lean-llvm*
             binary-check: otool -L
+          - name: macOS aarch64
+            os: macos-latest
+            release: true
+            cross: true
+            shell: bash -euxo pipefail {0}
+            CMAKE_OPTIONS: -DCMAKE_OSX_DEPLOYMENT_TARGET=10.15 -DUSE_GMP=OFF -DLEAN_INSTALL_SUFFIX=-darwin_aarch64
+            llvm-url: https://github.com/leanprover/lean-llvm/releases/download/14.0.0/lean-llvm-aarch64-apple-darwin.tar.zst https://github.com/leanprover/lean-llvm/releases/download/14.0.0/lean-llvm-x86_64-apple-darwin.tar.zst
+            prepare-llvm: EXTRA_FLAGS=--target=aarch64-apple-darwin ../script/prepare-llvm-macos.sh lean-llvm-aarch64-* lean-llvm-x86_64-*
+            binary-check: otool -L
           - name: Windows
             os: windows-2022
             release: true

RELEASES.md

@@ -1,9 +1,9 @@
 Unreleased
 ---------
 
-* [Added tutorial-like examples to our documentation](https://github.com/leanprover/lean4/tree/master/doc/examples). They will be soon rendered using LeanInk+Alectryon.
+* Add cross-compiled [aarch64 Linux](https://github.com/leanprover/lean4/pull/1066) and [aarch64 macOS](https://github.com/leanprover/lean4/pull/1076) releases.
 
-* [Add cross-compiled aarch64 Linux releases](https://github.com/leanprover/lean4/pull/1066).
+* [Added tutorial-like examples to our documentation](https://github.com/leanprover/lean4/tree/master/doc/examples). They will be soon rendered using LeanInk+Alectryon.
 
 v4.0.0-m4 (23 March 2022)
 ---------

doc/setup.md

@@ -16,12 +16,13 @@ Releases may be silently broken due to the lack of automated testing.
 Issue reports and fixes are welcome.
 
 * aarch64 Linux with glibc 2.27+
+* aarch64 (M1) macOS
 
+<!--
 ### Tier 3
 
 Platforms that are known to work from manual testing, but do not come with CI or official releases
-
-* aarch64 (M1) macOS - may also [use x86-64 releases via Rosetta](https://github.com/leanprover/elan#manual-installation)
+-->
 
 # Setting Up Lean
 

script/prepare-llvm-macos.sh

@@ -8,7 +8,14 @@ set -uxo pipefail
 
 # use full LLVM release for compiling C++ code, but subset for compiling C code and distribution
 
+GMP=${GMP:-$(brew --prefix)}
+
 [[ -d llvm ]] || (mkdir llvm; gtar xf $1 --strip-components 1 --directory llvm)
+[[ -d llvm-host ]] || if [[ "$#" -gt 1 ]]; then
+  (mkdir llvm-host; gtar xf $2 --strip-components 1 --directory llvm-host)
+else
+  ln -s llvm llvm-host
+fi
 SDK=$(xcrun --show-sdk-path)
 mkdir -p stage1/{bin,lib/libc,include/clang}
 CP="gcp -d"  # preserve symlinks
@@ -25,7 +32,6 @@ $CP llvm/lib/lib{clang-cpp,LLVM}.dylib stage1/lib/
 $CP llvm/lib/clang/*/include/{std*,__std*,limits}.h stage1/include/clang
 # runtime
 (cd llvm; $CP --parents lib/clang/*/lib/*/libclang_rt.osx.a ../stage1)
-gcp ${GMP:-/usr/local/opt/gmp}/lib/libgmp.a stage1/lib/
 # libSystem stub, includes libc
 cp $SDK/usr/lib/libSystem.tbd stage1/lib/libc
 # use for linking, use system libs for running
@@ -33,9 +39,16 @@ gcp llvm/lib/lib{c++,c++abi,unwind}.dylib stage1/lib/libc
 echo -n " -DLEAN_STANDALONE=ON"
 # do not change C++ compiler; libc++ etc. being system libraries means there's no danger of conflicts,
 # and the custom clang++ outputs a myriad of warnings when consuming the SDK
-echo -n " -DCMAKE_C_COMPILER=$PWD/stage1/bin/clang"
-echo -n " -DGMP_LIBRARIES=lib/libgmp.a -DGMP_INCLUDE_DIR=/usr/local/opt/gmp/include"
+echo -n " -DLEAN_EXTRA_CXX_FLAGS='${EXTRA_FLAGS:-}'"
+if [[ -L llvm-host ]]; then
+  echo -n " -DCMAKE_C_COMPILER=$PWD/stage1/bin/clang"
+  gcp $GMP/lib/libgmp.a stage1/lib/
+  echo -n " -DLEANC_INTERNAL_LINKER_FLAGS='-L ROOT/lib -lgmp -L ROOT/lib/libc -fuse-ld=lld'"
+else
+  echo -n " -DCMAKE_C_COMPILER=$PWD/llvm-host/bin/clang -DLEANC_OPTS='--sysroot $PWD/stage1 -resource-dir $PWD/stage1/lib/clang/14.0.0 ${EXTRA_FLAGS:-}'"
+  echo -n " -DLEANC_INTERNAL_LINKER_FLAGS='-L ROOT/lib -L ROOT/lib/libc -fuse-ld=lld'"
+fi
+echo -n " -DGMP_LIBRARIES=lib/libgmp.a -DGMP_INCLUDE_DIR=$GMP/include"
 echo -n " -DLEANC_INTERNAL_FLAGS='-nostdinc -isystem ROOT/include/clang' -DLEANC_CC=ROOT/bin/clang"
-echo -n " -DLEANC_INTERNAL_LINKER_FLAGS='-L ROOT/lib -L ROOT/lib/libc -fuse-ld=lld'"
 # do not set `LEAN_CC` for tests
 echo -n " -DLEAN_TEST_VARS=''"