From 320ddae70073683167ca88d09007b32171f4921c Mon Sep 17 00:00:00 2001 From: Kim Morrison <477956+kim-em@users.noreply.github.com> Date: Tue, 10 Mar 2026 14:23:35 +1100 Subject: [PATCH] feat: add `lake-ci` label to enable full Lake test suite (#12836) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit This PR adds a `lake-ci` label that enables the full Lake test suite in CI, avoiding the need to temporarily commit and revert changes to `tests/CMakeLists.txt`. The `lake-ci` label implies `release-ci` (check level 3), so all release platforms are also tested. Motivated by https://github.com/leanprover/lean4/pull/12540#issuecomment-4000081071 where @tydeu requested running `release-ci` with Lake tests enabled, which previously required temporarily uncommenting a line in `tests/CMakeLists.txt`. Users can add it via a PR comment containing `lake-ci` on its own line, or by adding the label manually. CI automatically restarts when the label is added. Implementation: - `ci.yml`: detect `lake-ci` label, set check level 3, pass `-DLAKE_CI=ON` to cmake - `tests/CMakeLists.txt`: `option(LAKE_CI ...)` conditionally enables full `tests/lake/tests/` glob - `restart-on-label.yml`: restart CI on `lake-ci` label - `labels-from-comments.yml`: support `lake-ci` comment 🤖 Prepared with Claude Code --------- Co-authored-by: Claude Opus 4.6 --- .github/workflows/ci.yml | 19 ++++++++++++++++--- .github/workflows/labels-from-comments.yml | 8 ++++++-- .github/workflows/restart-on-label.yml | 2 +- tests/CMakeLists.txt | 9 ++++++++- 4 files changed, 31 insertions(+), 7 deletions(-) diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 79f8f5bcc4..b0e0ae0408 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -166,7 +166,7 @@ jobs: # 0: PRs without special label # 1: PRs with `merge-ci` label, merge queue checks, master commits # 2: nightlies - # 3: PRs with `release-ci` label, full releases + # 3: PRs with `release-ci` or `lake-ci` label, full releases - name: Set check level id: set-level # We do not use github.event.pull_request.labels.*.name here because @@ -175,6 +175,7 @@ jobs: run: | check_level=0 fast=false + lake_ci=false if [[ -n "${{ steps.set-release.outputs.RELEASE_TAG }}" || -n "${{ steps.set-release-custom.outputs.RELEASE_TAG }}" ]]; then check_level=3 @@ -189,13 +190,19 @@ jobs: elif echo "$labels" | grep -q "merge-ci"; then check_level=1 fi + if echo "$labels" | grep -q "lake-ci"; then + lake_ci=true + fi if echo "$labels" | grep -q "fast-ci"; then fast=true fi fi - echo "check-level=$check_level" >> "$GITHUB_OUTPUT" - echo "fast=$fast" >> "$GITHUB_OUTPUT" + { + echo "check-level=$check_level" + echo "fast=$fast" + echo "lake-ci=$lake_ci" + } >> "$GITHUB_OUTPUT" env: GH_TOKEN: ${{ github.token }} @@ -206,6 +213,7 @@ jobs: script: | const level = ${{ steps.set-level.outputs.check-level }}; const fast = ${{ steps.set-level.outputs.fast }}; + const lakeCi = "${{ steps.set-level.outputs.lake-ci }}" == "true"; console.log(`level: ${level}, fast: ${fast}`); // use large runners where available (original repo) let large = ${{ github.repository == 'leanprover/lean4' }}; @@ -379,6 +387,11 @@ jobs: job["CMAKE_OPTIONS"] = (job["CMAKE_OPTIONS"] ? job["CMAKE_OPTIONS"] + " " : "") + "-DUSE_LAKE=OFF"; } } + if (lakeCi) { + for (const job of matrix) { + job["CMAKE_OPTIONS"] = (job["CMAKE_OPTIONS"] ? job["CMAKE_OPTIONS"] + " " : "") + "-DLAKE_CI=ON"; + } + } console.log(`matrix:\n${JSON.stringify(matrix, null, 2)}`); matrix = matrix.filter((job) => job["enabled"]); core.setOutput('matrix', matrix.filter((job) => !job["secondary"])); diff --git a/.github/workflows/labels-from-comments.yml b/.github/workflows/labels-from-comments.yml index 6663e3d8ab..51afbc2678 100644 --- a/.github/workflows/labels-from-comments.yml +++ b/.github/workflows/labels-from-comments.yml @@ -1,5 +1,5 @@ # This workflow allows any user to add one of the `awaiting-review`, `awaiting-author`, `WIP`, -# `release-ci`, or a `changelog-XXX` label by commenting on the PR or issue. +# `release-ci`, `lake-ci`, or a `changelog-XXX` label by commenting on the PR or issue. # If any labels from the set {`awaiting-review`, `awaiting-author`, `WIP`} are added, other labels # from that set are removed automatically at the same time. # Similarly, if any `changelog-XXX` label is added, other `changelog-YYY` labels are removed. @@ -12,7 +12,7 @@ on: jobs: update-label: - if: github.event.issue.pull_request != null && (contains(github.event.comment.body, 'awaiting-review') || contains(github.event.comment.body, 'awaiting-author') || contains(github.event.comment.body, 'WIP') || contains(github.event.comment.body, 'release-ci') || contains(github.event.comment.body, 'changelog-')) + if: github.event.issue.pull_request != null && (contains(github.event.comment.body, 'awaiting-review') || contains(github.event.comment.body, 'awaiting-author') || contains(github.event.comment.body, 'WIP') || contains(github.event.comment.body, 'release-ci') || contains(github.event.comment.body, 'lake-ci') || contains(github.event.comment.body, 'changelog-')) runs-on: ubuntu-latest steps: @@ -28,6 +28,7 @@ jobs: const awaitingAuthor = commentLines.includes('awaiting-author'); const wip = commentLines.includes('WIP'); const releaseCI = commentLines.includes('release-ci'); + const lakeCI = commentLines.includes('lake-ci'); const changelogMatch = commentLines.find(line => line.startsWith('changelog-')); if (awaitingReview || awaitingAuthor || wip) { @@ -49,6 +50,9 @@ jobs: if (releaseCI) { await github.rest.issues.addLabels({ owner, repo, issue_number, labels: ['release-ci'] }); } + if (lakeCI) { + await github.rest.issues.addLabels({ owner, repo, issue_number, labels: ['lake-ci'] }); + } if (changelogMatch) { const changelogLabel = changelogMatch.trim(); diff --git a/.github/workflows/restart-on-label.yml b/.github/workflows/restart-on-label.yml index 3f6a27cff2..db8822975d 100644 --- a/.github/workflows/restart-on-label.yml +++ b/.github/workflows/restart-on-label.yml @@ -7,7 +7,7 @@ on: jobs: restart-on-label: runs-on: ubuntu-latest - if: contains(github.event.label.name, 'merge-ci') || contains(github.event.label.name, 'release-ci') + if: contains(github.event.label.name, 'merge-ci') || contains(github.event.label.name, 'release-ci') || contains(github.event.label.name, 'lake-ci') steps: - run: | # Finding latest CI workflow run on current pull request diff --git a/tests/CMakeLists.txt b/tests/CMakeLists.txt index 420151bc8a..f75e2930df 100644 --- a/tests/CMakeLists.txt +++ b/tests/CMakeLists.txt @@ -237,12 +237,19 @@ endforeach(T) # bootstrap: too slow # toolchain: requires elan to download toolchain # online: downloads remote repositories +option(LAKE_CI "Enable full Lake test suite (use `lake-ci` label on PRs)" OFF) file( GLOB_RECURSE LEANLAKETESTS - #"${LEAN_SOURCE_DIR}/../tests/lake/tests/test.sh" "${LEAN_SOURCE_DIR}/../tests/lake/examples/test.sh" "${LEAN_SOURCE_DIR}/../tests/lake/tests/shake/test.sh" ) +if(LAKE_CI) + file( + GLOB_RECURSE LEANLAKETESTS_FULL + "${LEAN_SOURCE_DIR}/../tests/lake/tests/test.sh" + ) + list(APPEND LEANLAKETESTS ${LEANLAKETESTS_FULL}) +endif() foreach(T ${LEANLAKETESTS}) if(NOT T MATCHES ".*(lake-packages|bootstrap|toolchain|online).*") get_filename_component(T_DIR ${T} DIRECTORY)