0a75e1d92f
If we're using the downloaded LLVM release and building stage2/stage3, we need to also copy stage1 to stage2/stage3 respectively before continuing the build. Previously, the CI did not do this in every case. Now we do it unconditionally because the overhead is small enough.
309 lines
13 KiB
YAML
309 lines
13 KiB
YAML
# instantiated by ci.yml
|
|
name: build-template
|
|
on:
|
|
workflow_call:
|
|
inputs:
|
|
config:
|
|
type: string
|
|
required: true
|
|
nightly:
|
|
type: string
|
|
required: true
|
|
LEAN_VERSION_MAJOR:
|
|
type: string
|
|
required: true
|
|
LEAN_VERSION_MINOR:
|
|
type: string
|
|
required: true
|
|
LEAN_VERSION_PATCH:
|
|
type: string
|
|
required: true
|
|
LEAN_SPECIAL_VERSION_DESC:
|
|
type: string
|
|
required: true
|
|
RELEASE_TAG:
|
|
type: string
|
|
required: true
|
|
|
|
jobs:
|
|
build:
|
|
if: github.event_name != 'schedule' || github.repository == 'leanprover/lean4'
|
|
strategy:
|
|
matrix:
|
|
include: ${{fromJson(inputs.config)}}
|
|
# complete all jobs
|
|
fail-fast: false
|
|
runs-on: ${{ matrix.os }}
|
|
defaults:
|
|
run:
|
|
shell: ${{ matrix.shell || 'nix develop -c bash -euxo pipefail {0}' }}
|
|
name: ${{ matrix.name }}
|
|
env:
|
|
# must be inside workspace
|
|
CCACHE_DIR: ${{ github.workspace }}/.ccache
|
|
CCACHE_COMPRESS: true
|
|
# current cache limit
|
|
CCACHE_MAXSIZE: 400M
|
|
# squelch error message about missing nixpkgs channel
|
|
NIX_BUILD_SHELL: bash
|
|
LSAN_OPTIONS: max_leaks=10
|
|
# somehow MinGW clang64 (or cmake?) defaults to `g++` even though it doesn't exist
|
|
CXX: c++
|
|
MACOSX_DEPLOYMENT_TARGET: 11.0
|
|
steps:
|
|
- name: Install Nix
|
|
uses: DeterminateSystems/nix-installer-action@main
|
|
if: runner.os == 'Linux' && !matrix.cmultilib
|
|
- name: Install MSYS2
|
|
uses: msys2/setup-msys2@v2
|
|
with:
|
|
msystem: clang64
|
|
# `:` means do not prefix with msystem
|
|
pacboy: "make: python: cmake clang ccache gmp libuv git: zip: unzip: diffutils: binutils: tree: zstd tar:"
|
|
if: runner.os == 'Windows'
|
|
- name: Install Brew Packages
|
|
run: |
|
|
brew install ccache tree zstd coreutils gmp libuv
|
|
if: runner.os == 'macOS'
|
|
- name: Checkout
|
|
uses: actions/checkout@v6
|
|
with:
|
|
# the default is to use a virtual merge commit between the PR and master: just use the PR
|
|
ref: ${{ github.event.pull_request.head.sha }}
|
|
- name: Open Nix shell once
|
|
run: true
|
|
if: runner.os == 'Linux'
|
|
# Do check out some CI-relevant files from virtual merge commit to accommodate CI changes on
|
|
# master (as the workflow files themselves are always taken from the merge)
|
|
# (needs to be after "Install *" to use the right shell)
|
|
- name: CI Merge Checkout
|
|
run: |
|
|
git fetch --depth=${{ matrix.name == 'Linux Lake (Cached)' && '10' || '1' }} origin ${{ github.sha }}
|
|
git checkout FETCH_HEAD flake.nix flake.lock script/prepare-* tests/elab/importStructure.lean
|
|
if: github.event_name == 'pull_request'
|
|
# (needs to be after "Checkout" so files don't get overridden)
|
|
- name: Setup emsdk
|
|
uses: mymindstorm/setup-emsdk@v14
|
|
with:
|
|
version: 3.1.44
|
|
actions-cache-folder: emsdk
|
|
if: matrix.wasm
|
|
- name: Install 32bit c libs
|
|
run: |
|
|
sudo dpkg --add-architecture i386
|
|
sudo apt-get update
|
|
sudo apt-get install -y gcc-multilib g++-multilib ccache libuv1-dev:i386 pkgconf:i386
|
|
if: matrix.cmultilib
|
|
- name: Restore Cache
|
|
id: restore-cache
|
|
uses: actions/cache/restore@v5
|
|
with:
|
|
# NOTE: must be in sync with `save` below and with `restore-cache` in `update-stage0.yml`
|
|
path: |
|
|
.ccache
|
|
${{ matrix.lake-actions-cache && 'build/stage1/**/*.trace
|
|
build/stage1/**/*.olean*
|
|
build/stage1/**/*.ilean
|
|
build/stage1/**/*.ir
|
|
build/stage1/**/*.c
|
|
build/stage1/**/*.c.o*' || '' }}
|
|
key: ${{ matrix.name }}-build-v4-${{ github.sha }}
|
|
# fall back to (latest) previous cache
|
|
restore-keys: |
|
|
${{ matrix.name }}-build-v4
|
|
# open nix-shell once for initial setup
|
|
- name: Setup
|
|
run: |
|
|
ccache --zero-stats
|
|
if: runner.os == 'Linux'
|
|
- name: Set up env
|
|
run: |
|
|
echo "NPROC=$(nproc 2>/dev/null || sysctl -n hw.logicalcpu 2>/dev/null || echo 4)" >> $GITHUB_ENV
|
|
if ! diff src/stdlib_flags.h stage0/src/stdlib_flags.h; then
|
|
echo "src/stdlib_flags.h and stage0/src/stdlib_flags.h differ, will test and pack stage 2"
|
|
echo "TARGET_STAGE=stage2" >> $GITHUB_ENV
|
|
else
|
|
echo "TARGET_STAGE=stage1" >> $GITHUB_ENV
|
|
fi
|
|
- name: Configure Build
|
|
run: |
|
|
ulimit -c unlimited # coredumps
|
|
[ -d build ] || mkdir build
|
|
cd build
|
|
# arguments passed to `cmake`
|
|
OPTIONS=(-DWFAIL=ON)
|
|
if [[ -n '${{ matrix.release }}' ]]; then
|
|
# this also enables githash embedding into stage 1 library, which prohibits reusing
|
|
# `.olean`s across commits, so we don't do it in the fast non-release CI
|
|
OPTIONS+=(-DCHECK_OLEAN_VERSION=ON)
|
|
fi
|
|
if [[ -n '${{ matrix.cross_target }}' ]]; then
|
|
# used by `prepare-llvm`
|
|
export EXTRA_FLAGS=--target=${{ matrix.cross_target }}
|
|
OPTIONS+=(-DLEAN_PLATFORM_TARGET=${{ matrix.cross_target }})
|
|
fi
|
|
if [[ -n '${{ matrix.prepare-llvm }}' ]]; then
|
|
wget -q ${{ matrix.llvm-url }}
|
|
PREPARE="$(${{ matrix.prepare-llvm }})"
|
|
cp -r stage1 stage2
|
|
cp -r stage1 stage3
|
|
eval "OPTIONS+=($PREPARE)"
|
|
fi
|
|
if [[ -n '${{ matrix.release }}' && -n '${{ inputs.nightly }}' ]]; then
|
|
OPTIONS+=(-DLEAN_SPECIAL_VERSION_DESC=${{ inputs.nightly }})
|
|
fi
|
|
if [[ -n '${{ matrix.release }}' && -n '${{ inputs.RELEASE_TAG }}' ]]; then
|
|
OPTIONS+=(-DLEAN_VERSION_MAJOR=${{ inputs.LEAN_VERSION_MAJOR }})
|
|
OPTIONS+=(-DLEAN_VERSION_MINOR=${{ inputs.LEAN_VERSION_MINOR }})
|
|
OPTIONS+=(-DLEAN_VERSION_PATCH=${{ inputs.LEAN_VERSION_PATCH }})
|
|
OPTIONS+=(-DLEAN_VERSION_IS_RELEASE=1)
|
|
OPTIONS+=(-DLEAN_SPECIAL_VERSION_DESC=${{ inputs.LEAN_SPECIAL_VERSION_DESC }})
|
|
fi
|
|
# contortion to support empty OPTIONS with old macOS bash
|
|
cmake .. --preset ${{ matrix.CMAKE_PRESET || 'release' }} -B . ${{ matrix.CMAKE_OPTIONS }} ${OPTIONS[@]+"${OPTIONS[@]}"} -DLEAN_INSTALL_PREFIX=$PWD/..
|
|
- name: Build Stage 0 & Configure Stage 1
|
|
run: |
|
|
ulimit -c unlimited # coredumps
|
|
time make -C build stage1-configure -j$NPROC
|
|
- name: Download Lake Cache
|
|
if: matrix.name == 'Linux Lake (Cached)'
|
|
run: |
|
|
cd src
|
|
../build/stage0/bin/lake cache get --repo=${{ github.repository }}
|
|
timeout-minutes: 20 # prevent excessive hanging from network issues
|
|
continue-on-error: true
|
|
- name: Build Target Stage
|
|
run: |
|
|
ulimit -c unlimited # coredumps
|
|
time make -C build $TARGET_STAGE -j$NPROC
|
|
# Should be done as early as possible and in particular *before* "Check rebootstrap" which
|
|
# changes the state of stage1/
|
|
- name: Save Cache
|
|
# Caching on cancellation created some mysterious issues perhaps related to improper build
|
|
# shutdown
|
|
if: steps.restore-cache.outputs.cache-hit != 'true' && !cancelled()
|
|
uses: actions/cache/save@v5
|
|
with:
|
|
# NOTE: must be in sync with `restore` above
|
|
path: |
|
|
.ccache
|
|
${{ matrix.lake-actions-cache && 'build/stage1/**/*.trace
|
|
build/stage1/**/*.olean*
|
|
build/stage1/**/*.ilean
|
|
build/stage1/**/*.ir
|
|
build/stage1/**/*.c
|
|
build/stage1/**/*.c.o*' || '' }}
|
|
key: ${{ steps.restore-cache.outputs.cache-primary-key }}
|
|
- id: upload-lake-cache
|
|
name: Upload Lake Cache
|
|
# Caching on cancellation created some mysterious issues perhaps related to improper build
|
|
# shutdown. Also, since this needs access to secrets, it cannot be run on forks.
|
|
if: matrix.name == 'Linux release' && !cancelled() && (github.event_name != 'pull_request' || github.event.pull_request.head.repo.full_name == github.repository)
|
|
run: |
|
|
curl --version
|
|
cd src
|
|
time ../build/stage0/bin/lake build -o ../build/lake-mappings.jsonl
|
|
time ../build/stage0/bin/lake cache put ../build/lake-mappings.jsonl --repo=${{ github.repository }}
|
|
env:
|
|
LAKE_CACHE_KEY: ${{ secrets.LAKE_CACHE_KEY }}
|
|
LAKE_CACHE_ARTIFACT_ENDPOINT: ${{ vars.LAKE_CACHE_ENDPOINT }}/a1
|
|
LAKE_CACHE_REVISION_ENDPOINT: ${{ vars.LAKE_CACHE_ENDPOINT }}/r1
|
|
timeout-minutes: 20 # prevent excessive hanging from network issues
|
|
continue-on-error: true
|
|
- name: Verify Lake Cache
|
|
if: steps.upload-lake-cache.outcome == 'success'
|
|
run: |
|
|
mv build/stage1/lib/lean build/stage1/lib/lean.bak
|
|
cd src
|
|
../build/stage0/bin/lake cache clean
|
|
../build/stage0/bin/lake cache get --repo=${{ github.repository }}
|
|
../build/stage0/bin/lake build --no-build
|
|
continue-on-error: true
|
|
- name: Restore Build
|
|
if: steps.upload-lake-cache.outcome == 'success'
|
|
run: |
|
|
rm -rf build/stage1/lib/lean
|
|
mv build/stage1/lib/lean.bak build/stage1/lib/lean
|
|
- name: Install
|
|
run: |
|
|
make -C build/$TARGET_STAGE install
|
|
- name: Check Binaries
|
|
run: ${{ matrix.binary-check }} lean-*/bin/* || true
|
|
- name: Count binary symbols
|
|
run: |
|
|
for f in lean-*/bin/*; do
|
|
echo "$f: $(nm $f | grep " T " | wc -l) exported symbols"
|
|
done
|
|
if: matrix.name == 'Windows'
|
|
- name: List Install Tree
|
|
run: |
|
|
# omit contents of Init/, ...
|
|
tree --du -h lean-*-* | grep -E ' (Init|Lean|Lake|LICENSE|[a-z])'
|
|
- name: Pack
|
|
run: |
|
|
dir=$(echo lean-*-*)
|
|
mkdir pack
|
|
# high-compression tar.zst + zip for release, fast tar.zst otherwise
|
|
if [[ '${{ startsWith(github.ref, 'refs/tags/') && matrix.release }}' == true || -n '${{ inputs.nightly }}' || -n '${{ inputs.RELEASE_TAG }}' ]]; then
|
|
${{ matrix.tar || 'tar' }} cf - $dir | zstd -T0 --no-progress -19 -o pack/$dir.tar.zst
|
|
zip -rq pack/$dir.zip $dir
|
|
else
|
|
${{ matrix.tar || 'tar' }} cf - $dir | zstd -T0 --no-progress -o pack/$dir.tar.zst
|
|
fi
|
|
- uses: actions/upload-artifact@v5
|
|
if: matrix.release
|
|
with:
|
|
name: build-${{ matrix.name }}
|
|
path: pack/*
|
|
- name: Lean stats
|
|
run: |
|
|
build/$TARGET_STAGE/bin/lean --stats src/Lean.lean
|
|
if: ${{ !matrix.cross }}
|
|
- name: Test
|
|
id: test
|
|
run: |
|
|
ulimit -c unlimited # coredumps
|
|
time ctest --preset ${{ matrix.CMAKE_PRESET || 'release' }} --test-dir build/$TARGET_STAGE -j$NPROC --output-junit test-results.xml ${{ matrix.CTEST_OPTIONS }}
|
|
if: matrix.test
|
|
- name: Test Summary
|
|
uses: test-summary/action@31493c76ec9e7aa675f1585d3ed6f1da69269a86 # v2.4
|
|
with:
|
|
paths: build/${{ env.TARGET_STAGE }}/test-results.xml
|
|
# prefix `if` above with `always` so it's run even if tests failed
|
|
if: always() && steps.test.conclusion != 'skipped'
|
|
- name: Check Test Binary
|
|
run: ${{ matrix.binary-check }} tests/compile/534.lean.out
|
|
if: (!matrix.cross) && steps.test.conclusion != 'skipped'
|
|
- name: Build Stage 2
|
|
run: |
|
|
make -C build -j$NPROC stage2
|
|
if: matrix.test-bench
|
|
- name: Check Stage 3
|
|
run: |
|
|
make -C build -j$NPROC check-stage3
|
|
if: matrix.check-stage3
|
|
- name: Test Benchmarks
|
|
run: |
|
|
cd tests
|
|
nix develop -c make -C ../build -j$NPROC bench
|
|
if: matrix.test-bench
|
|
- name: Check rebootstrap
|
|
run: |
|
|
set -e
|
|
git config user.email "stage0@lean-fro.org"
|
|
git config user.name "update-stage0"
|
|
make -C build update-stage0
|
|
git commit --allow-empty -m "chore: update-stage0"
|
|
time make -C build -j$NPROC
|
|
time ctest --preset ${{ matrix.CMAKE_PRESET || 'release' }} --test-dir build/stage1 -j$NPROC
|
|
if: matrix.check-rebootstrap
|
|
- name: CCache stats
|
|
if: always()
|
|
run: ccache -s
|
|
- name: Show stacktrace for coredumps
|
|
if: failure() && runner.os == 'Linux'
|
|
run: |
|
|
for c in $(find . -name core); do
|
|
progbin="$(file $c | sed "s/.*execfn: '\([^']*\)'.*/\1/")"
|
|
echo bt | $GDB/bin/gdb -q $progbin $c || true
|
|
done
|