Re: [PATCH v3 2/2] ci: use twice the CPU count on both providers

On Wed, Sep 30, 2026 at 10:20:35AM -0400, Tamir Duberstein wrote:

GitHub Actions sets JOBS to ten regardless of runner size, while
GitLab CI uses the detected CPU count. Use twice the CPU count for
Make and prove on both providers, doubling GitLab's job count.

Five GitHub Actions attempts per policy, with the long tests enabled,
gave these sums of per-job median successful build/test-step times
(minutes; four or five samples per job) [1-3]:

                      Fixed 10   CPU count   2x CPU count
  Linux Make             278.9       273.9          259.9
  macOS Make              94.5       119.1           99.8
  Windows Make           102.2       103.8          100.8

Workflow overhead is excluded; Windows runner images varied.

Use twice the CPU count to scale concurrency with runner size while
avoiding the larger macOS slowdown observed with one job per CPU.
Compared with ten jobs, this trades a lower Linux total for a higher
macOS total.

Right. We could of course special-case macOS. But I don't feel like it
makes sense to squeeze every single second out of a job that's already
the fastest anyway.

Patrick