Recompile only what a PR push changed, and measure changes from current main

.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,31 @@ jobs:
             echo "Mathlib already present from cache"
           fi
 
+      - name: Install uv
+        if: github.event_name == 'pull_request'
+        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 +665,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
@@ -817,15 +852,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
@@ -1092,12 +1128,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,25 @@ 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.
+
 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.