The CI is in waiting in the queue

Stream: mathlib4

[Jiang Jiedong]

It seems that current CI jobs are too many and new CI's are waiting in the queue. It shows that Waiting for a runner to pick up this job.... I suspect this is already causing some trouble in slowing down the PR submissions and the review process.

[Bryan Gin-ge Chen]

Yeah, we have 10 self-hosted runners and it looks like they are all active and busy at the moment.

[Jiang Jiedong]

It seems that the current queue is 30 minutes long. But maybe this will be a more serious issue soon.

[Bryan Gin-ge Chen]

At present unfortunately there's not a lot that can be done, but thank you for bringing this up. If this keeps happening it may be possible for us to get more runners, so hearing about a long queue is useful.

[Ruben Van de Velde]

Though also I wouldn't worry too much - I think this happens occasionally, but we recover relatively soon