From 7e853621eb3d5cbd4d8178884d95b126f803a077 Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Tue, 22 Mar 2022 17:27:20 +0100 Subject: [PATCH] feat: CI: build linux_aarch64 --- .github/workflows/ci.yml | 19 +++++++++++++++---- script/prepare-llvm-linux.sh | 16 +++++++++++++--- src/CMakeLists.txt | 8 +++++++- 3 files changed, 35 insertions(+), 8 deletions(-) diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index eb56057e34..fae57fb55c 100644 --- a/.github/workflows/ci.yml +++ b/.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 diff --git a/script/prepare-llvm-linux.sh b/script/prepare-llvm-linux.sh index a261d3eac2..9eb0ece0f9 100755 --- a/script/prepare-llvm-linux.sh +++ b/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" diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index f75f8adf63..2437fc711a 100644 --- a/src/CMakeLists.txt +++ b/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()