queue missing PRs

Stream: mathlib4

[Michael Rothgang]

I noticed a curious issue with the (Github-search based) #queue: sometimes, PRs which have perfectly passing CI don't show up on it.

For example, #18221 and #18222 were both not shown on the page. (They were submitted 3 hours ago, passed CI 30 minutes later, but did not appear.) Re-running some CI job on one of them made both appear. I do not know why.
These are not the only ones.

Removing the "status:success" from the search query shows the PR, so the issue really seems to be about github not noticing that CI had passed. Was there a github outage some time ago?

[Michael Rothgang]

https://www.githubstatus.com/ doesn't show any for today...

[Michael Rothgang]

I found another instance of this: #17435, #18430 and #18589 each have passing CI, but #queue doesn't show them yet. (The queueboard does.)

@Arend Mellendijk suggested this might be a caching issue on github's side --- that the "search open PRs" features operates on a different version database, which could take some time to re-synchronise. Distributed databases are hard.