GitHub CI queuing

[andres-erbsen]

I've started noticing that it takes 15min+ for non-basic checks to start, even though they are queued:

I don't understand why this would happen yet, but I guess I can still write down the annoyance.

[JasonGross]

GitHub runners are shared between all repositories of an organization. I believe GitHub allocates 20 runners to each organization (not 100% sure about this, I've only verified this on my personal account). Checks are only queued once all dependencies complete, and are processed in order. I've seen wait times of 16+ hours on Fiat Crypto if I push a bunch of PRs simultaneously.

[Zimmi48]

We could perhaps look into whether GitHub does open source sponsoring by allowing more concurrent runners.

[andres-erbsen]

On our side, one thing I can think of is that we could stop testing reverse dependencies of stdlib on the previous rocq release.

[andres-erbsen]

There might be something more subtle going on with dynamically generated jobs. The Alpine-based quick build job I recently added does not seem to get delayed.

[JasonGross]

Is there something going on that's not explained by "Checks are only queued once all dependencies complete" + max 20 simultaneous jobs? The behavior I'd expect to see is that the static jobs with no dependencies run, and then initial dynamic jobs (up to 20) run, and the rest get queued. Are you seeing some other behavior?

[andres-erbsen]

I'm not sure how to check simultaneous jobs, but the above screenshot shows that there are no running jobs and yet some are queued (but they can't be waiting on dependencies because no jobs are running).

[JasonGross]

there are no running jobs

You have to check for running jobs across all repositories in the rocq-prover organization: https://github.com/organizations/rocq-prover/settings/actions/hosted-runners