Lint and audit projects in the build shards, and shard when checkers change

.github/CODE_QUALITY.md

@@ -32,20 +32,29 @@ After the build, it reads Lake's per-module times from the log and fails when a
 the PR adds or modifies took more than 600 s. Times are Lake's wall-clock times on
 GitHub's 4-vCPU runners. Existing files are checked only once a PR changes them.
 
-After all cache and artifact restores, `prepare` removes the compiled outputs
-of the added or modified modules that job is responsible for timing. This happens
-even for a cache produced under the same policy: an untouched file in that cache
-need not have passed the changed-file limit. Each changed module must emit a
-fresh successful build timing in its responsible job; missing timings and cache
-replays fail that check.
+`check` records each changed module's time in a receipt next to its compiled
+output (`<Module>.timing.json`), bound to a hash of that output's `.olean` files.
+After all cache and artifact restores, `prepare` removes the compiled outputs of
+every added or modified module the job is responsible for whose output has no
+matching receipt. So output that was compiled without being timed is always
+rebuilt, even from a cache produced under the same policy: an untouched file in
+that cache need not have passed the changed-file limit. Each changed module must
+then have either a fresh successful build timing from its responsible job or the
+recorded time of the exact output being reused; that time is checked against the
+limit either way, and a module with neither fails the check.
 
 Shards check their assigned modules. Assembly excludes projects listed in the
 same run's shard matrix and checks all remaining changed modules; the canonical
 gate requires every shard and assembly to succeed. Single and rebased root builds
 check all changed modules. Untouched modules can still reuse compiled output.
 
+"Changed" is measured from the main commit the run is tested against: the tested
+merge commit's first parent for a PR, not the event's `base.sha`, which can trail
+main and would count projects merged since as the PR's own.
+
+A later push to a PR restores the outputs of modules whose own source is unchanged
+from that PR's newest successful run; Lake's traces decide which are still valid.
 Reused PR, rebase and queue artifacts must still match `build_time_limits.py`.
-That match does not replace the fresh timing required for a changed module.
 
 The Lean workflow runs on Lean, Lake, project metadata, quality-checker, and workflow changes. It restores and saves Lake caches and pulls Mathlib oleans with `lake exe cache get` when the cache is cold.
 

.github/workflows/lean_action_ci.yml

@@ -97,6 +97,7 @@ jobs:
       reuse_run_id: ${{ steps.plan.outputs.reuse_run_id }}
       previous_head: ${{ steps.plan.outputs.previous_head }}
       queue_build: ${{ steps.plan.outputs.queue_build }}
+      diff_base: ${{ steps.plan.outputs.diff_base }}
     steps:
       - name: Checkout project
         uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd
@@ -162,14 +163,24 @@ jobs:
           # exceeds the kernel's 128 KiB limit on a single environment string.
           changed_files="$RUNNER_TEMP/changed-files.txt"
           : > "$changed_files"
+          # The revision this run's own changes are measured from, for the plan
+          # and for every job's build-time gate.
+          diff_base="$BASE_SHA"
           case "$EVENT_NAME" in
             merge_group)
               git diff --name-only --no-renames "$BASE_SHA"..HEAD > "$changed_files"
               ;;
             pull_request)
-              git diff --name-only --no-renames "$BASE_SHA"...HEAD > "$changed_files"
+              # The event's base.sha can trail main by days, which would count
+              # everything main merged since as this PR's change. The tested
+              # merge commit's first parent is the main tip it merges into.
+              if [ "$(git rev-parse -q --verify 'HEAD^2' || true)" = "$PR_HEAD" ]; then
+                diff_base=$(git rev-parse 'HEAD^1')
+              fi
+              git diff --name-only --no-renames "$diff_base"...HEAD > "$changed_files"
               ;;
             push)
+              diff_base="$BEFORE_SHA"
               if [ -n "$BEFORE_SHA" ] \
                  && ! printf '%s' "$BEFORE_SHA" | grep -q '^0*$' \
                  && git cat-file -e "$BEFORE_SHA" 2>/dev/null; then
@@ -182,6 +193,7 @@ jobs:
               diff_available=false
               ;;
           esac
+          echo "diff_base=$diff_base" >> "$GITHUB_OUTPUT"
           minimal_build=false
           if [ "$EVENT_NAME" = pull_request ] && grep -Eq '^(python/lean_pool/(exposition/|ci_artifacts.py$)|scripts/exposition/|.github/workflows/exposition-verify.yml$)' "$changed_files"; then
             minimal_build=true
@@ -382,12 +394,13 @@ jobs:
       - name: Build project
         id: compilation
         env:
-          BUILD_TIME_BASE: ${{ github.event.merge_group.base_sha || github.event.pull_request.base.sha || github.event.before }}
+          BUILD_TIME_BASE: ${{ needs.plan.outputs.diff_base }}
         run: |
           set -euo pipefail
