Repository navigation
T99: push a verified fix to your own pull request - #83
Merged
Merged
Conversation
"Verify the fixed commit" verified the PR's current GitHub head, but the fix only lived under the local refs/proofmerge/fix/, so it checked the same commit and gave the same BLOCK. `proofmerge push-fix` builds one commit from every verified fix on the head the run checked and pushes it to the PR branch without force. It refuses unless the PR is open, still at that commit, not from a fork and opened by the signed-in gh account. The app gets "Push the fix to PR #N as @account" with a confirm, and the old button reads "Verify PR #N again". Jobs with no title (approve, Ponytail, push-fix) showed "undefined: failed"; they have titles now.
Codex Review SummaryThis comment shows the latest Codex review activity on this pull request.
ℹ️ About Codex in GitHubYour team has set up Codex to review pull requests in this repo. Reviews are triggered when you
Codex reacts with 👀 while any review is running, comments if it has suggestions, and reacts with 👍 once all reviews finish with no findings. |
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.
Why
On a BLOCK run with verified fixes, Verify the fixed commit verified the pull request's current GitHub head. The fix lived only under the local
refs/proofmerge/fix/, and nothing pushed it, so the button checked the same commit again and gave the same BLOCK.What
proofmerge push-fix <proof.json> --pr N --repo R [--dry-run]builds one commit from every verified fix. It refuses when two fixes change one file differently. The commit's parent is the head the run checked, and it goes to the PR's branch without force. It refuses unless all of these hold:ghaccount opened the PR.For anyone else's PR, post the fix instead. Each fix was checked alone, so the output says to verify again.
App changes:
Checked
tests/test_push_fix.py:--force.Not checked
/).