CI: automatically re-download a PR's metadata once its CI finishes

[grunweg]

This is perhaps the last remaining blocker to leanprover-community/queueboard#70 (which is part of #23).

If a PR's CI finishes, github does not register this as an "update": this means that as-is, this repo's data will not automate directly. (It will re-download this after 60 minutes, but this adds a sizable delay.) A better solution is for the failing CI run to notify this repository.

This can be implemented through a github webhook. This webhook would call gather_stats_single.yml (caution: that logic has diverged from download_missing_outdated_prs.sh, make sure to synchronise before landing). Perhaps this repository needs to be transferred to the leanprover-community organisation for this to work.

My knowledge mostly ends here: help with this would be very warmly welcome.

[grunweg]

@grunweg can help with synchronising the logic in the script: the hard(er) part is writing the webhook, and making sure it does not conflict with the other workflow/handling such conflicts well.

[grunweg]

Status update:

• I have updated the gather_stats_single.yml workflow to match the existing logic
• it also uses sparse checkouts (tested and working)

Next/missing steps

• test the workflow downloads everything it needs
• make update_metadata.yml robust against conflicts: call git pull --rebase with automatically overwriting conflicting data; make sure to use a shallow checkout to make this less abyssimally slow
• make the PAT for this workflow a secret on mathlib
• modify mathlib CI to ping this workflow

[vlad902]

Hit an issue I related in person, but to log here: mathlib PR #25188 continued to be marked 'failed CI' for a couple weeks before I noticed, even though I reran CI through the GitHub interface right after it had failed, so queueboard is not aware of those CI updates.

[grunweg]

Thanks for the report! To repeat what I said in person: the issue is that re-running CI doesn't trigger any notion within github that a PR was updated. But fixing this issue should fix it.