coqbot removed the milestone of a merged PR

[Zimmi48]

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.

[Zimmi48]

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.