From cb483c207ee02d6ec7ce805cba89576746370079 Mon Sep 17 00:00:00 2001 From: Vasily Ilin Date: Sat, 10 Oct 2026 04:11:13 +0000 Subject: [PATCH 1/4] Scope PR tooling checks and move maintenance off the build path --- .github/workflows/cache-maintenance.yml | 28 +++ .github/workflows/docs.yml | 72 +++--- .github/workflows/lean_action_ci.yml | 78 +------ .github/workflows/proof-profile-comment.yml | 11 +- .github/workflows/proof-profile.yml | 43 +--- .github/workflows/workflow_lint.yml | 50 ++++ python/lean_pool/ci_cache.py | 40 +++- python/tests/test_ci_cache.py | 74 +++++- python/tests/test_ci_cache_contract.py | 241 +++++++++++++++++++- 9 files changed, 485 insertions(+), 152 deletions(-) create mode 100644 .github/workflows/cache-maintenance.yml diff --git a/.github/workflows/cache-maintenance.yml b/.github/workflows/cache-maintenance.yml new file mode 100644 index 0000000000..311a50fe9e --- /dev/null +++ b/.github/workflows/cache-maintenance.yml @@ -0,0 +1,28 @@ +name: Cache maintenance + +on: + schedule: + - cron: '43 * * * *' + workflow_dispatch: + +permissions: + contents: read + actions: write + +concurrency: + group: cache-maintenance + cancel-in-progress: false + +jobs: + prune: + runs-on: ubuntu-latest + name: Prune superseded main caches + steps: + - uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd + with: + persist-credentials: false + - name: Retain the newest cache in each known family + env: + GH_TOKEN: ${{ github.token }} + REPOSITORY: ${{ github.repository }} + run: PYTHONPATH=python python3 -m lean_pool.ci_cache prune --repository "$REPOSITORY" diff --git a/.github/workflows/docs.yml b/.github/workflows/docs.yml index 24f02beda4..712d6dc5c6 100644 --- a/.github/workflows/docs.yml +++ b/.github/workflows/docs.yml @@ -46,10 +46,40 @@ permissions: actions: read jobs: + scope: + runs-on: ubuntu-latest + outputs: + applicable: ${{ steps.scope.outputs.applicable }} + steps: + - uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd + with: + fetch-depth: 0 + persist-credentials: false + - id: scope + env: + EVENT: ${{ github.event_name }} + BASE: ${{ github.event.merge_group.base_sha || github.event.pull_request.base.sha }} + run: | + set -euo pipefail + applicable=true + if [ "$EVENT" = merge_group ] || [ "$EVENT" = pull_request ]; then + applicable=false + if [ "$EVENT" = pull_request ]; then + files=$(git diff --name-only "$BASE"...HEAD) + else + files=$(git diff --name-only "$BASE"..HEAD) + fi + if grep -Eq '^(docbuild/|lean-toolchain$|lakefile\.toml$|lake-manifest\.json$|python/lean_pool/(exposition/|quality\.py$|validation_cache\.py$|ci_artifacts\.py$|ci_cache\.py$|rebase_fastpath\.py$)|python/(pyproject\.toml|uv\.lock)$|scripts/exposition/|\.github/workflows/docs\.yml$)' <<< "$files"; then + applicable=true + fi + fi + echo "applicable=$applicable" >> "$GITHUB_OUTPUT" # Fail cheap consistency checks before either multi-hour documentation job # starts. In particular, a stale generated root should not spend runner time # building documentation that cannot be merged. preflight: + needs: scope + if: always() && (needs.scope.result != 'success' || needs.scope.outputs.applicable != 'false') runs-on: ubuntu-latest name: Documentation preflight outputs: @@ -57,6 +87,15 @@ jobs: readme_only: ${{ steps.scope.outputs.readme_only }} rebase_only: ${{ steps.rebase.outputs.rebase_only }} steps: + - name: Require successful change classification + env: + SCOPE_RESULT: ${{ needs.scope.result }} + APPLICABLE: ${{ needs.scope.outputs.applicable }} + run: | + if [ "$SCOPE_RESULT" != success ] || [ "$APPLICABLE" != true ]; then + echo "::error::Change classification failed; required validation cannot be skipped." + exit 1 + fi - name: Checkout project uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd with: @@ -275,17 +314,6 @@ jobs: path: .lake/exposition-cache/v1 key: ${{ steps.extraction-cache.outputs.cache-primary-key }} - - name: Prune old copies of project extraction cache - if: always() && steps.extraction-cache-save.outcome == 'success' && github.ref == 'refs/heads/main' - continue-on-error: true - env: - GH_TOKEN: ${{ github.token }} - REPOSITORY: ${{ github.repository }} - CACHE_KEY: ${{ steps.extraction-cache.outputs.cache-primary-key }} - run: >- - PYTHONPATH=python python3 -m lean_pool.ci_cache prune - --repository "$REPOSITORY" --key "$CACHE_KEY" - - name: Upload extraction timings and logs if: always() uses: actions/upload-artifact@ea165f8d65b6e75b540449e92b4886f43607fa02 @@ -419,17 +447,6 @@ jobs: .lake/packages/MD4Lean key: DocsInfoMathlib-v3-${{ runner.os }}-${{ hashFiles('lean-toolchain', 'lakefile.toml', 'lake-manifest.json', 'docbuild/lean-toolchain', 'docbuild/lakefile.toml', 'docbuild/lake-manifest.json') }} - - name: Prune old copies of mathlib documentation checkpoint - if: steps.mathlib-doc-cache.outputs.cache-hit != 'true' && github.ref == 'refs/heads/main' - continue-on-error: true - env: - GH_TOKEN: ${{ github.token }} - REPOSITORY: ${{ github.repository }} - CACHE_KEY: DocsInfoMathlib-v3-${{ runner.os }}-${{ hashFiles('lean-toolchain', 'lakefile.toml', 'lake-manifest.json', 'docbuild/lean-toolchain', 'docbuild/lakefile.toml', 'docbuild/lake-manifest.json') }} - run: >- - PYTHONPATH=python python3 -m lean_pool.ci_cache prune - --repository "$REPOSITORY" --key "$CACHE_KEY" - build: needs: - preflight @@ -562,17 +579,6 @@ jobs: .lake/packages/MD4Lean key: DocsInfo-v3-${{ runner.os }}-${{ hashFiles('lean-toolchain', 'lakefile.toml', 'lake-manifest.json', 'docbuild/lean-toolchain', 'docbuild/lakefile.toml', 'docbuild/lake-manifest.json') }}-${{ needs.preflight.outputs.build_revision }} - - name: Prune old copies of pool documentation checkpoint - if: steps.pool-doc-cache.outputs.cache-hit != 'true' && github.ref == 'refs/heads/main' - continue-on-error: true - env: - GH_TOKEN: ${{ github.token }} - REPOSITORY: ${{ github.repository }} - CACHE_KEY: DocsInfo-v3-${{ runner.os }}-${{ hashFiles('lean-toolchain', 'lakefile.toml', 'lake-manifest.json', 'docbuild/lean-toolchain', 'docbuild/lakefile.toml', 'docbuild/lake-manifest.json') }}-${{ needs.preflight.outputs.build_revision }} - run: >- - PYTHONPATH=python python3 -m lean_pool.ci_cache prune - --repository "$REPOSITORY" --key "$CACHE_KEY" - - name: Build documentation run: cd docbuild && ~/.elan/bin/lake build LeanPool:docs diff --git a/.github/workflows/lean_action_ci.yml b/.github/workflows/lean_action_ci.yml index 1c82f0de20..dcdb00569a 100644 --- a/.github/workflows/lean_action_ci.yml +++ b/.github/workflows/lean_action_ci.yml @@ -87,6 +87,7 @@ jobs: build_revision: ${{ steps.build-identity.outputs.revision }} base_build_revision: ${{ steps.build-identity.outputs.base_revision }} minimal_build: ${{ steps.plan.outputs.minimal_build }} + dependency_tests: ${{ steps.plan.outputs.dependency_tests }} mode: ${{ steps.plan.outputs.mode }} matrix: ${{ steps.plan.outputs.matrix }} reuse_run_id: ${{ steps.plan.outputs.reuse_run_id }} @@ -168,6 +169,14 @@ jobs: minimal_build=true fi echo "minimal_build=$minimal_build" >> "$GITHUB_OUTPUT" + dependency_tests=true + if [ "$diff_available" = true ] && [ "$FORCE_FULL" != true ]; then + dependency_tests=false + if grep -Eq '^(lean-toolchain$|lakefile\.toml$|lake-manifest\.json$|python/|scripts/ci/|scripts/ProjectIndexes\.lean$|\.github/workflows/lean_action_ci\.yml$)' "$changed_files"; then + dependency_tests=true + fi + fi + echo "dependency_tests=$dependency_tests" >> "$GITHUB_OUTPUT" cold=false if [ -z "$CACHE_MATCHED" ]; then cold=true; fi plan=$(CHANGED_FILES_PATH="$changed_files" DIFF_AVAILABLE="$diff_available" \ @@ -242,6 +251,7 @@ jobs: enable-cache: true - name: Check compiled artifact dependency tracking with pinned Lean + if: needs.plan.outputs.dependency_tests == 'true' env: LEAN_POOL_REQUIRE_TEST_TOOLCHAIN: '1' run: >- @@ -428,17 +438,6 @@ jobs: path: .lake/validation-cache/v1 key: LeanValidation-v1-${{ runner.os }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json', 'lakefile.toml') }}-${{ github.sha }} - - name: Prune old copies of project validation - if: success() && github.ref == 'refs/heads/main' - continue-on-error: true - env: - GH_TOKEN: ${{ github.token }} - REPOSITORY: ${{ github.repository }} - CACHE_KEY: LeanValidation-v1-${{ runner.os }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json', 'lakefile.toml') }}-${{ github.sha }} - run: >- - PYTHONPATH=python python3 -m lean_pool.ci_cache prune - --repository "$REPOSITORY" --key "$CACHE_KEY" - - name: Save Lean dependencies if: always() && github.ref == 'refs/heads/main' && steps.mathlib-cache.outcome == 'success' && steps.dependency-cache.outputs.cache-hit != 'true' uses: actions/cache/save@27d5ce7f107fe9357f9df03efb73ab90386fccae @@ -448,17 +447,6 @@ jobs: .lake/packages key: LeanDependencies-v1-${{ runner.os }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json') }} - - name: Prune old copies of lean dependencies - if: always() && github.ref == 'refs/heads/main' && steps.mathlib-cache.outcome == 'success' && steps.dependency-cache.outputs.cache-hit != 'true' - continue-on-error: true - env: - GH_TOKEN: ${{ github.token }} - REPOSITORY: ${{ github.repository }} - CACHE_KEY: LeanDependencies-v1-${{ runner.os }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json') }} - run: >- - PYTHONPATH=python python3 -m lean_pool.ci_cache prune - --repository "$REPOSITORY" --key "$CACHE_KEY" - - name: Save pool build if: always() && github.ref == 'refs/heads/main' && steps.compilation.outcome == 'success' && steps.cache.outputs.cache-hit != 'true' uses: actions/cache/save@27d5ce7f107fe9357f9df03efb73ab90386fccae @@ -466,17 +454,6 @@ jobs: path: .lake/build key: LeanPoolBuild-v1-${{ runner.os }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json', 'lakefile.toml') }}-${{ needs.plan.outputs.build_revision }} - - name: Prune old copies of pool build - if: always() && github.ref == 'refs/heads/main' && steps.compilation.outcome == 'success' && steps.cache.outputs.cache-hit != 'true' - continue-on-error: true - env: - GH_TOKEN: ${{ github.token }} - REPOSITORY: ${{ github.repository }} - CACHE_KEY: LeanPoolBuild-v1-${{ runner.os }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json', 'lakefile.toml') }}-${{ needs.plan.outputs.build_revision }} - run: >- - PYTHONPATH=python python3 -m lean_pool.ci_cache prune - --repository "$REPOSITORY" --key "$CACHE_KEY" - shard: needs: plan if: needs.plan.outputs.mode == 'sharded' @@ -624,6 +601,7 @@ jobs: enable-cache: true - name: Check compiled artifact dependency tracking with pinned Lean + if: needs.plan.outputs.dependency_tests == 'true' env: LEAN_POOL_REQUIRE_TEST_TOOLCHAIN: '1' run: >- @@ -814,17 +792,6 @@ jobs: path: .lake/validation-cache/v1 key: LeanValidation-v1-${{ runner.os }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json', 'lakefile.toml') }}-${{ github.sha }} - - name: Prune old copies of project validation - if: success() && github.ref == 'refs/heads/main' - continue-on-error: true - env: - GH_TOKEN: ${{ github.token }} - REPOSITORY: ${{ github.repository }} - CACHE_KEY: LeanValidation-v1-${{ runner.os }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json', 'lakefile.toml') }}-${{ github.sha }} - run: >- - PYTHONPATH=python python3 -m lean_pool.ci_cache prune - --repository "$REPOSITORY" --key "$CACHE_KEY" - - name: Save Lean dependencies if: always() && github.ref == 'refs/heads/main' && steps.mathlib-cache.outcome == 'success' && steps.dependency-cache.outputs.cache-hit != 'true' uses: actions/cache/save@27d5ce7f107fe9357f9df03efb73ab90386fccae @@ -834,17 +801,6 @@ jobs: .lake/packages key: LeanDependencies-v1-${{ runner.os }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json') }} - - name: Prune old copies of lean dependencies - if: always() && github.ref == 'refs/heads/main' && steps.mathlib-cache.outcome == 'success' && steps.dependency-cache.outputs.cache-hit != 'true' - continue-on-error: true - env: - GH_TOKEN: ${{ github.token }} - REPOSITORY: ${{ github.repository }} - CACHE_KEY: LeanDependencies-v1-${{ runner.os }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json') }} - run: >- - PYTHONPATH=python python3 -m lean_pool.ci_cache prune - --repository "$REPOSITORY" --key "$CACHE_KEY" - - name: Save pool build if: always() && github.ref == 'refs/heads/main' && steps.compilation.outcome == 'success' && steps.cache.outputs.cache-hit != 'true' uses: actions/cache/save@27d5ce7f107fe9357f9df03efb73ab90386fccae @@ -854,17 +810,6 @@ jobs: # 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. - - name: Prune old copies of pool build - if: always() && github.ref == 'refs/heads/main' && steps.compilation.outcome == 'success' && steps.cache.outputs.cache-hit != 'true' - continue-on-error: true - env: - GH_TOKEN: ${{ github.token }} - REPOSITORY: ${{ github.repository }} - CACHE_KEY: LeanPoolBuild-v1-${{ runner.os }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json', 'lakefile.toml') }}-${{ needs.plan.outputs.build_revision }} - run: >- - PYTHONPATH=python python3 -m lean_pool.ci_cache prune - --repository "$REPOSITORY" --key "$CACHE_KEY" - rebase: needs: plan if: needs.plan.outputs.mode == 'rebase' @@ -930,6 +875,7 @@ jobs: use-mathlib-cache: false - name: Check compiled artifact dependency tracking with pinned Lean + if: needs.plan.outputs.dependency_tests == 'true' env: LEAN_POOL_REQUIRE_TEST_TOOLCHAIN: '1' run: >- diff --git a/.github/workflows/proof-profile-comment.yml b/.github/workflows/proof-profile-comment.yml index f05e0ac81d..ab72cccc11 100644 --- a/.github/workflows/proof-profile-comment.yml +++ b/.github/workflows/proof-profile-comment.yml @@ -1,13 +1,8 @@ name: Proof Profile Comment -# Companion to the `Proof Profile` workflow. That workflow runs the PR's Lean -# code to profile it, so it must run on the `pull_request` event — where a PR -# from a fork only gets a read-only GITHUB_TOKEN and cannot post a comment. -# This workflow fires when it finishes, runs in the base-repo context with a -# writable token, and posts the already-rendered profile for every PR, fork or -# not. It never checks out or runs PR code; it only downloads the pre-rendered -# `proof-profile-comment` artifact and posts it, so the writable token is never -# exposed to untrusted PR code. +# Retries comment publication when an on-demand `Proof Profile` run could not +# post directly. It only downloads the rendered artifact and never executes +# PR code with its writable token. on: workflow_run: workflows: ["Proof Profile"] diff --git a/.github/workflows/proof-profile.yml b/.github/workflows/proof-profile.yml index 6613b23f4d..b97c53e69f 100644 --- a/.github/workflows/proof-profile.yml +++ b/.github/workflows/proof-profile.yml @@ -1,11 +1,7 @@ name: Proof Profile -# Profile once when a ready PR is opened or a draft becomes ready, and again -# on demand when the PR author or anyone with write access comments `/profile`. -# No `synchronize` trigger — the -# profile is advisory, so re-run it by hand after a push if you want a fresh -# one. That on-demand path is what lets an external contributor re-profile -# their own PR after pushing. workflow_dispatch takes an explicit PR number. +# Profile on demand when the PR author or anyone with write access comments +# `/profile`, or through workflow_dispatch with an explicit PR number. # # Added files get an absolute profile (`lean --profile` + heartbeat counts). # Modified files instead get a base→head compile-cost comparison: heartbeats @@ -47,8 +43,6 @@ name: Proof Profile # also take from the default branch). on: - pull_request: - types: [opened, ready_for_review] issue_comment: types: [created] workflow_dispatch: @@ -74,7 +68,6 @@ concurrency: group: >- ${{ (github.event_name == 'workflow_dispatch' || - github.event_name == 'pull_request' || (github.event_name == 'issue_comment' && startsWith(github.event.comment.body, '/profile'))) && format('proof-profile-{0}', @@ -89,19 +82,16 @@ jobs: plan: runs-on: ubuntu-latest name: Plan profile - # Run automatically on ready PRs; workflow_dispatch also supports drafts. For issue - # comments, only when the body starts with `/profile` AND the commenter is + # workflow_dispatch also supports drafts. For issue comments, run only + # when the body starts with `/profile` AND the commenter is # either the PR author or someone with write access. The measurement jobs # check out and *run* the PR's Lean code, so the workflow stays # least-privilege (read-only token, no secrets) and the workflow # definition always comes from the base default branch (issue_comment - # context) — the same trust model under which fork PRs are already - # auto-profiled on `opened`. Letting the PR author re-profile their own PR - # therefore adds no new code-execution surface, while still barring an - # arbitrary commenter from triggering a run on someone else's fork PR. + # context), while barring an arbitrary commenter from triggering a run + # on someone else's fork PR. if: >- github.event_name == 'workflow_dispatch' || - (github.event_name == 'pull_request' && !github.event.pull_request.draft) || (github.event_name == 'issue_comment' && github.event.issue.pull_request != null && startsWith(github.event.comment.body, '/profile') && @@ -503,10 +493,8 @@ jobs: needs.plan.outputs.files != '' runs-on: ubuntu-latest name: Report profile - # `pull-requests: write` is only honored on runs whose token is writable - # anyway (same-repo `pull_request`, `/profile` comments, dispatch); fork - # `pull_request` tokens are capped read-only by the platform regardless - # of this declaration, and those runs take the companion path below. + # Only the reporting job receives comment permissions; measurement jobs + # execute PR Lean code with a read-only token. permissions: contents: read pull-requests: write @@ -558,8 +546,7 @@ jobs: || cp scripts/proof-profile/statements.py "$RUNNER_TEMP/statements.py" python3 "$RUNNER_TEMP/render.py" - # A run with a writable token (same-repo `pull_request`, a `/profile` - # comment, or a dispatch) posts the comment itself. The `workflow_run` + # A `/profile` comment or dispatch posts the comment itself. The `workflow_run` # companion cannot cover these reliably: GitHub never emits the event # for re-run attempts, which silently lost the comment on a bot-opened # PR whose first attempt sat waiting for approval (#326). @@ -594,16 +581,8 @@ jobs: gh pr comment "$PR_NUMBER" --repo "$REPO" --body-file comment-body.md fi - # A `pull_request` run from a fork gets a read-only GITHUB_TOKEN and - # cannot post a PR comment, so the comment is posted by the separate - # `Proof Profile Comment` workflow (workflow_run), which runs in the - # base-repo context with a writable token. Here we only stage the - # rendered profile and the PR number as an artifact for it to consume — - # this keeps the untrusted, PR-code-executing jobs read-only while the - # privileged poster never runs PR code. Staged whenever the direct - # post did not succeed — skipped (fork PR) or failed (API hiccup) — so - # the payload is never lost; the companion cannot double-post because - # a successful direct post stages nothing. + # Stage a retry payload if the direct post fails. The companion only + # publishes the rendered artifact and never executes PR code. - name: Stage comment payload for the companion workflow if: ${{ !cancelled() && steps.direct_post.outcome != 'success' }} env: diff --git a/.github/workflows/workflow_lint.yml b/.github/workflows/workflow_lint.yml index e8930e4776..ba9ce7882d 100644 --- a/.github/workflows/workflow_lint.yml +++ b/.github/workflows/workflow_lint.yml @@ -18,10 +18,49 @@ permissions: contents: read jobs: + scope: + runs-on: ubuntu-latest + outputs: + applicable: ${{ steps.scope.outputs.applicable }} + steps: + - uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd + with: + fetch-depth: 0 + persist-credentials: false + - id: scope + env: + EVENT: ${{ github.event_name }} + BASE: ${{ github.event.merge_group.base_sha || github.event.pull_request.base.sha }} + run: | + set -euo pipefail + applicable=true + if [ "$EVENT" = merge_group ] || [ "$EVENT" = pull_request ]; then + applicable=false + if [ "$EVENT" = pull_request ]; then + files=$(git diff --name-only "$BASE"...HEAD) + else + files=$(git diff --name-only "$BASE"..HEAD) + fi + if grep -Eq '^\.github/' <<< "$files"; then + applicable=true + fi + fi + echo "applicable=$applicable" >> "$GITHUB_OUTPUT" actionlint: + needs: scope + if: always() && (needs.scope.result != 'success' || needs.scope.outputs.applicable != 'false') runs-on: ubuntu-latest name: actionlint steps: + - name: Require successful change classification + env: + SCOPE_RESULT: ${{ needs.scope.result }} + APPLICABLE: ${{ needs.scope.outputs.applicable }} + run: | + if [ "$SCOPE_RESULT" != success ] || [ "$APPLICABLE" != true ]; then + echo "::error::Change classification failed; required validation cannot be skipped." + exit 1 + fi - name: Checkout uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd @@ -31,9 +70,20 @@ jobs: fail_level: any pinned-actions: + needs: scope + if: always() && (needs.scope.result != 'success' || needs.scope.outputs.applicable != 'false') runs-on: ubuntu-latest name: SHA-pinned Actions steps: + - name: Require successful change classification + env: + SCOPE_RESULT: ${{ needs.scope.result }} + APPLICABLE: ${{ needs.scope.outputs.applicable }} + run: | + if [ "$SCOPE_RESULT" != success ] || [ "$APPLICABLE" != true ]; then + echo "::error::Change classification failed; required validation cannot be skipped." + exit 1 + fi - name: Checkout uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd diff --git a/python/lean_pool/ci_cache.py b/python/lean_pool/ci_cache.py index 8d79e09dec..52f554259a 100644 --- a/python/lean_pool/ci_cache.py +++ b/python/lean_pool/ci_cache.py @@ -79,9 +79,32 @@ def obsolete_caches(caches: list[dict[str, Any]], key: str) -> list[int]: ] -def prune_cache(repository: str, key: str) -> None: - """Retain the replacement and remove older copies after a successful upload.""" - cache_family(key) +def obsolete_main_caches(caches: list[dict[str, Any]]) -> list[int]: + """Retain the newest main cache per known family and operating system.""" + newest: dict[str, dict[str, Any]] = {} + for cache in caches: + if cache.get("ref") != "refs/heads/main" or not cache.get("created_at"): + continue + try: + family = cache_family(cache.get("key", "")) + except ValueError: + continue + previous = newest.get(family) + if previous is None or cache["created_at"] > previous["created_at"]: + newest[family] = cache + return sorted( + { + identifier + for cache in newest.values() + for identifier in obsolete_caches(caches, cache["key"]) + } + ) + + +def prune_cache(repository: str, key: str | None = None) -> None: + """Remove older main caches after a specific or the newest replacement.""" + if key is not None: + cache_family(key) pages = json.loads( subprocess.check_output( [ @@ -96,7 +119,12 @@ def prune_cache(repository: str, key: str) -> None: ) ) caches = [cache for page in pages for cache in page["actions_caches"]] - for identifier in obsolete_caches(caches, key): + obsolete = ( + obsolete_caches(caches, key) + if key is not None + else obsolete_main_caches(caches) + ) + for identifier in obsolete: subprocess.run( [ "gh", @@ -119,7 +147,9 @@ def main() -> None: revision.add_argument("--ref", default="HEAD") prune = commands.add_parser("prune") prune.add_argument("--repository", required=True) - prune.add_argument("--key", required=True) + prune.add_argument( + "--key", help="Replacement key; omit to prune all known families" + ) arguments = parser.parse_args() logging.basicConfig(level=logging.INFO, format="cache: %(message)s") if arguments.command == "revision": diff --git a/python/tests/test_ci_cache.py b/python/tests/test_ci_cache.py index 5aad24ab84..7ac19e2650 100644 --- a/python/tests/test_ci_cache.py +++ b/python/tests/test_ci_cache.py @@ -8,7 +8,13 @@ import pytest -from lean_pool.ci_cache import build_revision, obsolete_caches, prune_cache +from lean_pool.ci_cache import ( + CACHE_PREFIXES, + build_revision, + obsolete_caches, + obsolete_main_caches, + prune_cache, +) def _commit(root: Path) -> None: @@ -182,3 +188,69 @@ def test_unknown_cache_family_is_rejected_before_api_calls(monkeypatch) -> None: ) with pytest.raises(ValueError, match="unsupported cache key"): prune_cache("owner/repo", "unknown") + + +def test_scheduled_pruning_preserves_newest_main_cache_per_family_and_platform(): + """All supported families retain a replacement; PR and unknown caches survive.""" + keys = [ + (f"{prefix}Linux-{age}", "refs/heads/main", f"2026-10-10T0{age}:00:00Z") + for prefix in CACHE_PREFIXES + for age in range(2) + ] + [ + ("LeanPoolBuild-v1-Windows-only", "refs/heads/main", "2026-10-10T00:00:00Z"), + ("LeanPoolBuild-v1-Linux-pr", "refs/pull/1/merge", "2026-10-10T02:00:00Z"), + ("unknown-cache", "refs/heads/main", "2026-10-10T00:00:00Z"), + ] + caches = [ + { + "id": index, + "key": key, + "ref": reference, + "created_at": created, + } + for index, (key, reference, created) in enumerate(keys) + ] + assert obsolete_main_caches(caches) == list(range(0, len(CACHE_PREFIXES) * 2, 2)) + caches.reverse() + assert obsolete_main_caches(caches) == list(range(0, len(CACHE_PREFIXES) * 2, 2)) + + +def test_scheduled_pruning_ignores_incomplete_timestamps(): + """Unordered API data cannot choose an arbitrary replacement without timestamps.""" + caches = [ + { + "id": index, + "key": f"LeanPoolBuild-v1-Linux-{index}", + "ref": "refs/heads/main", + } + for index in range(2) + ] + assert obsolete_main_caches(caches) == [] + + +def test_scheduled_pruning_uses_a_single_snapshot(monkeypatch): + """Maintenance deletes only older main entries found in its API snapshot.""" + pages = [ + { + "actions_caches": [ + { + "id": index, + "key": f"LeanPoolBuild-v1-Linux-{index}", + "ref": "refs/heads/main", + "created_at": f"2026-10-10T0{index}:00:00Z", + } + for index in range(2) + ] + } + ] + calls = [] + monkeypatch.setattr( + subprocess, "check_output", lambda *args, **kwargs: json.dumps(pages) + ) + monkeypatch.setattr( + subprocess, "run", lambda command, **kwargs: calls.append(command) + ) + prune_cache("owner/repo") + assert calls == [ + ["gh", "api", "--method", "DELETE", "repos/owner/repo/actions/caches/0"] + ] diff --git a/python/tests/test_ci_cache_contract.py b/python/tests/test_ci_cache_contract.py index 388c8dae4f..db75289fa1 100644 --- a/python/tests/test_ci_cache_contract.py +++ b/python/tests/test_ci_cache_contract.py @@ -6,6 +6,7 @@ import subprocess from pathlib import Path +import pytest import yaml WORKFLOWS = Path(__file__).resolve().parents[2] / ".github/workflows" @@ -62,10 +63,10 @@ def _docs_condition(condition: str, event: str, ref: str, preview: bool, readme: def test_docs_generate_on_main_and_explicit_preview_only() -> None: - """A PR runs its protected preflight without allocating heavy docs runners.""" + """PRs scope preflight without allocating heavy docs runners.""" jobs = yaml.safe_load((WORKFLOWS / "docs.yml").read_text())["jobs"] assert jobs["preflight"]["name"] == "Documentation preflight" - assert "if" not in jobs["preflight"] + assert jobs["preflight"]["needs"] == "scope" scenarios = [ ("pull_request", "refs/pull/123/merge", False, False, False), ("push", "refs/heads/main", False, False, True), @@ -179,6 +180,8 @@ def test_required_scoped_checks_fail_closed_when_classification_fails() -> None: for filename, names in ( ("python_ci.yml", ("lint", "test")), ("exposition-verify.yml", ("verify",)), + ("docs.yml", ("preflight",)), + ("workflow_lint.yml", ("actionlint", "pinned-actions")), ): workflow = yaml.safe_load((WORKFLOWS / filename).read_text()) for name in names: @@ -228,7 +231,9 @@ def test_minimal_verifier_pr_has_an_explicit_project_build_producer(tmp_path): assert pattern in planning["run"] classification = ( "minimal_build=false" - + planning["run"].split("minimal_build=false", 1)[1].split("cold=false", 1)[0] + + planning["run"] + .split("minimal_build=false", 1)[1] + .split("dependency_tests=true", 1)[0] ) changed = tmp_path / "changed-files.txt" output = tmp_path / "output.txt" @@ -321,10 +326,6 @@ def test_extraction_caches_survive_failure_and_retry_keys_can_advance(): assert "scripts/exposition/build-minimal.mjs" not in extraction_key assert "scripts/exposition/Extract.lean" in extraction_key assert "scripts/exposition/extract-all.sh" in extraction_key - if workflow == "docs.yml": - pruned = names["Prune old copies of project extraction cache"] - assert "steps.extraction-cache-save.outcome == 'success'" in pruned["if"] - assert "github.ref == 'refs/heads/main'" in pruned["if"] def test_minimal_build_wait_does_not_consume_verification_window() -> None: @@ -367,3 +368,229 @@ def test_minimal_build_wait_does_not_consume_verification_window() -> None: capture_output=True, ) assert (process.returncode == 0) == accepted + + +@pytest.fixture +def scope_repository(tmp_path: Path) -> tuple[Path, str]: + """Create a real diff for executing the workflow classifiers.""" + subprocess.run(["git", "init", "-q"], cwd=tmp_path, check=True) + subprocess.run( + [ + "git", + "-c", + "user.name=Test", + "-c", + "user.email=test@example.com", + "commit", + "--allow-empty", + "-qm", + "base", + ], + cwd=tmp_path, + check=True, + ) + base = subprocess.check_output( + ["git", "rev-parse", "HEAD"], cwd=tmp_path, text=True + ).strip() + return tmp_path, base + + +@pytest.mark.parametrize("event", ["pull_request", "merge_group"]) +@pytest.mark.parametrize( + "filename,changed,expected", + [ + ("docs.yml", "LeanPool/Example/Proof.lean", False), + ("docs.yml", "LeanPool/projects/example.yaml", False), + ("docs.yml", "README.md", False), + ("docs.yml", "docbuild/lakefile.toml", True), + ("docs.yml", "lean-toolchain", True), + ("docs.yml", "lake-manifest.json", True), + ("docs.yml", "python/lean_pool/exposition/generate.py", True), + ("docs.yml", "scripts/exposition/extract-all.sh", True), + ("docs.yml", ".github/workflows/docs.yml", True), + ("workflow_lint.yml", "LeanPool/Example/Proof.lean", False), + ("workflow_lint.yml", "python/lean_pool/ci_cache.py", False), + ("workflow_lint.yml", ".github/workflows/cache-maintenance.yml", True), + ], +) +def test_scoped_checks_classify_real_diffs( + scope_repository, filename, changed, expected, event +) -> None: + """Only relevant PR and queue changes allocate expensive validation jobs.""" + root, base = scope_repository + path = root / changed + path.parent.mkdir(parents=True, exist_ok=True) + path.write_text("change\n") + subprocess.run(["git", "add", "."], cwd=root, check=True) + subprocess.run( + [ + "git", + "-c", + "user.name=Test", + "-c", + "user.email=test@example.com", + "commit", + "-qm", + "change", + ], + cwd=root, + check=True, + ) + workflow = yaml.safe_load((WORKFLOWS / filename).read_text()) + command = workflow["jobs"]["scope"]["steps"][-1]["run"] + output = root / "output" + subprocess.run( + ["bash", "-e", "-c", command], + cwd=root, + check=True, + env={**os.environ, "EVENT": event, "BASE": base, "GITHUB_OUTPUT": str(output)}, + ) + assert output.read_text().strip() == f"applicable={str(expected).lower()}" + + +@pytest.mark.parametrize("filename", ["docs.yml", "workflow_lint.yml"]) +def test_scoped_checks_do_not_skip_when_git_diff_fails(scope_repository, filename): + """An unavailable base produces failure rather than a false skip decision.""" + root, _ = scope_repository + workflow = yaml.safe_load((WORKFLOWS / filename).read_text()) + command = workflow["jobs"]["scope"]["steps"][-1]["run"] + output = root / "output" + process = subprocess.run( + ["bash", "-e", "-c", command], + cwd=root, + capture_output=True, + env={ + **os.environ, + "EVENT": "pull_request", + "BASE": "missing-base", + "GITHUB_OUTPUT": str(output), + }, + ) + assert process.returncode != 0 + assert not output.exists() + + +@pytest.mark.parametrize("filename", ["docs.yml", "workflow_lint.yml"]) +@pytest.mark.parametrize("event", ["push", "workflow_dispatch"]) +def test_scoped_checks_run_for_main_and_manual_requests(tmp_path, filename, event): + """Publishing and explicit requests retain validation without needing a diff.""" + workflow = yaml.safe_load((WORKFLOWS / filename).read_text()) + command = workflow["jobs"]["scope"]["steps"][-1]["run"] + output = tmp_path / "output" + subprocess.run( + ["bash", "-e", "-c", command], + cwd=tmp_path, + check=True, + env={ + **os.environ, + "EVENT": event, + "BASE": "missing-base", + "GITHUB_OUTPUT": str(output), + }, + ) + assert output.read_text().strip() == "applicable=true" + + +@pytest.mark.parametrize("filename", ["docs.yml", "workflow_lint.yml"]) +def test_scoped_checks_handle_large_diffs(tmp_path, filename): + """An early match cannot become a false skip through a broken shell pipe.""" + commands = tmp_path / "commands" + commands.mkdir() + git = commands / "git" + git.write_text('#!/bin/bash\ncat "$CHANGED_FILES"\n') + git.chmod(0o755) + changed_files = tmp_path / "changed" + changed_files.write_text( + ".github/workflows/docs.yml\n" + + "LeanPool/Example/LongPath/Proof.lean\n" * 10000 + ) + workflow = yaml.safe_load((WORKFLOWS / filename).read_text()) + command = workflow["jobs"]["scope"]["steps"][-1]["run"] + output = tmp_path / "output" + subprocess.run( + ["bash", "-e", "-c", command], + cwd=tmp_path, + check=True, + env={ + **os.environ, + "PATH": f"{commands}:{os.environ['PATH']}", + "EVENT": "pull_request", + "BASE": "base", + "CHANGED_FILES": str(changed_files), + "GITHUB_OUTPUT": str(output), + }, + ) + assert output.read_text().strip() == "applicable=true" + + +@pytest.mark.parametrize( + "changed,diff_available,force_full,expected", + [ + ("LeanPool/Example/Proof.lean", "true", "false", False), + ("LeanPool/projects/example.yaml", "true", "false", False), + ("lean-toolchain", "true", "false", True), + ("lakefile.toml", "true", "false", True), + ("lake-manifest.json", "true", "false", True), + ("python/lean_pool/ci_pr_build.py", "true", "false", True), + ("python/tests/test_ci_pr_build.py", "true", "false", True), + ("scripts/ProjectIndexes.lean", "true", "false", True), + (".github/workflows/lean_action_ci.yml", "true", "false", True), + ("", "false", "false", True), + ("LeanPool/Example/Proof.lean", "true", "true", True), + ], +) +def test_dependency_tracking_tests_scope( + tmp_path, changed, diff_available, force_full, expected +): + """Dependency tracking is tested for tooling changes and unknown/manual scopes.""" + jobs = yaml.safe_load((WORKFLOWS / "lean_action_ci.yml").read_text())["jobs"] + planning = next(step for step in jobs["plan"]["steps"] if step.get("id") == "plan") + command = ( + "dependency_tests=true" + + planning["run"].split("dependency_tests=true", 1)[1].split("cold=false", 1)[0] + ) + changed_files = tmp_path / "changed" + changed_files.write_text(changed + "\n") + output = tmp_path / "output" + subprocess.run( + ["bash", "-e", "-c", command], + check=True, + env={ + **os.environ, + "changed_files": str(changed_files), + "diff_available": diff_available, + "FORCE_FULL": force_full, + "GITHUB_OUTPUT": str(output), + }, + ) + assert output.read_text().strip() == f"dependency_tests={str(expected).lower()}" + for name in ("build", "finalize", "rebase"): + tracking = next( + step + for step in jobs[name]["steps"] + if step.get("name") + == "Check compiled artifact dependency tracking with pinned Lean" + ) + assert tracking["if"] == "needs.plan.outputs.dependency_tests == 'true'" + + +def test_profiling_is_opt_in_and_cache_pruning_is_scheduled() -> None: + """Advisory compilation and maintenance do not run on ordinary PR events.""" + profiling = yaml.safe_load((WORKFLOWS / "proof-profile.yml").read_text()) + assert set(profiling.get("on", profiling.get(True))) == { + "issue_comment", + "workflow_dispatch", + } + maintenance = yaml.safe_load((WORKFLOWS / "cache-maintenance.yml").read_text()) + assert set(maintenance.get("on", maintenance.get(True))) == { + "schedule", + "workflow_dispatch", + } + assert maintenance["permissions"]["actions"] == "write" + for filename in ("lean_action_ci.yml", "docs.yml"): + workflow = yaml.safe_load((WORKFLOWS / filename).read_text()) + assert not any( + "lean_pool.ci_cache prune" in step.get("run", "") + for job in workflow["jobs"].values() + for step in job["steps"] + ) From b681fd353c922300b8d549413b87835621cb170c Mon Sep 17 00:00:00 2001 From: Vasily Ilin Date: Sat, 10 Oct 2026 07:15:35 +0000 Subject: [PATCH 2/4] Keep renamed inputs in CI scope and preserve incomplete caches --- .github/workflows/docs.yml | 6 +- .github/workflows/lean_action_ci.yml | 6 +- .github/workflows/workflow_lint.yml | 4 +- python/lean_pool/ci_cache.py | 16 +++- python/tests/test_ci_cache.py | 22 +++++ python/tests/test_ci_cache_contract.py | 128 +++++++++++++++++++++++++ 6 files changed, 170 insertions(+), 12 deletions(-) diff --git a/.github/workflows/docs.yml b/.github/workflows/docs.yml index 712d6dc5c6..d5d3c4957c 100644 --- a/.github/workflows/docs.yml +++ b/.github/workflows/docs.yml @@ -65,9 +65,9 @@ jobs: if [ "$EVENT" = merge_group ] || [ "$EVENT" = pull_request ]; then applicable=false if [ "$EVENT" = pull_request ]; then - files=$(git diff --name-only "$BASE"...HEAD) + files=$(git diff --name-only --no-renames "$BASE"...HEAD) else - files=$(git diff --name-only "$BASE"..HEAD) + files=$(git diff --name-only --no-renames "$BASE"..HEAD) fi if grep -Eq '^(docbuild/|lean-toolchain$|lakefile\.toml$|lake-manifest\.json$|python/lean_pool/(exposition/|quality\.py$|validation_cache\.py$|ci_artifacts\.py$|ci_cache\.py$|rebase_fastpath\.py$)|python/(pyproject\.toml|uv\.lock)$|scripts/exposition/|\.github/workflows/docs\.yml$)' <<< "$files"; then applicable=true @@ -123,7 +123,7 @@ jobs: set -euo pipefail readme_only=false if [ "$EVENT_NAME" = "pull_request" ]; then - files="$(git diff --name-only "$BASE_SHA"..."$HEAD_SHA")" + files="$(git diff --name-only --no-renames "$BASE_SHA"..."$HEAD_SHA")" if [ "$files" = "README.md" ]; then readme_only=true fi diff --git a/.github/workflows/lean_action_ci.yml b/.github/workflows/lean_action_ci.yml index dcdb00569a..5fe9f390c2 100644 --- a/.github/workflows/lean_action_ci.yml +++ b/.github/workflows/lean_action_ci.yml @@ -146,16 +146,16 @@ jobs: : > "$changed_files" case "$EVENT_NAME" in merge_group) - git diff --name-only "$BASE_SHA"..HEAD > "$changed_files" + git diff --name-only --no-renames "$BASE_SHA"..HEAD > "$changed_files" ;; pull_request) - git diff --name-only "$BASE_SHA"...HEAD > "$changed_files" + git diff --name-only --no-renames "$BASE_SHA"...HEAD > "$changed_files" ;; push) if [ -n "$BEFORE_SHA" ] \ && ! printf '%s' "$BEFORE_SHA" | grep -q '^0*$' \ && git cat-file -e "$BEFORE_SHA" 2>/dev/null; then - git diff --name-only "$BEFORE_SHA"..HEAD > "$changed_files" + git diff --name-only --no-renames "$BEFORE_SHA"..HEAD > "$changed_files" else diff_available=false fi diff --git a/.github/workflows/workflow_lint.yml b/.github/workflows/workflow_lint.yml index ba9ce7882d..c0c48dde76 100644 --- a/.github/workflows/workflow_lint.yml +++ b/.github/workflows/workflow_lint.yml @@ -37,9 +37,9 @@ jobs: if [ "$EVENT" = merge_group ] || [ "$EVENT" = pull_request ]; then applicable=false if [ "$EVENT" = pull_request ]; then - files=$(git diff --name-only "$BASE"...HEAD) + files=$(git diff --name-only --no-renames "$BASE"...HEAD) else - files=$(git diff --name-only "$BASE"..HEAD) + files=$(git diff --name-only --no-renames "$BASE"..HEAD) fi if grep -Eq '^\.github/' <<< "$files"; then applicable=true diff --git a/python/lean_pool/ci_cache.py b/python/lean_pool/ci_cache.py index 52f554259a..5f4feb8123 100644 --- a/python/lean_pool/ci_cache.py +++ b/python/lean_pool/ci_cache.py @@ -81,10 +81,18 @@ def obsolete_caches(caches: list[dict[str, Any]], key: str) -> list[int]: def obsolete_main_caches(caches: list[dict[str, Any]]) -> list[int]: """Retain the newest main cache per known family and operating system.""" + completed = [ + cache + for cache in caches + if cache.get("ref") == "refs/heads/main" + and isinstance(cache.get("created_at"), str) + and cache["created_at"] + and isinstance(cache.get("size_in_bytes"), int) + and cache["size_in_bytes"] > 0 + and isinstance(cache.get("key"), str) + ] newest: dict[str, dict[str, Any]] = {} - for cache in caches: - if cache.get("ref") != "refs/heads/main" or not cache.get("created_at"): - continue + for cache in completed: try: family = cache_family(cache.get("key", "")) except ValueError: @@ -96,7 +104,7 @@ def obsolete_main_caches(caches: list[dict[str, Any]]) -> list[int]: { identifier for cache in newest.values() - for identifier in obsolete_caches(caches, cache["key"]) + for identifier in obsolete_caches(completed, cache["key"]) } ) diff --git a/python/tests/test_ci_cache.py b/python/tests/test_ci_cache.py index 7ac19e2650..a19a630a18 100644 --- a/python/tests/test_ci_cache.py +++ b/python/tests/test_ci_cache.py @@ -207,6 +207,7 @@ def test_scheduled_pruning_preserves_newest_main_cache_per_family_and_platform() "key": key, "ref": reference, "created_at": created, + "size_in_bytes": 1024, } for index, (key, reference, created) in enumerate(keys) ] @@ -238,6 +239,7 @@ def test_scheduled_pruning_uses_a_single_snapshot(monkeypatch): "key": f"LeanPoolBuild-v1-Linux-{index}", "ref": "refs/heads/main", "created_at": f"2026-10-10T0{index}:00:00Z", + "size_in_bytes": 1024, } for index in range(2) ] @@ -254,3 +256,23 @@ def test_scheduled_pruning_uses_a_single_snapshot(monkeypatch): assert calls == [ ["gh", "api", "--method", "DELETE", "repos/owner/repo/actions/caches/0"] ] + + +def test_scheduled_pruning_requires_complete_cache_metadata(): + """Empty uploads and missing metadata cannot replace or erase a saved build.""" + caches = [ + { + "id": index, + "key": f"LeanPoolBuild-v1-Linux-{index}", + "ref": "refs/heads/main", + "created_at": f"2026-10-10T0{index}:00:00Z", + "size_in_bytes": 1024, + } + for index in range(5) + ] + caches[2]["size_in_bytes"] = 0 + del caches[3]["created_at"] + del caches[4]["size_in_bytes"] + assert obsolete_main_caches(caches) == [0] + caches[1]["key"] = None + assert obsolete_main_caches(caches) == [] diff --git a/python/tests/test_ci_cache_contract.py b/python/tests/test_ci_cache_contract.py index db75289fa1..85f5590d0c 100644 --- a/python/tests/test_ci_cache_contract.py +++ b/python/tests/test_ci_cache_contract.py @@ -448,6 +448,134 @@ def test_scoped_checks_classify_real_diffs( assert output.read_text().strip() == f"applicable={str(expected).lower()}" +@pytest.mark.parametrize("event", ["pull_request", "merge_group"]) +@pytest.mark.parametrize( + "filename,original", + [ + ("docs.yml", "docbuild/lean-toolchain"), + ("workflow_lint.yml", ".github/workflows/example.yml"), + ], +) +def test_moving_files_out_of_scope_still_runs_validation( + scope_repository, filename, original, event +): + """Renaming a configuration outside its directory must validate its removal.""" + root, _ = scope_repository + base = _move_scope_file(root, original) + workflow = yaml.safe_load((WORKFLOWS / filename).read_text()) + output = root / "output" + subprocess.run( + ["bash", "-e", "-c", workflow["jobs"]["scope"]["steps"][-1]["run"]], + cwd=root, + check=True, + env={**os.environ, "EVENT": event, "BASE": base, "GITHUB_OUTPUT": str(output)}, + ) + assert output.read_text().strip() == "applicable=true" + if filename == "docs.yml" and event == "pull_request": + detection = next( + step + for step in workflow["jobs"]["preflight"]["steps"] + if step.get("name") == "Detect README-only change" + ) + output.write_text("") + subprocess.run( + ["bash", "-e", "-c", detection["run"]], + cwd=root, + check=True, + env={ + **os.environ, + "EVENT_NAME": event, + "BASE_SHA": base, + "HEAD_SHA": "HEAD", + "GITHUB_OUTPUT": str(output), + }, + ) + assert output.read_text().strip() == "readme_only=false" + + +def _scope_commit(root: Path) -> None: + subprocess.run( + [ + "git", + "-c", + "user.name=Test", + "-c", + "user.email=test@example.com", + "commit", + "-qm", + "configuration change", + ], + cwd=root, + check=True, + ) + + +def _move_scope_file(root: Path, original: str) -> str: + path = root / original + path.parent.mkdir(parents=True, exist_ok=True) + path.write_text("original configuration\n") + subprocess.run(["git", "add", "."], cwd=root, check=True) + _scope_commit(root) + base = subprocess.check_output( + ["git", "rev-parse", "HEAD"], cwd=root, text=True + ).strip() + path.rename(root / "README.md") + subprocess.run(["git", "add", "-A"], cwd=root, check=True) + _scope_commit(root) + return base + + +@pytest.mark.parametrize("event", ["pull_request", "merge_group", "push"]) +def test_lean_planner_retains_removed_configuration_after_rename( + scope_repository, event +): + """A renamed toolchain remains a build and dependency-test input.""" + root, _ = scope_repository + base = _move_scope_file(root, "lean-toolchain") + jobs = yaml.safe_load((WORKFLOWS / "lean_action_ci.yml").read_text())["jobs"] + planning = next(step for step in jobs["plan"]["steps"] if step.get("id") == "plan") + command = ( + 'case "$EVENT_NAME" in' + + planning["run"].split('case "$EVENT_NAME" in', 1)[1].split("esac", 1)[0] + + "esac" + ) + changed_files = root / "changed" + subprocess.run( + ["bash", "-e", "-c", command], + cwd=root, + check=True, + env={ + **os.environ, + "EVENT_NAME": event, + "BASE_SHA": base, + "BEFORE_SHA": base, + "changed_files": str(changed_files), + }, + ) + assert set(changed_files.read_text().splitlines()) == { + "README.md", + "lean-toolchain", + } + command = ( + "dependency_tests=true" + + planning["run"].split("dependency_tests=true", 1)[1].split("cold=false", 1)[0] + ) + output = root / "output" + subprocess.run( + ["bash", "-e", "-c", command], + cwd=root, + check=True, + env={ + **os.environ, + "changed_files": str(changed_files), + "diff_available": "true", + "FORCE_FULL": "false", + "GITHUB_OUTPUT": str(output), + }, + ) + assert output.read_text().strip() == "dependency_tests=true" + + @pytest.mark.parametrize("filename", ["docs.yml", "workflow_lint.yml"]) def test_scoped_checks_do_not_skip_when_git_diff_fails(scope_repository, filename): """An unavailable base produces failure rather than a false skip decision.""" From a5357d01e007a4e9fd9ae7e7c5c957433f66791e Mon Sep 17 00:00:00 2001 From: Vasily Ilin Date: Sat, 10 Oct 2026 07:39:43 +0000 Subject: [PATCH 3/4] Recognize Git-quoted paths in scoped CI checks --- .github/workflows/docs.yml | 3 ++- .github/workflows/lean_action_ci.yml | 3 ++- .github/workflows/workflow_lint.yml | 3 ++- python/tests/test_ci_cache_contract.py | 8 ++++++++ 4 files changed, 14 insertions(+), 3 deletions(-) diff --git a/.github/workflows/docs.yml b/.github/workflows/docs.yml index d5d3c4957c..86c31bc3be 100644 --- a/.github/workflows/docs.yml +++ b/.github/workflows/docs.yml @@ -69,7 +69,8 @@ jobs: else files=$(git diff --name-only --no-renames "$BASE"..HEAD) fi - if grep -Eq '^(docbuild/|lean-toolchain$|lakefile\.toml$|lake-manifest\.json$|python/lean_pool/(exposition/|quality\.py$|validation_cache\.py$|ci_artifacts\.py$|ci_cache\.py$|rebase_fastpath\.py$)|python/(pyproject\.toml|uv\.lock)$|scripts/exposition/|\.github/workflows/docs\.yml$)' <<< "$files"; then + # Git may quote names containing Unicode or control characters. + if grep -Eq '^"?(docbuild/|lean-toolchain$|lakefile\.toml$|lake-manifest\.json$|python/lean_pool/(exposition/|quality\.py$|validation_cache\.py$|ci_artifacts\.py$|ci_cache\.py$|rebase_fastpath\.py$)|python/(pyproject\.toml|uv\.lock)$|scripts/exposition/|\.github/workflows/docs\.yml$)' <<< "$files"; then applicable=true fi fi diff --git a/.github/workflows/lean_action_ci.yml b/.github/workflows/lean_action_ci.yml index 5fe9f390c2..5917d80666 100644 --- a/.github/workflows/lean_action_ci.yml +++ b/.github/workflows/lean_action_ci.yml @@ -172,7 +172,8 @@ jobs: dependency_tests=true if [ "$diff_available" = true ] && [ "$FORCE_FULL" != true ]; then dependency_tests=false - if grep -Eq '^(lean-toolchain$|lakefile\.toml$|lake-manifest\.json$|python/|scripts/ci/|scripts/ProjectIndexes\.lean$|\.github/workflows/lean_action_ci\.yml$)' "$changed_files"; then + # Git may quote names containing Unicode or control characters. + if grep -Eq '^"?(lean-toolchain$|lakefile\.toml$|lake-manifest\.json$|python/|scripts/ci/|scripts/ProjectIndexes\.lean$|\.github/workflows/lean_action_ci\.yml$)' "$changed_files"; then dependency_tests=true fi fi diff --git a/.github/workflows/workflow_lint.yml b/.github/workflows/workflow_lint.yml index c0c48dde76..7ed2c5aaf4 100644 --- a/.github/workflows/workflow_lint.yml +++ b/.github/workflows/workflow_lint.yml @@ -41,7 +41,8 @@ jobs: else files=$(git diff --name-only --no-renames "$BASE"..HEAD) fi - if grep -Eq '^\.github/' <<< "$files"; then + # Git may quote names containing Unicode or control characters. + if grep -Eq '^"?\.github/' <<< "$files"; then applicable=true fi fi diff --git a/python/tests/test_ci_cache_contract.py b/python/tests/test_ci_cache_contract.py index 85f5590d0c..bb654a37a5 100644 --- a/python/tests/test_ci_cache_contract.py +++ b/python/tests/test_ci_cache_contract.py @@ -374,6 +374,9 @@ def test_minimal_build_wait_does_not_consume_verification_window() -> None: def scope_repository(tmp_path: Path) -> tuple[Path, str]: """Create a real diff for executing the workflow classifiers.""" subprocess.run(["git", "init", "-q"], cwd=tmp_path, check=True) + subprocess.run( + ["git", "config", "core.quotePath", "true"], cwd=tmp_path, check=True + ) subprocess.run( [ "git", @@ -403,6 +406,8 @@ def scope_repository(tmp_path: Path) -> tuple[Path, str]: ("docs.yml", "LeanPool/projects/example.yaml", False), ("docs.yml", "README.md", False), ("docs.yml", "docbuild/lakefile.toml", True), + ("docs.yml", "docbuild/名前.lean", True), + ("docs.yml", "docbuild/line\nbreak.lean", True), ("docs.yml", "lean-toolchain", True), ("docs.yml", "lake-manifest.json", True), ("docs.yml", "python/lean_pool/exposition/generate.py", True), @@ -411,6 +416,8 @@ def scope_repository(tmp_path: Path) -> tuple[Path, str]: ("workflow_lint.yml", "LeanPool/Example/Proof.lean", False), ("workflow_lint.yml", "python/lean_pool/ci_cache.py", False), ("workflow_lint.yml", ".github/workflows/cache-maintenance.yml", True), + ("workflow_lint.yml", ".github/workflows/名前.yml", True), + ("workflow_lint.yml", ".github/workflows/line\nbreak.yml", True), ], ) def test_scoped_checks_classify_real_diffs( @@ -661,6 +668,7 @@ def test_scoped_checks_handle_large_diffs(tmp_path, filename): ("lake-manifest.json", "true", "false", True), ("python/lean_pool/ci_pr_build.py", "true", "false", True), ("python/tests/test_ci_pr_build.py", "true", "false", True), + ('"python/lean_pool/quoted.py"', "true", "false", True), ("scripts/ProjectIndexes.lean", "true", "false", True), (".github/workflows/lean_action_ci.yml", "true", "false", True), ("", "false", "false", True), From 90b9f434a3febb9d34906161ca8183542def3fd1 Mon Sep 17 00:00:00 2001 From: Vasily Ilin Date: Sat, 10 Oct 2026 07:47:06 +0000 Subject: [PATCH 4/4] Address cache-version retention and preserve helper regression coverage --- .github/workflows/docs.yml | 4 +++- .github/workflows/lean_action_ci.yml | 2 +- python/lean_pool/ci_cache.py | 22 +++++++++++++++------- python/tests/test_ci_cache.py | 21 +++++++++++++++++++++ python/tests/test_ci_cache_contract.py | 14 ++++++++++++++ 5 files changed, 54 insertions(+), 9 deletions(-) diff --git a/.github/workflows/docs.yml b/.github/workflows/docs.yml index 86c31bc3be..3e4aeb1480 100644 --- a/.github/workflows/docs.yml +++ b/.github/workflows/docs.yml @@ -15,6 +15,8 @@ on: - 'lean-toolchain' - 'docbuild/**' - 'python/lean_pool/exposition/**' + - 'python/lean_pool/documentation.py' + - 'python/lean_pool/indexes.py' - 'python/lean_pool/quality.py' - 'python/lean_pool/validation_cache.py' - 'python/lean_pool/ci_artifacts.py' @@ -70,7 +72,7 @@ jobs: files=$(git diff --name-only --no-renames "$BASE"..HEAD) fi # Git may quote names containing Unicode or control characters. - if grep -Eq '^"?(docbuild/|lean-toolchain$|lakefile\.toml$|lake-manifest\.json$|python/lean_pool/(exposition/|quality\.py$|validation_cache\.py$|ci_artifacts\.py$|ci_cache\.py$|rebase_fastpath\.py$)|python/(pyproject\.toml|uv\.lock)$|scripts/exposition/|\.github/workflows/docs\.yml$)' <<< "$files"; then + if grep -Eq '^"?(docbuild/|lean-toolchain$|lakefile\.toml$|lake-manifest\.json$|python/lean_pool/(exposition/|documentation\.py$|indexes\.py$|quality\.py$|validation_cache\.py$|ci_artifacts\.py$|ci_cache\.py$|rebase_fastpath\.py$)|python/(pyproject\.toml|uv\.lock)$|scripts/exposition/|\.github/workflows/docs\.yml$)' <<< "$files"; then applicable=true fi fi diff --git a/.github/workflows/lean_action_ci.yml b/.github/workflows/lean_action_ci.yml index 5917d80666..9911b4185a 100644 --- a/.github/workflows/lean_action_ci.yml +++ b/.github/workflows/lean_action_ci.yml @@ -173,7 +173,7 @@ jobs: if [ "$diff_available" = true ] && [ "$FORCE_FULL" != true ]; then dependency_tests=false # Git may quote names containing Unicode or control characters. - if grep -Eq '^"?(lean-toolchain$|lakefile\.toml$|lake-manifest\.json$|python/|scripts/ci/|scripts/ProjectIndexes\.lean$|\.github/workflows/lean_action_ci\.yml$)' "$changed_files"; then + if grep -Eq '^"?(lean-toolchain$|lakefile\.toml$|lake-manifest\.json$|python/|scripts/ci/|scripts/exposition/|scripts/ProjectIndexes\.lean$|\.github/workflows/lean_action_ci\.yml$)' "$changed_files"; then dependency_tests=true fi fi diff --git a/python/lean_pool/ci_cache.py b/python/lean_pool/ci_cache.py index 5f4feb8123..e90aba847d 100644 --- a/python/lean_pool/ci_cache.py +++ b/python/lean_pool/ci_cache.py @@ -59,7 +59,7 @@ def cache_family(key: str) -> str: def obsolete_caches(caches: list[dict[str, Any]], key: str) -> list[int]: """Prune old copies only after the replacement is visible on main.""" - family = cache_family(key) + cache_family(key) replacements = [ cache for cache in caches @@ -67,20 +67,28 @@ def obsolete_caches(caches: list[dict[str, Any]], key: str) -> list[int]: ] if not replacements: return [] - created = replacements[0].get("created_at", "") - return [ + replacement = max(replacements, key=lambda cache: cache.get("created_at", "")) + return _obsolete_before(caches, replacement) + + +def _obsolete_before( + caches: list[dict[str, Any]], replacement: dict[str, Any] +) -> list[int]: + family = cache_family(replacement["key"]) + created = replacement.get("created_at", "") + return sorted( cache["id"] for cache in caches if cache.get("ref") == "refs/heads/main" and isinstance(cache.get("key"), str) and cache["key"].startswith(family) - and cache["key"] != key + and cache["id"] != replacement["id"] and (not created or cache.get("created_at", "") < created) - ] + ) def obsolete_main_caches(caches: list[dict[str, Any]]) -> list[int]: - """Retain the newest main cache per known family and operating system.""" + """Retain the newest completed main record per family/OS across cache versions.""" completed = [ cache for cache in caches @@ -104,7 +112,7 @@ def obsolete_main_caches(caches: list[dict[str, Any]]) -> list[int]: { identifier for cache in newest.values() - for identifier in obsolete_caches(completed, cache["key"]) + for identifier in _obsolete_before(completed, cache) } ) diff --git a/python/tests/test_ci_cache.py b/python/tests/test_ci_cache.py index a19a630a18..cb46c8af00 100644 --- a/python/tests/test_ci_cache.py +++ b/python/tests/test_ci_cache.py @@ -276,3 +276,24 @@ def test_scheduled_pruning_requires_complete_cache_metadata(): assert obsolete_main_caches(caches) == [0] caches[1]["key"] = None assert obsolete_main_caches(caches) == [] + + +@pytest.mark.parametrize("reverse", [False, True]) +def test_retention_selects_a_record_when_versions_share_a_key(reverse): + """A newer version replaces older versions regardless of API list order.""" + caches = [ + { + "id": index, + "key": f"LeanPoolBuild-v1-Linux-{key}", + "version": version, + "ref": "refs/heads/main", + "created_at": f"2026-10-10T0{index}:00:00Z", + "size_in_bytes": 1024, + } + for index, (key, version) in enumerate([("A", "v1"), ("B", "v1"), ("A", "v2")]) + ] + if reverse: + caches.reverse() + assert obsolete_main_caches(caches) == [0, 1] + assert obsolete_caches(caches, "LeanPoolBuild-v1-Linux-A") == [0, 1] + assert obsolete_caches(caches, "LeanPoolBuild-v1-Linux-B") == [0] diff --git a/python/tests/test_ci_cache_contract.py b/python/tests/test_ci_cache_contract.py index bb654a37a5..f8ec886aa9 100644 --- a/python/tests/test_ci_cache_contract.py +++ b/python/tests/test_ci_cache_contract.py @@ -92,6 +92,16 @@ def test_docs_generate_on_main_and_explicit_preview_only() -> None: ) +def test_documentation_helper_changes_trigger_main_publishing() -> None: + """Documentation's preparation/rendering helpers also trigger publication.""" + workflow = yaml.safe_load((WORKFLOWS / "docs.yml").read_text()) + events = workflow.get("on", workflow.get(True)) + assert { + "python/lean_pool/documentation.py", + "python/lean_pool/indexes.py", + } <= set(events["push"]["paths"]) + + def test_single_and_sharded_builds_use_validation_cache() -> None: """Both execution paths validate before saving receipts and keep the same gate.""" jobs = yaml.safe_load((WORKFLOWS / "lean_action_ci.yml").read_text())["jobs"] @@ -411,6 +421,8 @@ def scope_repository(tmp_path: Path) -> tuple[Path, str]: ("docs.yml", "lean-toolchain", True), ("docs.yml", "lake-manifest.json", True), ("docs.yml", "python/lean_pool/exposition/generate.py", True), + ("docs.yml", "python/lean_pool/documentation.py", True), + ("docs.yml", "python/lean_pool/indexes.py", True), ("docs.yml", "scripts/exposition/extract-all.sh", True), ("docs.yml", ".github/workflows/docs.yml", True), ("workflow_lint.yml", "LeanPool/Example/Proof.lean", False), @@ -670,6 +682,8 @@ def test_scoped_checks_handle_large_diffs(tmp_path, filename): ("python/tests/test_ci_pr_build.py", "true", "false", True), ('"python/lean_pool/quoted.py"', "true", "false", True), ("scripts/ProjectIndexes.lean", "true", "false", True), + ("scripts/exposition/Extract.lean", "true", "false", True), + ("scripts/exposition/tests/EmbeddedNames.lean", "true", "false", True), (".github/workflows/lean_action_ci.yml", "true", "false", True), ("", "false", "false", True), ("LeanPool/Example/Proof.lean", "true", "true", True),