From 9f0df2a12862dc548c5ad286f54652c0ebde00d5 Mon Sep 17 00:00:00 2001 From: Vasily Ilin Date: Mon, 2 Nov 2026 23:47:19 -0800 Subject: [PATCH 1/3] Fix silent main build-cache save failures and cancel discarded queue runs Every main-branch "Save pool build" since 2026-10-16 failed because the runner ran out of disk while archiving .lake/build (52 MB free). The failure is only a warning, so runs stayed green while every PR, queue and main build kept restoring the 2026-10-16 cache and rebuilding weeks of changes (5,351 modules, ~3.5h for a one-project merge group). - Free ~25 GB of preinstalled toolchains before the build jobs. - Fail the run when the main build cache did not actually save. - Cancel merge-group runs whose queue ref GitHub already discarded, which happens after every out-of-queue push to main. Co-Authored-By: Claude Opus 5.5 --- .github/workflows/lean_action_ci.yml | 94 ++++++++++++++++++++++++++++ 1 file changed, 94 insertions(+) diff --git a/.github/workflows/lean_action_ci.yml b/.github/workflows/lean_action_ci.yml index 9911b4185a..3598c5539f 100644 --- a/.github/workflows/lean_action_ci.yml +++ b/.github/workflows/lean_action_ci.yml @@ -83,6 +83,9 @@ jobs: plan: runs-on: ubuntu-latest name: Plan build + permissions: + contents: read + actions: write outputs: build_revision: ${{ steps.build-identity.outputs.revision }} base_build_revision: ${{ steps.build-identity.outputs.base_revision }} @@ -98,6 +101,29 @@ jobs: with: fetch-depth: 0 + # A push to main outside the queue (such as the generated-metadata + # commit) makes GitHub rebuild every queued group, but the discarded + # groups' runs keep building for hours. Their refs are deleted, so + # cancel any queue run whose ref no longer exists. + - name: Cancel discarded merge-group runs + if: github.event_name == 'merge_group' + continue-on-error: true + env: + GH_TOKEN: ${{ github.token }} + run: | + set -uo pipefail + gh run list --repo "$GITHUB_REPOSITORY" --workflow lean_action_ci.yml \ + --event merge_group --limit 100 --json databaseId,status,headBranch \ + --jq '.[] | select(.status != "completed") | "\(.databaseId) \(.headBranch)"' | + while read -r run_id branch; do + [ "$run_id" = "$GITHUB_RUN_ID" ] && continue + status=$(gh api -i "repos/$GITHUB_REPOSITORY/git/ref/heads/$branch" 2>/dev/null | head -n 1 | awk '{print $2}') + if [ "$status" = 404 ]; then + echo "Cancelling run $run_id: merge group $branch was discarded." + gh run cancel "$run_id" --repo "$GITHUB_REPOSITORY" || true + fi + done + - name: Install Python tooling runtime uses: astral-sh/setup-uv@d0d8abe699bfb85fec6de9f7adb5ae17292296ff with: @@ -220,6 +246,15 @@ jobs: with: fetch-depth: 0 + # Restored caches plus the cache-save archive overflow the runner's + # default free space: every main build-cache save failed from + # 2026-10-16, so all runs rebuilt weeks of changes from a stale cache. + - name: Free runner disk space + run: | + sudo rm -rf /usr/share/dotnet /usr/local/lib/android /opt/ghc \ + /usr/local/.ghcup /opt/hostedtoolcache/CodeQL /usr/share/swift + df -h / + # Keep the large toolchain/Mathlib cache independent of per-commit builds. - name: Restore Lean dependencies id: dependency-cache @@ -449,12 +484,28 @@ jobs: key: LeanDependencies-v1-${{ runner.os }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json') }} - name: Save pool build + id: save-build if: always() && github.ref == 'refs/heads/main' && steps.compilation.outcome == 'success' && steps.cache.outputs.cache-hit != 'true' uses: actions/cache/save@27d5ce7f107fe9357f9df03efb73ab90386fccae with: path: .lake/build key: LeanPoolBuild-v1-${{ runner.os }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json', 'lakefile.toml') }}-${{ needs.plan.outputs.build_revision }} + # actions/cache only warns when a save fails; a missing main cache makes + # every later run rebuild from an older one, so fail loudly instead. + - name: Verify pool build cache + if: always() && steps.save-build.outcome == 'success' + env: + GH_TOKEN: ${{ github.token }} + KEY: LeanPoolBuild-v1-${{ runner.os }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json', 'lakefile.toml') }}-${{ needs.plan.outputs.build_revision }} + run: | + set -euo pipefail + saved=$(gh cache list --repo "$GITHUB_REPOSITORY" --key "$KEY" --json key --jq length) + if [ "$saved" = 0 ]; then + echo "::error::Pool build cache $KEY was not saved; later runs will rebuild from a stale cache." + exit 1 + fi + shard: needs: plan if: needs.plan.outputs.mode == 'sharded' @@ -473,6 +524,15 @@ jobs: with: fetch-depth: 0 + # Restored caches plus the cache-save archive overflow the runner's + # default free space: every main build-cache save failed from + # 2026-10-16, so all runs rebuilt weeks of changes from a stale cache. + - name: Free runner disk space + run: | + sudo rm -rf /usr/share/dotnet /usr/local/lib/android /opt/ghc \ + /usr/local/.ghcup /opt/hostedtoolcache/CodeQL /usr/share/swift + df -h / + - name: Restore Lean dependencies id: dependency-cache uses: actions/cache/restore@27d5ce7f107fe9357f9df03efb73ab90386fccae @@ -571,6 +631,15 @@ jobs: with: fetch-depth: 0 + # Restored caches plus the cache-save archive overflow the runner's + # default free space: every main build-cache save failed from + # 2026-10-16, so all runs rebuilt weeks of changes from a stale cache. + - name: Free runner disk space + run: | + sudo rm -rf /usr/share/dotnet /usr/local/lib/android /opt/ghc \ + /usr/local/.ghcup /opt/hostedtoolcache/CodeQL /usr/share/swift + df -h / + - name: Restore Lean dependencies id: dependency-cache uses: actions/cache/restore@27d5ce7f107fe9357f9df03efb73ab90386fccae @@ -803,12 +872,28 @@ jobs: key: LeanDependencies-v1-${{ runner.os }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json') }} - name: Save pool build + id: save-build if: always() && github.ref == 'refs/heads/main' && steps.compilation.outcome == 'success' && steps.cache.outputs.cache-hit != 'true' uses: actions/cache/save@27d5ce7f107fe9357f9df03efb73ab90386fccae with: path: .lake/build key: LeanPoolBuild-v1-${{ runner.os }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json', 'lakefile.toml') }}-${{ needs.plan.outputs.build_revision }} + # actions/cache only warns when a save fails; a missing main cache makes + # every later run rebuild from an older one, so fail loudly instead. + - name: Verify pool build cache + if: always() && steps.save-build.outcome == 'success' + env: + GH_TOKEN: ${{ github.token }} + KEY: LeanPoolBuild-v1-${{ runner.os }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json', 'lakefile.toml') }}-${{ needs.plan.outputs.build_revision }} + run: | + set -euo pipefail + saved=$(gh cache list --repo "$GITHUB_REPOSITORY" --key "$KEY" --json key --jq length) + if [ "$saved" = 0 ]; then + echo "::error::Pool build cache $KEY was not saved; later runs will rebuild from a stale cache." + exit 1 + fi + # Reuse the prior green project's compiled modules and current main's cache. # A missing artifact falls back to the full validation sequence in this job. rebase: @@ -822,6 +907,15 @@ jobs: with: fetch-depth: 0 + # Restored caches plus the cache-save archive overflow the runner's + # default free space: every main build-cache save failed from + # 2026-10-16, so all runs rebuilt weeks of changes from a stale cache. + - name: Free runner disk space + run: | + sudo rm -rf /usr/share/dotnet /usr/local/lib/android /opt/ghc \ + /usr/local/.ghcup /opt/hostedtoolcache/CodeQL /usr/share/swift + df -h / + - name: Restore Lean dependencies uses: actions/cache/restore@27d5ce7f107fe9357f9df03efb73ab90386fccae with: From 01b541f0d1bb1a8a1efcabec5505338e13581730 Mon Sep 17 00:00:00 2001 From: Vasily Ilin Date: Mon, 2 Nov 2026 23:55:04 -0800 Subject: [PATCH 2/3] Make discarded-run cancellation testable and prune the old build cache The inline cancel loop stopped at the first missing ref: GitHub runs steps with bash -e, so the failing lookup exited the loop (Greptile P1). Move the logic into lean_pool.merge_queue_cleanup, which treats only a definite 404 as missing and keeps scanning, with tests for a missing ref followed by more runs. Also prune the superseded build cache right after a verified main save, so two 6+ GB build copies never sit over the 10 GB repository cache limit and push out the dependency or docs caches. Co-Authored-By: Claude Opus 5.5 --- .github/workflows/lean_action_ci.yml | 28 +++--- python/lean_pool/merge_queue_cleanup.py | 105 +++++++++++++++++++++++ python/tests/test_merge_queue_cleanup.py | 84 ++++++++++++++++++ 3 files changed, 202 insertions(+), 15 deletions(-) create mode 100644 python/lean_pool/merge_queue_cleanup.py create mode 100644 python/tests/test_merge_queue_cleanup.py diff --git a/.github/workflows/lean_action_ci.yml b/.github/workflows/lean_action_ci.yml index 3598c5539f..94f31cb5bc 100644 --- a/.github/workflows/lean_action_ci.yml +++ b/.github/workflows/lean_action_ci.yml @@ -110,19 +110,9 @@ jobs: continue-on-error: true env: GH_TOKEN: ${{ github.token }} - run: | - set -uo pipefail - gh run list --repo "$GITHUB_REPOSITORY" --workflow lean_action_ci.yml \ - --event merge_group --limit 100 --json databaseId,status,headBranch \ - --jq '.[] | select(.status != "completed") | "\(.databaseId) \(.headBranch)"' | - while read -r run_id branch; do - [ "$run_id" = "$GITHUB_RUN_ID" ] && continue - status=$(gh api -i "repos/$GITHUB_REPOSITORY/git/ref/heads/$branch" 2>/dev/null | head -n 1 | awk '{print $2}') - if [ "$status" = 404 ]; then - echo "Cancelling run $run_id: merge group $branch was discarded." - gh run cancel "$run_id" --repo "$GITHUB_REPOSITORY" || true - fi - done + run: >- + PYTHONPATH=python python3 -m lean_pool.merge_queue_cleanup + --repository "$GITHUB_REPOSITORY" --current-run-id "$GITHUB_RUN_ID" - name: Install Python tooling runtime uses: astral-sh/setup-uv@d0d8abe699bfb85fec6de9f7adb5ae17292296ff @@ -493,7 +483,10 @@ jobs: # actions/cache only warns when a save fails; a missing main cache makes # every later run rebuild from an older one, so fail loudly instead. - - name: Verify pool build cache + # Then drop the superseded copy at once: two build copies plus the + # dependency cache exceed the 10 GB repository limit, and GitHub's + # eviction could otherwise drop the dependency or docs caches. + - name: Verify and prune pool build cache if: always() && steps.save-build.outcome == 'success' env: GH_TOKEN: ${{ github.token }} @@ -505,6 +498,7 @@ jobs: echo "::error::Pool build cache $KEY was not saved; later runs will rebuild from a stale cache." exit 1 fi + PYTHONPATH=python python3 -m lean_pool.ci_cache prune --repository "$GITHUB_REPOSITORY" --key "$KEY" shard: needs: plan @@ -881,7 +875,10 @@ jobs: # actions/cache only warns when a save fails; a missing main cache makes # every later run rebuild from an older one, so fail loudly instead. - - name: Verify pool build cache + # Then drop the superseded copy at once: two build copies plus the + # dependency cache exceed the 10 GB repository limit, and GitHub's + # eviction could otherwise drop the dependency or docs caches. + - name: Verify and prune pool build cache if: always() && steps.save-build.outcome == 'success' env: GH_TOKEN: ${{ github.token }} @@ -893,6 +890,7 @@ jobs: echo "::error::Pool build cache $KEY was not saved; later runs will rebuild from a stale cache." exit 1 fi + PYTHONPATH=python python3 -m lean_pool.ci_cache prune --repository "$GITHUB_REPOSITORY" --key "$KEY" # Reuse the prior green project's compiled modules and current main's cache. # A missing artifact falls back to the full validation sequence in this job. diff --git a/python/lean_pool/merge_queue_cleanup.py b/python/lean_pool/merge_queue_cleanup.py new file mode 100644 index 0000000000..aba26a319c --- /dev/null +++ b/python/lean_pool/merge_queue_cleanup.py @@ -0,0 +1,105 @@ +"""Cancel merge-queue CI runs whose queue entry GitHub has already discarded. + +A push to main from outside the queue makes GitHub rebuild every queued group +and delete the old groups' `gh-readonly-queue/...` refs, but runs started for +those refs keep building. A run whose ref no longer exists can never merge. +""" + +from __future__ import annotations + +import argparse +import json +import logging +import subprocess +from collections.abc import Callable +from typing import Any + +LOGGER = logging.getLogger(__name__) +WORKFLOW = "lean_action_ci.yml" + + +def discarded_runs( + runs: list[dict[str, Any]], + current_run_id: int, + branch_exists: Callable[[str], bool], +) -> list[int]: + """Select unfinished queue runs, other than this one, whose branch is gone.""" + return [ + run["databaseId"] + for run in runs + if run.get("status") != "completed" + and run.get("databaseId") != current_run_id + and str(run.get("headBranch", "")).startswith("gh-readonly-queue/") + and not branch_exists(run["headBranch"]) + ] + + +def branch_exists(repository: str, branch: str) -> bool: + """Report a branch as missing only on a definite 404, never on other errors.""" + result = subprocess.run( + ["gh", "api", f"repos/{repository}/git/ref/heads/{branch}"], + capture_output=True, + text=True, + timeout=60, + ) + if result.returncode == 0: + return True + if "HTTP 404" in result.stderr: + return False + LOGGER.warning("Could not look up %s: %s", branch, result.stderr.strip()) + return True + + +def queue_runs(repository: str) -> list[dict[str, Any]]: + """List recent merge-group runs of the Lean CI workflow.""" + output = subprocess.check_output( + [ + "gh", + "run", + "list", + "--repo", + repository, + "--workflow", + WORKFLOW, + "--event", + "merge_group", + "--limit", + "100", + "--json", + "databaseId,status,headBranch", + ], + text=True, + timeout=60, + ) + return json.loads(output) + + +def cancel_discarded(repository: str, current_run_id: int) -> list[int]: + """Cancel every discarded queue run and return the cancelled run IDs.""" + cancelled = discarded_runs( + queue_runs(repository), + current_run_id, + lambda branch: branch_exists(repository, branch), + ) + for run_id in cancelled: + LOGGER.info("Cancelling run %s: its merge group was discarded", run_id) + subprocess.run( + ["gh", "run", "cancel", str(run_id), "--repo", repository], + check=False, + timeout=60, + ) + return cancelled + + +def main() -> None: + """Cancel discarded merge-group runs for one repository.""" + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--repository", required=True) + parser.add_argument("--current-run-id", type=int, required=True) + arguments = parser.parse_args() + logging.basicConfig(level=logging.INFO, format="queue: %(message)s") + cancel_discarded(arguments.repository, arguments.current_run_id) + + +if __name__ == "__main__": + main() diff --git a/python/tests/test_merge_queue_cleanup.py b/python/tests/test_merge_queue_cleanup.py new file mode 100644 index 0000000000..67e9709e64 --- /dev/null +++ b/python/tests/test_merge_queue_cleanup.py @@ -0,0 +1,84 @@ +"""Check that only runs for discarded merge groups are cancelled.""" + +from __future__ import annotations + +import subprocess +from typing import Any + +import pytest + +from lean_pool import merge_queue_cleanup +from lean_pool.merge_queue_cleanup import ( + branch_exists, + cancel_discarded, + discarded_runs, +) + +LIVE = "gh-readonly-queue/main/pr-2-live" +GONE = "gh-readonly-queue/main/pr-1-gone" +ALSO_GONE = "gh-readonly-queue/main/pr-3-gone" + + +def _run(identifier: int, branch: str, status: str = "in_progress") -> dict[str, Any]: + return {"databaseId": identifier, "headBranch": branch, "status": status} + + +def test_every_missing_branch_is_selected_after_the_first() -> None: + """A missing ref must not stop the scan before later discarded runs.""" + runs = [_run(1, GONE), _run(2, LIVE), _run(3, ALSO_GONE)] + assert discarded_runs(runs, 99, lambda branch: branch == LIVE) == [1, 3] + + +def test_current_completed_and_non_queue_runs_are_kept() -> None: + """Never cancel this run, finished runs, or runs outside the queue.""" + runs = [ + _run(1, GONE), + _run(2, GONE, status="completed"), + _run(3, "feature/branch"), + ] + assert discarded_runs(runs, 1, lambda branch: False) == [] + + +@pytest.mark.parametrize( + ("returncode", "stderr", "expected"), + [ + (0, "", True), + (1, "gh: Not Found (HTTP 404)", False), + (1, "gh: Server Error (HTTP 502)", True), + ], +) +def test_only_a_definite_404_counts_as_missing( + monkeypatch: pytest.MonkeyPatch, returncode: int, stderr: str, expected: bool +) -> None: + """Transient API errors must not cancel a live queue run.""" + + def fake_run(*args: Any, **kwargs: Any) -> subprocess.CompletedProcess[str]: + return subprocess.CompletedProcess(args, returncode, "", stderr) + + monkeypatch.setattr(subprocess, "run", fake_run) + assert branch_exists("owner/repository", GONE) is expected + + +def test_cancel_discarded_cancels_each_missing_run( + monkeypatch: pytest.MonkeyPatch, +) -> None: + """Both discarded runs are cancelled even though the first lookup 404s.""" + cancelled: list[list[str]] = [] + monkeypatch.setattr( + merge_queue_cleanup, + "queue_runs", + lambda repository: [_run(1, GONE), _run(2, LIVE), _run(3, ALSO_GONE)], + ) + + def fake_run(command: list[str], **kwargs: Any) -> subprocess.CompletedProcess[str]: + if command[:2] == ["gh", "api"]: + missing = command[2].endswith(("-gone",)) + return subprocess.CompletedProcess( + command, 1 if missing else 0, "", "HTTP 404" if missing else "" + ) + cancelled.append(command) + return subprocess.CompletedProcess(command, 0, "", "") + + monkeypatch.setattr(subprocess, "run", fake_run) + assert cancel_discarded("owner/repository", 99) == [1, 3] + assert [command[3] for command in cancelled] == ["1", "3"] From abb701fe3396c8e4088f7372f732d1fbf3ba2942 Mon Sep 17 00:00:00 2001 From: Vasily Ilin Date: Mon, 2 Nov 2026 23:58:27 -0800 Subject: [PATCH 3/3] Leave build-cache pruning to the scheduled maintenance job #630 deliberately moved cache pruning off the build path into the hourly cache-maintenance workflow, and a contract test enforces that. Keep the save verification and drop the inline prune. Co-Authored-By: Claude Opus 5.5 --- .github/workflows/lean_action_ci.yml | 12 ++---------- 1 file changed, 2 insertions(+), 10 deletions(-) diff --git a/.github/workflows/lean_action_ci.yml b/.github/workflows/lean_action_ci.yml index 94f31cb5bc..8990a93522 100644 --- a/.github/workflows/lean_action_ci.yml +++ b/.github/workflows/lean_action_ci.yml @@ -483,10 +483,7 @@ jobs: # actions/cache only warns when a save fails; a missing main cache makes # every later run rebuild from an older one, so fail loudly instead. - # Then drop the superseded copy at once: two build copies plus the - # dependency cache exceed the 10 GB repository limit, and GitHub's - # eviction could otherwise drop the dependency or docs caches. - - name: Verify and prune pool build cache + - name: Verify pool build cache if: always() && steps.save-build.outcome == 'success' env: GH_TOKEN: ${{ github.token }} @@ -498,7 +495,6 @@ jobs: echo "::error::Pool build cache $KEY was not saved; later runs will rebuild from a stale cache." exit 1 fi - PYTHONPATH=python python3 -m lean_pool.ci_cache prune --repository "$GITHUB_REPOSITORY" --key "$KEY" shard: needs: plan @@ -875,10 +871,7 @@ jobs: # actions/cache only warns when a save fails; a missing main cache makes # every later run rebuild from an older one, so fail loudly instead. - # Then drop the superseded copy at once: two build copies plus the - # dependency cache exceed the 10 GB repository limit, and GitHub's - # eviction could otherwise drop the dependency or docs caches. - - name: Verify and prune pool build cache + - name: Verify pool build cache if: always() && steps.save-build.outcome == 'success' env: GH_TOKEN: ${{ github.token }} @@ -890,7 +883,6 @@ jobs: echo "::error::Pool build cache $KEY was not saved; later runs will rebuild from a stale cache." exit 1 fi - PYTHONPATH=python python3 -m lean_pool.ci_cache prune --repository "$GITHUB_REPOSITORY" --key "$KEY" # Reuse the prior green project's compiled modules and current main's cache. # A missing artifact falls back to the full validation sequence in this job.