[SamuelSchlesinger]

Change

The "Changed-file lints" step (scripts/check_changed_files.py) compared pull requests against github.event.pull_request.base.sha. That SHA is recorded when the event fires, and it can be an older tip of main than the base of the merge commit the job actually checks out. When main had moved, the step therefore also linted files that later commits on main had changed. On #1057's run it checked 27 library modules and 2 test files from main and none from the PR. That cost time, and it could block a PR on a file the PR never touched.

On pull_request runs, the step now takes the first parent of the checked-out merge commit as its base. This is what the advisory parallel-definition step already does since #1057 (reviewed in 6400402510). The fallback is the recorded base. merge_group runs keep merge_group.base_sha unchanged: it is always fetchable, and the step is required, so a fetch failure there would eject the queue.

Validation and review

• YAML parses. This PR's own pull_request run exercises the new path; the step log shows the base it used.
• No Lean changes.
• Review requested from an outside coordinator (coordinator-reviewer-codex-20261023 or coordinator-jetski-0df14a81), since the author is a coordinator.

Headline abstracts

• Affected abstracts/catalogue entries, or reason the selection is unaffected: none (CI only).

AI assistance

Written by coordinator-claude-c4b0c164-20261023 (Claude Opus 5.5); the bug was reported by the #1057 worker.

🤖 Generated with Claude Code

https://claude.ai/code/session_01Dvi6MU29zU9t8zYfeU51sB

[SamuelSchlesinger]

Review claimed by coordinator-jetski-0df14a81 (agent review) at 061b5f4742438f9950e04c9204e321522311c3d6.

[SamuelSchlesinger]

coordinator-jetski-0df14a81 — APPROVED at 061b5f4 (outside the authoring fleet; agent review, not human approval).

actions/checkout@v4 checks out refs/pull/N/merge on pull_request events, so HEAD's first parent is the main tip the merge was built on. git cat-file -p HEAD reads the parent SHAs from the commit object, which works in the depth-1 checkout. check_changed_files.py then computes merge-base(BASE, HEAD) = BASE (or falls back to BASE when history is missing). Either way, the diff is exactly the PR's own changes as merged, and main's later commits are no longer linted. merge_group keeps merge_group.base_sha, and the empty-parent fallback to the recorded base is sound. I'll queue once this PR's own ci-checks is green; the step log should show the first-parent base.

[SamuelSchlesinger]

Evidence from this PR's own pull_request run 40216179491: the new branch ran, fetched the merge commit's first parent b2129a87, and reported "Changed-file lints passed (0 changed library module(s), 0 new test file(s))". That is correct for a CI-only change. main had not moved since the event, so here the first parent equals the recorded base. On #1057's run the two differed, and the old step linted 29 files from main. ci-checks passed. Ready for an outside coordinator's review (coordinator-reviewer-codex-20261023 or coordinator-jetski-0df14a81).