feat: CI: build linux_aarch64

.github/workflows/ci.yml

@@ -50,7 +50,7 @@ jobs:
             release: true
             shell: nix-shell --arg pkgsDist "import (fetchTarball \"channel:nixos-19.03\") {{}}" --run "bash -euxo pipefail {0}"
             llvm-url: https://github.com/leanprover/lean-llvm/releases/download/14.0.0/lean-llvm-x86_64-linux-gnu.tar.zst
-            prepare-llvm: script/prepare-llvm-linux.sh lean-llvm*
+            prepare-llvm: ../script/prepare-llvm-linux.sh lean-llvm*
             binary-check: ldd -v
           - name: Linux
             os: ubuntu-latest
@@ -71,7 +71,7 @@ jobs:
             shell: bash -euxo pipefail {0}
             CMAKE_OPTIONS: -DCMAKE_OSX_DEPLOYMENT_TARGET=10.15
             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*
+            prepare-llvm: ../script/prepare-llvm-macos.sh lean-llvm*
             binary-check: otool -L
           - name: Windows
             os: windows-2022
@@ -81,8 +81,16 @@ jobs:
             # for reasons unknown, interactivetests are flaky on Windows
             CTEST_OPTIONS: --repeat until-pass:2
             llvm-url: https://github.com/leanprover/lean-llvm/releases/download/14.0.0/lean-llvm-x86_64-w64-windows-gnu.tar.zst
-            prepare-llvm: script/prepare-llvm-mingw.sh lean-llvm*
+            prepare-llvm: ../script/prepare-llvm-mingw.sh lean-llvm*
             binary-check: ldd
+          - name: Linux aarch64
+            os: ubuntu-latest
+            CMAKE_OPTIONS: -DCMAKE_PREFIX_PATH=$GMP
+            release: true
+            cross: true
+            shell: nix-shell --arg pkgsDist "import (fetchTarball \"channel:nixos-19.03\") {{ localSystem.config = \"aarch64-unknown-linux-gnu\"; }}" --run "bash -euxo pipefail {0}"
+            llvm-url: https://github.com/leanprover/lean-llvm/releases/download/14.0.0/lean-llvm-x86_64-linux-gnu.tar.zst https://github.com/leanprover/lean-llvm/releases/download/14.0.0/lean-llvm-aarch64-linux-gnu.tar.zst
+            prepare-llvm: EXTRA_FLAGS=--target=aarch64-unknown-linux-gnu ../script/prepare-llvm-linux.sh lean-llvm-aarch64-* lean-llvm-x86_64-*
       # complete all jobs
       fail-fast: false
     name: ${{ matrix.name }}
@@ -134,7 +142,7 @@ jobs:
           cd build
           OPTIONS=()
           [[ -z '${{ matrix.llvm-url }}' ]] || wget -q ${{ matrix.llvm-url }}
-          [[ -z '${{ matrix.prepare-llvm }}' ]] || eval "OPTIONS+=($(../${{ matrix.prepare-llvm }}))"
+          [[ -z '${{ matrix.prepare-llvm }}' ]] || eval "OPTIONS+=($(${{ matrix.prepare-llvm }}))"
           if [[ -n '${{ matrix.release }}' && -n '${{ needs.set-nightly.outputs.nightly }}' ]]; then
             OPTIONS+=(-DLEAN_SPECIAL_VERSION_DESC=${{ needs.set-nightly.outputs.nightly }})
           fi
@@ -167,12 +175,15 @@ jobs:
       - name: Lean stats
         run: |
           build/stage1/bin/lean --stats src/Lean.lean
+        if: ${{ !matrix.cross }}
       - name: Test
         run: |
           cd build/stage1
           ctest -j4 --output-on-failure ${{ matrix.CTEST_OPTIONS }} < /dev/null
+        if: ${{ !matrix.cross }}
       - name: Check Test Binary
         run: ${{ matrix.binary-check }} tests/compiler/534.lean.out