-          # Always rebuild this job's changed files after every cache/artifact
-          # restore. A same-policy cache need not have timed them while changed.
-          # `check` requires fresh timings; `watch` retains the 60-minute limit.
+          # After every cache/artifact restore, `prepare` forces a rebuild of
+          # each changed file whose restored output has no recorded build time,
+          # so `check` judges a time measured in CI for every changed file.
+          # `watch` retains the 60-minute limit.
           time_base=""
           if [ -n "$BUILD_TIME_BASE" ] && ! printf '%s' "$BUILD_TIME_BASE" | grep -q '^0*$' \
              && git cat-file -e "$BUILD_TIME_BASE" 2>/dev/null; then
@@ -615,10 +628,30 @@ jobs:
             echo "Mathlib already present from cache"
           fi
 
+      - name: Install uv
+        uses: astral-sh/setup-uv@d0d8abe699bfb85fec6de9f7adb5ae17292296ff
+        with:
+          enable-cache: true
+
+      - name: Reuse compiled files from this PR's successful runs
+        if: github.event_name == 'pull_request' && steps.cache.outputs.cache-hit != 'true'
+        continue-on-error: true
+        env:
+          GH_TOKEN: ${{ github.token }}
+          PR_NUMBER: ${{ github.event.pull_request.number }}
+          PR_BRANCH: ${{ github.head_ref }}
+          PR_HEAD: ${{ github.event.pull_request.head.sha }}
+          PR_BASE: ${{ github.event.pull_request.base.sha }}
+          CURRENT_RUN: ${{ github.run_id }}
+        run: >-
+          PYTHONPATH=python uv run --project python --locked python -m lean_pool.ci_pr_build
+          --number "$PR_NUMBER" --branch "$PR_BRANCH"
+          --head "$PR_HEAD" --base "$PR_BASE" --current-run "$CURRENT_RUN"
+
       - name: Build this shard's projects
         env:
           PROJECTS: ${{ matrix.projects }}
-          BUILD_TIME_BASE: ${{ github.event.merge_group.base_sha || github.event.pull_request.base.sha || github.event.before }}
+          BUILD_TIME_BASE: ${{ needs.plan.outputs.diff_base }}
         run: |
           set -euo pipefail
           touch "$RUNNER_TEMP/build-stamp"
@@ -631,9 +664,10 @@ jobs:
               | tr '\n' ' ')
             modules="$modules $project_modules"
           done
-          # Always rebuild this job's changed files after every cache/artifact
-          # restore. A same-policy cache need not have timed them while changed.
-          # `check` requires fresh timings; `watch` retains the 60-minute limit.
+          # After every cache/artifact restore, `prepare` forces a rebuild of
+          # each changed file whose restored output has no recorded build time,
+          # so `check` judges a time measured in CI for every changed file.
+          # `watch` retains the 60-minute limit.
           time_base=""
           if [ -n "$BUILD_TIME_BASE" ] && ! printf '%s' "$BUILD_TIME_BASE" | grep -q '^0*$' \
              && git cat-file -e "$BUILD_TIME_BASE" 2>/dev/null; then
@@ -683,6 +717,44 @@ jobs:
           if-no-files-found: ignore
           retention-days: 1
 
