max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore: CI: overhaul check level logic (#10806)

Browse source 
The logic was *still* wrong after two PRs so let's get rid of
`check-level` as a matrix entry and trust in simple bools.
This commit is contained in:
Sebastian Ullrich 2025-10-16 22:27:02 +02:00 • committed by GitHub
parent 5c7b003191
commit 83126883d9
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
2 changed files with 27 additions and 27 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

5
.github/workflows/build-template.yml vendored
View file

@ -3,9 +3,6 @@ name: build-template
on:
workflow_call:
inputs:
check-level:
type: string
required: true
config:
type: string
required: true
@ -230,7 +227,7 @@ jobs:
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.wasm || !matrix.cross) && (inputs.check-level >= 1 || matrix.test)
if: matrix.test
- name: Test Summary
uses: test-summary/action@v2
with:

49
.github/workflows/ci.yml vendored
View file

@ -31,10 +31,6 @@ jobs:
configure:
runs-on: ubuntu-latest
outputs:
# 0: PRs without special label
# 1: PRs with `merge-ci` label, merge queue checks, master commits
# 2: PRs with `release-ci` label, releases (incl. nightlies)
check-level: ${{ steps.set-level.outputs.check-level }}
# The build matrix, dynamically generated here
matrix: ${{ steps.set-matrix.outputs.matrix }}
# secondary build jobs that should not block the CI success/merge queue
@ -110,6 +106,9 @@ jobs:
TAG_NAME="${GITHUB_REF##*/}"
echo "RELEASE_TAG=$TAG_NAME" >> "$GITHUB_OUTPUT"
# 0: PRs without special label
# 1: PRs with `merge-ci` label, merge queue checks, master commits
# 2: PRs with `release-ci` label, releases (incl. nightlies)
- name: Set check level
id: set-level
# We do not use github.event.pull_request.labels.*.name here because
@ -152,7 +151,8 @@ jobs:
"name": "Linux LLVM",
"os": "ubuntu-latest",
"release": false,
"check-level": 2,
"enabled": level >= 2,
"test": true,
"shell": "nix develop .#oldGlibc -c bash -euxo pipefail {0}",
"llvm-url": "https://github.com/leanprover/lean-llvm/releases/download/19.1.2/lean-llvm-x86_64-linux-gnu.tar.zst",
"prepare-llvm": "../script/prepare-llvm-linux.sh lean-llvm*",
@ -168,14 +168,15 @@ jobs:
"os": "ubuntu-latest",
"release": true,
// Special handling for release jobs. We want:
// 1. To run it in PRs so developers get PR toolchains (so secondary is sufficient)
// 1. To run it in PRs so developers get PR toolchains (so secondary without tests is sufficient)
// 2. To skip it in merge queues as it takes longer than the
// Linux lake build and adds little value in the merge queue
// 3. To run it in release (obviously)
// 4. To run it for pushes to master so that pushes to master have a Linux toolchain
// available as an artifact for Grove to use.
"check-level": (isPr || isPushToMaster) ? 0 : 2,
"secondary": isPr,
"enabled": isPr || level != 1 || isPushToMaster,
"test": level >= 1,
"secondary": level == 0,
"shell": "nix develop .#oldGlibc -c bash -euxo pipefail {0}",
"llvm-url": "https://github.com/leanprover/lean-llvm/releases/download/19.1.2/lean-llvm-x86_64-linux-gnu.tar.zst",
"prepare-llvm": "../script/prepare-llvm-linux.sh lean-llvm*",
@ -186,10 +187,9 @@ jobs:
{
"name": "Linux Lake",
"os": large ? "nscloud-ubuntu-22.04-amd64-8x16-with-cache" : "ubuntu-latest",
"check-level": 0,
"enabled": true,
"check-rebootstrap": level >= 1,
"check-stage3": level >= 2,
// only check-level >= 1 opts into tests implicitly. TODO: Clean up this logic.
"test": true,
// NOTE: `test-speedcenter` currently seems to be broken on `ubuntu-latest`
"test-speedcenter": large && level >= 2,
@ -199,14 +199,16 @@ jobs:
{
"name": "Linux Reldebug",
"os": "ubuntu-latest",
"check-level": 2,
"enabled": level >= 2,
"test": true,
"CMAKE_PRESET": "reldebug",
},
// TODO: suddenly started failing in CI
/*{
"name": "Linux fsanitize",
"os": "ubuntu-latest",
"check-level": 2,
"enabled": level >= 2,
"test": true,
// turn off custom allocator & symbolic functions to make LSAN do its magic
"CMAKE_PRESET": "sanitize",
// exclude seriously slow/problematic tests (laketests crash)
@ -217,7 +219,7 @@ jobs:
"os": "macos-15-intel",
"release": true,
"test": false, // Tier 2 platform
"check-level": 2,
"enabled": level >= 2,
"shell": "bash -euxo pipefail {0}",
"llvm-url": "https://github.com/leanprover/lean-llvm/releases/download/19.1.2/lean-llvm-x86_64-apple-darwin.tar.zst",
"prepare-llvm": "../script/prepare-llvm-macos.sh lean-llvm*",
@ -228,23 +230,25 @@ jobs:
{
"name": "macOS aarch64",
// standard GH runner only comes with 7GB so use large runner if possible when running tests
"os": large && !isPr ? "nscloud-macos-sequoia-arm64-6x14" : "macos-15",
"os": large && level >= 1 ? "nscloud-macos-sequoia-arm64-6x14" : "macos-15",
"CMAKE_OPTIONS": "-DLEAN_INSTALL_SUFFIX=-darwin_aarch64",
"release": true,
"test": true,
"shell": "bash -euxo pipefail {0}",
"llvm-url": "https://github.com/leanprover/lean-llvm/releases/download/19.1.2/lean-llvm-aarch64-apple-darwin.tar.zst",
"prepare-llvm": "../script/prepare-llvm-macos.sh lean-llvm*",
"binary-check": "otool -L",
"tar": "gtar", // https://github.com/actions/runner-images/issues/2619
// See "Linux release" for release job levels; Grove is not a concern here
"check-level": isPr ? 0 : 2,
"secondary": isPr,
"enabled": isPr || level != 1,
"secondary": level == 0,
},
{
"name": "Windows",
"os": large && level == 2 ? "namespace-profile-windows-amd64-4x16" : "windows-2022",
"release": true,
"check-level": 2,
"enabled": level >= 2,
"test": true,
"shell": "msys2 {0}",
"CMAKE_OPTIONS": "-G \"Unix Makefiles\"",
"llvm-url": "https://github.com/leanprover/lean-llvm/releases/download/19.1.2/lean-llvm-x86_64-w64-windows-gnu.tar.zst",
@ -256,7 +260,8 @@ jobs:
"os": "nscloud-ubuntu-22.04-arm64-4x16",
"CMAKE_OPTIONS": "-DLEAN_INSTALL_SUFFIX=-linux_aarch64",
"release": true,
"check-level": 2,
"enabled": level >= 2,
"test": true,
"shell": "nix develop .#oldGlibcAArch -c bash -euxo pipefail {0}",
"llvm-url": "https://github.com/leanprover/lean-llvm/releases/download/19.1.2/lean-llvm-aarch64-linux-gnu.tar.zst",
"prepare-llvm": "../script/prepare-llvm-linux.sh lean-llvm*",
@ -269,7 +274,7 @@ jobs:
// "CMAKE_OPTIONS": "-DSTAGE0_USE_GMP=OFF -DSTAGE0_LEAN_EXTRA_CXX_FLAGS='-m32' -DSTAGE0_LEANC_OPTS='-m32' -DSTAGE0_MMAP=OFF -DUSE_GMP=OFF -DLEAN_EXTRA_CXX_FLAGS='-m32' -DLEANC_OPTS='-m32' -DMMAP=OFF -DLEAN_INSTALL_SUFFIX=-linux_x86 -DCMAKE_LIBRARY_PATH=/usr/lib/i386-linux-gnu/ -DSTAGE0_CMAKE_LIBRARY_PATH=/usr/lib/i386-linux-gnu/ -DPKG_CONFIG_EXECUTABLE=/usr/bin/i386-linux-gnu-pkg-config",
// "cmultilib": true,
// "release": true,
// "check-level": 2,
// "enabled": level >= 2,
// "cross": true,
// "shell": "bash -euxo pipefail {0}"
//}
@ -281,7 +286,7 @@ jobs:
// "wasm": true,
// "cmultilib": true,
// "release": true,
// "check-level": 2,
// "enabled": level >= 2,
// "cross": true,
// "shell": "bash -euxo pipefail {0}",
// // Just a few selected tests because wasm is slow
@ -295,7 +300,7 @@ jobs:
}
}
console.log(`matrix:\n${JSON.stringify(matrix, null, 2)}`);
matrix = matrix.filter((job) => level >= job["check-level"]);
matrix = matrix.filter((job) => job["enabled"]);
core.setOutput('matrix', matrix.filter((job) => !job["secondary"]));
core.setOutput('matrix-secondary', matrix.filter((job) => job["secondary"]));
@ -305,7 +310,6 @@ jobs:
uses: ./.github/workflows/build-template.yml
with:
config: ${{needs.configure.outputs.matrix}}
check-level: ${{ needs.configure.outputs.check-level }}
nightly: ${{ needs.configure.outputs.nightly }}
LEAN_VERSION_MAJOR: ${{ needs.configure.outputs.LEAN_VERSION_MAJOR }}
LEAN_VERSION_MINOR: ${{ needs.configure.outputs.LEAN_VERSION_MINOR }}
@ -321,7 +325,6 @@ jobs:
uses: ./.github/workflows/build-template.yml
with:
config: ${{needs.configure.outputs.matrix-secondary}}
check-level: ${{ needs.configure.outputs.check-level }}
nightly: ${{ needs.configure.outputs.nightly }}
LEAN_VERSION_MAJOR: ${{ needs.configure.outputs.LEAN_VERSION_MAJOR }}
LEAN_VERSION_MINOR: ${{ needs.configure.outputs.LEAN_VERSION_MINOR }}