+        if: ${{ !matrix.cross }}
       - name: Build Stage 2
         run: |
           cd build

script/prepare-llvm-linux.sh

@@ -9,6 +9,11 @@ set -uo pipefail
 # use full LLVM release for compiling C++ code, but subset for compiling C code and distribution
 
 [[ -d llvm ]] || (mkdir llvm; tar xf $1 --strip-components 1 --directory llvm)
+[[ -d llvm-host ]] || if [[ "$#" -gt 1 ]]; then
+  (mkdir llvm-host; tar xf $2 --strip-components 1 --directory llvm-host)
+else
+  ln -s llvm llvm-host
+fi
 mkdir -p stage1/{bin,lib,lib/glibc,include/clang}
 CP="cp -d"  # preserve symlinks
 # a C compiler!
@@ -34,9 +39,14 @@ $CP $GLIBC/lib/libc_nonshared.a stage1/lib/glibc
 for f in $GLIBC/lib/lib{c,dl,m,rt,pthread}-*; do b=$(basename $f); cp $f stage1/lib/glibc/${b%-*}.so; done
 OPTIONS=()
 echo -n " -DLEAN_STANDALONE=ON"
-echo -n " -DCMAKE_CXX_COMPILER=$PWD/llvm/bin/clang++ -DLEAN_CXX_STDLIB='-Wl,-Bstatic -lc++ -lc++abi -Wl,-Bdynamic'"
-echo -n " -DLEAN_EXTRA_CXX_FLAGS='--sysroot $PWD/llvm -idirafter $GLIBC_DEV/include'"
-echo -n " -DCMAKE_C_COMPILER=$PWD/stage1/bin/clang"
+echo -n " -DCMAKE_CXX_COMPILER=$PWD/llvm-host/bin/clang++ -DLEAN_CXX_STDLIB='-Wl,-Bstatic -lc++ -lc++abi -Wl,-Bdynamic'"
+echo -n " -DLEAN_EXTRA_CXX_FLAGS='--sysroot $PWD/llvm -idirafter $GLIBC_DEV/include ${EXTRA_FLAGS:-}'"
+# use target compiler directly when not cross-compiling
+if [[ -L llvm-host ]]; then
+  echo -n " -DCMAKE_C_COMPILER=$PWD/stage1/bin/clang"
+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:-}'"
+fi
 # use `-nostdinc` to make sure headers are not visible by default (in particular, not to `#include_next` in the clang headers),
 # but do not change sysroot so users can still link against system libs
 echo -n " -DLEANC_INTERNAL_FLAGS='-nostdinc -isystem ROOT/include/clang' -DLEANC_CC=ROOT/bin/clang"

src/CMakeLists.txt

@@ -544,7 +544,13 @@ set(CPACK_PACKAGE_VERSION "${LEAN_VERSION_STRING}.${COMPILE_DATETIME}")
 if(NOT (${GIT_SHA1} MATCHES ""))
   string(APPEND CPACK_PACKAGE_VERSION ".git${GIT_SHA1}")
 endif()
-set(CPACK_PACKAGE_FILE_NAME "lean-${LEAN_VERSION_STRING}-${LOWER_SYSTEM_NAME}")
+if (${CMAKE_SYSTEM_PROCESSOR} MATCHES "x86_64|AMD64")
+  # for compatibility with elan/previous releases
+  set(ARCH_SUFFIX "")
+else()
+  set(ARCH_SUFFIX "_${CMAKE_SYSTEM_PROCESSOR}")
+endif()
+set(CPACK_PACKAGE_FILE_NAME "lean-${LEAN_VERSION_STRING}-${LOWER_SYSTEM_NAME}${ARCH_SUFFIX}")
 if(${CMAKE_SYSTEM_NAME} MATCHES "Linux")
   SET(CPACK_GENERATOR TGZ)
 else()