Closed fatho closed 10 months ago
Referencing the next steps for this issue here to keep a coherent log: https://github.com/channable/hoff/commit/39f3595ca6625ad6890790fe5fe0c032543d3199#r105710903
Fixed by #209, which ironically was itself affected by the bug
This still appears to happen. However, instead of sleeping more and more, perhaps we could instead wait for the "branch updated" webhook before pushing master?
EDIT: Should read before I comment, Bert suggested the same, so to elaborate a bit more on that:
We already even handle the webhook events from GitHub when the commit corresponding to a PR changes. In most cases, that causes hoff to abandon the PR, but we already specifically check whether the updated commit SHA corresponds to the commit we pushed ourselves for integrating the PR:
https://github.com/channable/hoff/blob/bbedc31af3ee6df7693efeb005775c06a7545ac4/src/Logic.hs#L424
So maybe we could make hoff wait for that webhook after force-pushing the branch, and only upon receiving it continue with the push of the merge commit to master. It's a bit more complicated though, because currently, the push sequence happens sequentially as part of a single action, which is handled in a different place than the webhook events:
One way to do this would be to split up the action into to, and incorporate waiting on the PR change webhook into the PR state machine, but this all appears to become quite complex :sweat_smile:
Perhaps we also need some sort of timeout there, too, after which we just proceed to push master anyway. Otherwise we have yet another webhook on the critical path and thus increase our chance of stalls when GitHub has webhook issues.
Occasionally, it happens that a PR merged by hoff ends up showing as closed rather than merged, i.e. rather than
And sometimes, github just doesn't close the PR at all.
In hoff, the merging procedure is defined here:
https://github.com/channable/hoff/blob/46805f05a0c23ee1bac5be786da1acd23d076ce3/src/Logic.hs#L203-L210
We first force-push the rebased version of the original branch, and then push the merge to master.
That way, GitHub should see that the commits in the PR branch are exactly those that are on master, and correctly close the PR as merged. This is just like a human would do a rebase & merge via the
git
command line (i.e. not using GitHub's interface for that), albeit a lot faster.The latter point might actually be the issue here. My hypothesis is that if the force push of the PR branch and the push to master are sent in rapid succession, GitHub might become confused about the state of the branches, and incorrectly observe a state where the commits that were merged are not yet on the PR branch.
A hacky band-aid could be to just sleep for a few seconds between force-pushing the PR branch and pushing master.