Waiting for a runner

Stream: mathlib4

[Michael Stoll]

The "Build (fork)" CI step on #33893 shows

Waiting for a runner to pick up this job...

since about 1 hour. This does not look normal...

[Junyan Xu]

This is happening more often lately, perhaps due to #mathlib4 > slow linting step CI? @ 💬 wasting a lot of runner hours ...

[Bryan Gin-ge Chen]

Right -- until that gets fixed maybe we need a job to cancel those automatically...

[Thomas Murrills]

I'm vaguely curious what happens if we call IO.Process.exit 0 at the end of main in runLinter. It shouldn't have any effect, but the process is not exiting as-is, so I wonder if it actually would...

Ideally we find out why this is happening instead of just patching around it, though.

But, should we try it and see what happens, if anything? Or should we try to do more debugging first? (We could also do it under e.g. a debugging-only flag that we could turn off for testing if we try to replicate the issue, either in isolation or CI.)

[Bryan Gin-ge Chen]

I wouldn't be opposed to trying more things to get to the bottom of this!

[Moritz Doll]

How many runners are doing the normal CI testing? At the moment it seems like there are only 5, which feels very few. Reason is that I have PRs that waited for 2.5hrs to get picked up and that in the middle of the day in AU, which should be low volume (unless all of Europe does their mathlib coding at night). None of the running PRs seem to be hanging on the linting step.

[Bryan Gin-ge Chen]

I'm taking a look now. We did take one runner offline to devote to trying to reproduce the stuck linting step in a debug environment.