Skip to content

pre-push: gate a commit whose tree does not track the contract - #47

Open
mgillr wants to merge 1 commit into
mainfrom
gate-copies-untracked-contract
Open

mgillr wants to merge 1 commit into
mainfrom
gate-copies-untracked-contract

Conversation

@mgillr

@mgillr mgillr commented Oct 21, 2026

Copy link
Copy Markdown
Collaborator

A contract that keeps proofline.json untracked (scope allow-lists exclude it, hygiene requires it untracked) can never pass hookPrePush: gateAtCommit builds a worktree of the pushed commit, and a fresh worktree never contains an untracked file, so every gate refuses with "no proofline.json (run: proofline init)".

The fix copies the root's proofline.json into the fresh worktree when the commit does not track one, so the gate verifies the commit against the same contract bytes the root gates. Tracked contracts are untouched; nothing else changes.

Measured red-green on a real repo holding such a contract: before the patch the push refuses for every commit; after it the per-commit gate runs and passes.

The contract deliberately stays untracked: scope and hygiene keep
proofline.json out of the tree, so a pushed commit does not carry it.
gateAtCommit materialized a worktree of the commit and refused with
"no proofline.json" because the fresh worktree never holds an untracked
file. Copy the root's contract into the worktree when the commit does
not track one, so the gate runs against the same bytes the root gates.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant