On Mon, Sep 28, 2026 at 06:16:33AM -0400, Tamir Duberstein wrote:
On Mon, Sep 28, 2026 at 2:36 AM Patrick Steinhardt [off-list ref] wrote:
quoted
On Fri, Sep 25, 2026 at 12:35:39PM -0400, Tamir Duberstein wrote:
quoted
GitHub Actions sets JOBS to ten regardless of runner size, while
GitLab CI uses the detected CPU count. Use the CPU count for Make and
prove on both providers, selecting JOBS after the operating system
is identified.
Again, it should be noted here what the effect of this is. In other
words, does GitHub slow down as a result? You already showed numbers
during the discussion on v1 of this series, and these numbers should
probably be included in this message, too.
Agreed, but in this case there was no reliable performance change
across 10 runs; I could include that.
I think it should be included, as it's the one thing that people will be
wondering about when they see this change.
Patrick