fix: build PR diffs with git and bind merge verdicts to the reviewed merge base - #146
Merged
Merged
Conversation
GitHub refuses `gh pr diff` for a PR touching more than 300 files (HTTP 406: Sorry, the diff exceeded the maximum number of files (300)), which broke the merge-only job on a Lean toolchain bump and would break reviews. Such bumps are exempt from TauCeti's size cap, so they recur. Add runner/pr_diff.py, which fetches the merge base and the head by SHA into a throwaway bare repository (blobless, depth 1, anonymous HTTPS, user and system git config ignored) and runs `git diff` on them. The review, shadow-review and merge-only workflows, the local CLI and the merge sweep all use it, so every path produces the same bytes for the same head, which the patch digest and the changed-path check rely on. The diff is also now bound to the resolved HEAD_SHA rather than whatever the head is when `gh pr diff` runs. The output matches `gh pr diff` byte for byte on TauCeti's Lean sources, including renames, deletions, binary files and missing trailing newlines. It differs only in hunk-header section labels for files GitHub gives a language-specific diff driver (Python, BibTeX), so an approval recorded against a gh-built diff of such a PR is re-earned once instead of carried forward. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
…paths from git The merge gate matched a scoreboard to the PR only by head SHA, but the diff under a head changes if the PR is retargeted or its base history is rewritten. The diff is determined by (merge base, head), and every scoreboard since June has recorded the merge base it reviewed against (`merge_base_sha`, from the same compare API the merge job asks), so decide_from_comments now requires it to equal the merge base now, and fails closed when either is missing. It is stable while main merely advances. All 20 open TauCeti PRs with a current-head scoreboard record a matching merge base, so this costs no re-reviews. Changed paths feeding a merge decision (merge-only, the sweep and review.py's merge decision) are now machine-read by pr_diff.py (`git diff --name-only -z`, NUL-separated) instead of parsed from patch headers, where git quotes names with control or non-ASCII bytes and the parser dropped them. Without renames a rename lists as the deletion and addition of its two paths, the same set the headers gave, and git needs no file contents for it. pr_diff.py now bounds every git call with a timeout that kills git's whole process group, streams the diff and path list under a 64 MiB limit (the 909-file mathlib4 #3780 diff is 5.7 MB), removes a partial output on failure, and runs git with an allowlisted environment, so no token, provider key, askpass or ssh helper reaches it. shadow-review.yml takes the helper from its own commit rather than falling back to `gh pr diff` for an older pinned engine. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
kim-em
changed the title
… threads by machine paths pr_diff.py bounded git's output but not what git downloaded: the diff fetched missing blobs lazily, so a PR of huge binary files could fill the disk behind a tiny "Binary files differ" patch. It now fetches the two commits' trees, then exactly the changed files' blobs (listed with `git diff --raw`) in one explicit fetch, and runs every diff and listing with GIT_NO_LAZY_FETCH=1 so nothing else is ever downloaded. A watchdog kills git once the repository passes 256 MiB, checked again when git exits; mathlib4 #3780 (909 files) needs about 6 MB. The merge gate checked the merge base when deciding, but the final race check before enqueue in merge-only.yml and the sweep re-read only the head, and enqueueing binds only the head. Both now re-read the PR's current base and its merge base with the head immediately before acting, and dequeue or skip if it moved; the sweep also skips a PR no longer targeting main. Review threads now anchor to the machine-read path list (review.py --paths-file, also passed by the CLI), so a finding on a file whose name git quotes in patch headers anchors to it. review.yml, shadow-review.yml and the CLI stop before reviewing when the merge base cannot be resolved, since a scoreboard recorded without one can never merge. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
…ter enqueue In merge-only.yml, a failed base or compare read aborted the step under `set -e` (and an empty merge base exited) without dequeueing, so an already-queued PR stayed queued though its reviewed merge base could no longer be verified. The re-check is now a function whose reads cannot abort: a moved merge base dequeues, and an unreadable one dequeues and then fails the step. It runs before the enqueue mutation and again right after it, since the mutation binds only the head. The sweep does the same after enqueueing: a moved or unreadable merge base dequeues at once (it never enqueues on a failed pre-check). pr_diff.py's timeout and disk watchdog now kill git only while it is unreaped: they check a flag under a lock, git's exit is awaited without reaping (waitid WNOWAIT) until that flag is set, and the watcher thread is joined, so a recycled PID is never signalled. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
This PR adds
runner/pr_diff.pyand uses it inreview.yml,shadow-review.yml,merge-only.yml, the local CLI and the merge sweep in place ofgh pr diff, which GitHub refuses for PRs touching more than 300 files (could not find pull request diff: HTTP 406: Sorry, the diff exceeded the maximum number of files (300)). That refusal broke the merge-only job on TauCetiProject/TauCeti#8856 (chore: bump to Lean v4.35.0-rc3 and adapt to current mathlib master), and TauCeti now exempts Lake-pin bumps from its size cap, so such PRs will recur.The helper fetches the merge base and the head by SHA into a throwaway bare repository (blobless, depth 1, anonymous HTTPS, no work tree, global and system git config ignored, an allowlisted environment with no tokens, provider keys, askpass or ssh helpers) and writes the
git diffbetween them, plus the changed paths machine-read withgit diff --name-only -z. Only the two commits' trees and then exactly the changed files' blobs are downloaded, with git's lazy fetching off and the total capped at 256 MiB; every git call has a timeout that kills git's process group, and output is streamed under a 64 MiB limit. The PR's own.gitattributesis never read. The output matchesgh pr diffbyte for byte on TauCeti's Lean sources, including renames, deletions, new and binary files and missing trailing newlines; it differs only in hunk-header section labels for files GitHub diffs with a language-specific driver (Python, BibTeX) and, for repositories larger than TauCeti, the abbreviation length ofindexblob ids, whichpatch_digestignores. An approval recorded against a gh-built diff of a PR touching such files is therefore re-earned once rather than carried forward.shadow-review.ymltakes the helper from its own commit, so an older pinned engine gets the same diff.The merge decision (
merge_from_scoreboard.py, shared by merge-only and the sweep) now also requires the scoreboard's recordedmerge_base_shato equal the PR's merge base now, failing closed when either is missing, and merge-only and the sweep re-read the merge base immediately before enqueueing, so a verdict cannot outlive a retarget or a rewrite of the base history under the same head. The review workflows and the CLI stop before reviewing if the merge base cannot be resolved. Scoreboards have recorded that field since the provenance work in June. Merge decisions and review-thread anchors read the machine path list rather than parsing patch headers, where git quotes names with control or non-ASCII bytes. TauCeti's pins of these workflows need bumping for the fix to take effect there.🤖 Prepared with Claude Code