mirror of
https://github.com/leanprover/lean4.git
synced 2026-03-17 18:34:06 +00:00
c1bcc4d1ac
This PR fixes a few warnings that were introduced by #12325, presumably because of an interaction with another PR.
267 lines
10 KiB
YAML
267 lines
10 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: ${{ endsWith(matrix.os, '-with-cache') && fromJSON(format('["{0}", "nscloud-git-mirror-1gb"]', matrix.os)) || 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=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.name == 'Linux Lake' && '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: Build
|
|
run: |
|
|
ulimit -c unlimited # coredumps
|
|
[ -d build ] || mkdir build
|
|
cd build
|
|
# arguments passed to `cmake`
|
|
OPTIONS=(-DLEAN_EXTRA_MAKE_OPTS=-DwarningAsError=true)
|
|
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 }})"
|
|
if [ "$TARGET_STAGE" == "stage2" ]; then
|
|
cp -r stage1 stage2
|
|
fi
|
|
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/..
|
|
time make $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.name == 'Linux Lake' && '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 }}
|
|
- 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@v2
|
|
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
|
|
# clean rebuild in case of Makefile changes/Lake does not detect uncommited stage 0
|
|
# changes yet
|
|
make -C build update-stage0
|
|
make -C build/stage1 clean-stdlib
|
|
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
|