coqbot removed the milestone of a merged PR
Opened this issue · 1 comments
coqbot normally automatically removes the milestone of PRs that are closed without being merged.
It looks like it very rarely happens (I have seen only two examples: coq/coq#15845 and coq/coq#16794) that coqbot does that for a merged PR.
By looking at the recent case, I could determine that the problem comes from GitHub's webhooks. I've filled a bug at GitHub:
Description
My GitHub App (coqbot-app) has received a webhook delivery for a "pull request closed" event on 2022-11-17 for which the webhook payload contained some inconsistent information.
Reproduction Steps
This is not reproducible, but the "id"
of the webhook delivery is 33535994659
and the "guid"
is "880bdf90-665b-11ed-9a04-f9c1589ce4f8"
. This likely happened once in the past (on 2022-03-25) given the behavior of the bot at the time, but it is too ancient to be able to dig the webhook delivery logs.
Logs
As shown in this extract below (I skip many irrelevant lines of the payload), the "action"
is "closed"
but the "state"
of the pull request is "opened"
, the "closed_at"
and "merged_at"
fields are null
and the "merge_commit_sha"
is "ab373fb63f2c62098f95bc55246165db60773e51"
:
"payload": {
"action": "closed",
"number": 16794,
"pull_request": {
"state": "open",
"created_at": "2022-11-12T14:58:26Z",
"updated_at": "2022-11-17T09:37:55Z",
"closed_at": null,
"merged_at": null,
"merge_commit_sha": "ab373fb63f2c62098f95bc55246165db60773e51",
Currently, coqbot relies on "merged_at"
not being null
to know that a PR was merged. If the bug happens again, we could look at "merge_commit_sha"
as a back-up, or at "closed_at"
to learn that something is off.
This happened again today: coq/coq#16837 (comment)
The issue with the webhook was the same.
The "merge_commit_sha"
is irrelevant (it exists even for unmerged PRs).
There is a "merged"
field, but it is also reporting something wrong (it is false
when it should be true).
So the only thing we can do as a workaround is have a look at "closed_at"
to learn that something is off. In this case, we may retrieve the merge state of the PR with a query and an exponential backoff strategy.