+      # Lint and audit this shard's projects here, in parallel with the other
+      # shards, instead of one after another in `finalize`. Only passes are
+      # handed on: `finalize` recomputes every fingerprint and runs whatever
+      # has no matching pass, so a failure here is reported there.
+      - name: Restore project validation
+        uses: actions/cache/restore@27d5ce7f107fe9357f9df03efb73ab90386fccae
+        with:
+          path: .lake/validation-cache/v1
+          key: LeanValidation-v1-${{ runner.os }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json', 'lakefile.toml') }}-${{ github.sha }}
+          restore-keys: |
+            LeanValidation-v1-${{ runner.os }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json', 'lakefile.toml') }}-
+
+      - name: Install validation dependencies
+        continue-on-error: true
+        run: cd python && uv sync --locked
+
+      - name: Lint and audit this shard's projects
+        id: shard-validation
+        continue-on-error: true
+        env:
+          PROJECTS: ${{ matrix.projects }}
+        run: |
+          cd python
+          # shellcheck disable=SC2086 # word-split the project list on purpose
+          uv run python -m lean_pool.shard_validation --repo .. --units $PROJECTS
+
+      - name: Upload validation passes
+        if: always() && steps.shard-validation.outcome != 'skipped'
+        continue-on-error: true
+        uses: actions/upload-artifact@ea165f8d65b6e75b540449e92b4886f43607fa02
+        with:
+          name: ci-validation-${{ matrix.shard }}
+          path: .lake/validation-cache/v1/passes.json
+          include-hidden-files: true
+          if-no-files-found: ignore
+          compression-level: 1
+          retention-days: 1
+
   finalize:
     needs: [plan, shard]
     # Run even when a shard failed: merging what succeeded and building the
@@ -817,15 +889,16 @@ jobs:
       - name: Build project
         id: compilation
         env:
-          BUILD_TIME_BASE: ${{ github.event.merge_group.base_sha || github.event.pull_request.base.sha || github.event.before }}
+          BUILD_TIME_BASE: ${{ needs.plan.outputs.diff_base }}
           # This run's shards already compiled and timed these projects'
           # changed files, so assembly neither rebuilds nor re-times them.
           SHARD_PROJECTS: ${{ join(fromJSON(needs.plan.outputs.matrix).include.*.projects, ' ') }}
         run: |
           set -euo pipefail
-          # Always rebuild this job's changed files after every cache/artifact
-          # restore. A same-policy cache need not have timed them while changed.
-          # `check` requires fresh timings; `watch` retains the 60-minute limit.
+          # After every cache/artifact restore, `prepare` forces a rebuild of
+          # each changed file whose restored output has no recorded build time,
+          # so `check` judges a time measured in CI for every changed file.
+          # `watch` retains the 60-minute limit.
           time_base=""
           if [ -n "$BUILD_TIME_BASE" ] && ! printf '%s' "$BUILD_TIME_BASE" | grep -q '^0*$' \
              && git cat-file -e "$BUILD_TIME_BASE" 2>/dev/null; then
@@ -911,6 +984,21 @@ jobs:
           PYTHONPATH=python uv run --project python --locked python -m lean_pool.queue_build
           --base "$BASE_SHA" --head "$HEAD_SHA" --receipts
 
+      - name: Download shard validation passes
+        continue-on-error: true
+        uses: actions/download-artifact@d3f86a106a0bac45b974a628896c90dbdf5c8093
+        with:
+          pattern: ci-validation-*
+          path: ${{ runner.temp }}/shard-validation
+
+      - name: Merge shard validation passes
+        continue-on-error: true
+        env:
+          FRAGMENTS: ${{ runner.temp }}/shard-validation
+        run: >-
+          PYTHONPATH=python python3 -m lean_pool.validation_cache merge
+          "$FRAGMENTS"
+
       - name: Lint
         run: |
           cd python
@@ -1092,12 +1180,13 @@ jobs:
 
       - name: Build combined Lean root
         env:
-          BUILD_TIME_BASE: ${{ github.event.merge_group.base_sha || github.event.pull_request.base.sha || github.event.before }}
+          BUILD_TIME_BASE: ${{ needs.plan.outputs.diff_base }}
         run: |
           set -euo pipefail
-          # Always rebuild this job's changed files after every cache/artifact
-          # restore. A same-policy cache need not have timed them while changed.
-          # `check` requires fresh timings; `watch` retains the 60-minute limit.
+          # After every cache/artifact restore, `prepare` forces a rebuild of
+          # each changed file whose restored output has no recorded build time,
+          # so `check` judges a time measured in CI for every changed file.
+          # `watch` retains the 60-minute limit.
           time_base=""
           if [ -n "$BUILD_TIME_BASE" ] && ! printf '%s' "$BUILD_TIME_BASE" | grep -q '^0*$' \
              && git cat-file -e "$BUILD_TIME_BASE" 2>/dev/null; then

python/ci-performance.md

@@ -37,6 +37,45 @@ checkout, never the artifact paths. So every CI build step is followed by
 artifact lists, and preserves
 modification times, so shard packaging still ships only fresh files.
 
+### Incremental PR pushes
+
+Until November 2026 every run recompiled every file a PR changed relative to
+main, to time it against the 600 s limit. A PR that adds a 1,300-file project
+therefore recompiled all of it (about 38 minutes on a 4-vCPU runner) on each
+push, in the merge queue, and again on main, even when a push edited a handful
+of files.
+
+Now `build_time_limits check` writes a `<Module>.timing.json` receipt beside each
+changed module's output, bound to a hash of its `.olean` files, and `prepare`
+only invalidates changed modules without a matching receipt. Receipts travel
+with every artifact that carries the outputs themselves. `ci_pr_build` restores
+the unchanged-source modules of the PR's newest successful run, so a later push
+compiles only what it edited and whatever Lake's traces say depends on it.
+
+The plan and the build-time gate also measure a PR's changes from the tested
+merge commit's first parent. The event's `base.sha` can trail main by days,
+which made every project merged since look changed and be rebuilt.
+
+### Validation in shards
+
+Lint and the quality audits reuse per-project pass receipts, so an ordinary PR
+validates only the project it touches. A change to any checker input (the
+workflow, `validation_cache.py`, `quality.py`, the no-lint lists, the pins)
+invalidates every receipt. One job then linted the pool for about 36 minutes and
+audited it for about 68, one project at a time.
+
+In-job concurrency does not fix that: PR #785 measured that a single lint
+process already saturates a 4-vCPU runner. Instead the planner now shards the
+whole pool when checker inputs change, even with a warm build cache, and every
+shard job lints and audits the projects it built
+(`python -m lean_pool.shard_validation --units ...`). Shards upload only their pass receipts.
+`finalize` merges them (`validation_cache merge`) and then runs the unchanged
+Lint and quality steps, which recompute every fingerprint, reuse matching passes,
+and run anything a shard did not pass. A shard's validation step can therefore
+neither fail nor pass the run by itself.
+
+`MAX_SHARDS` is 14: beyond that the costliest project fills a shard alone.
+
 Documentation retains its separate, integrity-checked SQLite checkpoints. They
 still depend on available cache capacity; this change reduces duplicate data
 instead of changing the repository's paid storage limit.