Goal: "fast" webpage updates

Currently, the webpage is updated every 10-15 minutes. This is useful for many purposes, but a noticeable delay. How difficult is it to e.g. ensure that a PR update is reflected on the webpage within 30 seconds?

On a technical level, there are a few hurdles, but this should be possible. It will require significant refactorings, and upgrading the infrastructure for downloading PR metadata, though. Some necessary steps are

• prerequisite: make re-downloading more robust to intermittent failures, by downloading to a temporary file and overwriting the existing data only if that download was successful

• refactor the webpage: make it operate only on aggregate data
  leanprover-community/queueboard#70 does this; the main obstacle is ensuring that PR metadata really stays up to date always.

• refactor the webpage generation, into its own workflow. Use a shallow checkout of just the right aggregate file to make this fast. leanprover-community/queueboard#71 does this

• split the aggregate data files into one file per PR: this way, the metadata for two PRs can be updated without conflicts on timestamps of the generated file

• CI refactor: add a webhook for downloading the metadata for just a single PR. (Use shallow clones to make this really fast.) Switch from gather_stats.sh to running this webhook instead. Challenges: handle merge conflicts. Avoid starting several webhooks if a PR is changed several times in a short time (e.g., making a comment and changing a label).

• To make sure: have a job which periodically checks for out-of-date data (similarly to check_data_integrity.py today). Need to think how re-downloading PRs from that job would avoid conflicts.

• Change the webpage rebuild job, to trigger whenever e.g. a new commit is made to the main branch: this makes the webpage also update with new data.

Start by reading gather_stats.sh and check_data_integrity.py, then review the referenced queueboard issues #70 and #71 for the aggregate-data and webpage-generation approaches. The work is complete when PR updates reliably reach the webpage within 30 seconds, downloads survive intermittent failures, and CI avoids conflicting or redundant updates.