Repository navigation
feat(gauntlet): push lints only; full gauntlet once at merge with a tree-hash pass cache (GH #735) - #740
Merged
Conversation
…e by tree (GH #735) pre-push keeps ref parsing, the develop refusal and the overlap check, then lints only the files the pushed commit changed (scripts/_lib/gauntlet-lint.sh, shared with run-gauntlet.sh's lint layer): no tests, no gauntlet queue. MH_PREPUSH_FULL=1 runs the old queued full gauntlet. merge-pr.sh and sync-pr-head.sh run the full gauntlet themselves, under the gauntlet lock, on the exact tree they push and merge, before the push (sync-pr-head.sh also on an already-synced head). A full, clean, passing run-gauntlet.sh records ~/.cache/mh/gauntlet-pass/<HEAD^{tree}>; both scripts skip the run on a hit. GAUNTLET_PASS_CACHE=0 neither reads nor writes it.
…push # Conflicts: # scripts/gate-differential.sh # tests/scripts/test-pre-push-refs.sh
…pass for its tree (GH #735) A push only lints now, so the cloud path's guarantee that the merged tree passed the full gauntlet rests on sync-pr-head.sh. --verify makes it enforced: it refuses unless a pass is cached for <head>^{tree} (GAUNTLET_PASS_DIR), naming sync-pr-head.sh or a clean run-gauntlet.sh as the way to get one. GAUNTLET_PASS_CACHE=0 means no cache satisfies it.
- gauntlet_pass_start records nothing unless the cwd is the checkout's top (a non-repo copy in an ignored dir keyed on the enclosing checkout's tree), and counts untracked files even with status.showUntrackedFiles=no (also merge-pr.sh's two clean checks). - merge-pr.sh refuses when HEAD moved off $head during the gauntlet (status stays clean on a commit). - gauntlet_full unsets GAUNTLET_SHARD so a leftover shard cannot pass a partial run. - gauntlet-lint.sh matches a literal dot as [.]: awk -v turned '\.sh$' into '.sh$'. - lock-owner docs: the child skip applies with MH_PREPUSH_FULL=1, not to a plain push.
…push # Conflicts: # docs/reference/repo-gotchas.md # scripts/gate-differential.sh
gauntlet_pass_has shared by gauntlet_full and merge-pr.sh --verify; _lint_existing; gauntlet_pass_start returns on a missing HEAD with a reason; codex-integration-map and the pipefail lint comment name the new lint-at-push, gauntlet-at-merge split and _lint_pick.
Owner
Author
|
Fresh-context re-review of the clean-up commit 5cb2638, done by a separate agent on a clean checkout. The commit changes 5 files (+11/-8) and makes only the five listed clean-ups:
Earlier full-gauntlet PASS and two-axis MERGE reviews were done at 64bb153. This commit has no behaviour change on top of that. Fresh-context review: MERGE @ 5cb2638 |
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
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.
Closes #735
Summary
Evidence
HEAD^{tree}.GAUNTLET_SHARD,status.showUntrackedFiles=no, an awk regex escape, doc wording). All fixed in 35501e5; each fix's test fails when the fix is reverted.Merge Danger
Door: two-way (revert restores the full pre-push gauntlet)
Blast Radius: merge-gate
The only full-gauntlet gate moves from pre-push to
merge-pr.sh/sync-pr-head.sh. A merge made outside those (e.g. the GitHub web UI) gets only the lint, as it already got nothing from a push made elsewhere. Pre-existing, not added here: between the last develop fetch andgh pr merge, a merge that bypasses the merge lock can move develop; GitHub's "require branches to be up to date" setting would close that and is the operator's call.core.hooksPathmust stay relative (git-hooks) for each worktree to run its own hook; it was found absolute (pointing at the main checkout, then on an old develop) on 2026-10-27 and was reset.