From 83126883d941185aa53256dcf70798f16fb0d2ce Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Thu, 16 Oct 2025 22:27:02 +0200 Subject: [PATCH] chore: CI: overhaul check level logic (#10806) 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. --- .github/workflows/build-template.yml | 5 +-- .github/workflows/ci.yml | 49 +++++++++++++++------------- 2 files changed, 27 insertions(+), 27 deletions(-) diff --git a/.github/workflows/build-template.yml b/.github/workflows/build-template.yml index 79a5465250..f5e3f656ed 100644 --- a/.github/workflows/build-template.yml +++ b/.github/workflows/build-template.yml @@ -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: diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index f12c440628..9fbd811f64 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -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 }}