Better Mathlib build scaling on v4.19.0-rc2

Stream: general

[Jannis Limperg]

PSA: @Sebastian Ullrich's work on theorem-level parallelism speeds up Mathlib builds substantially on systems with many cores. Here are Mathlib build times on AWS c8g instances with different numbers of cores:

Instance type	cores	v4.19.0-rc2	v4.18.0
c8g	16	30m17s	30m15s
c8g	32	17m58s	19m36s
c8g	64	12m49s	16m1s
c8g	96	11m38s
c8g	192	12m51s

So we have no difference on 16 cores, but 32 got somewhat faster and on 64 there's a big difference. 96 and 192 are still not worth it.

I also tested different AWS instance types. c8g (Gravitron, ARM64) seems to be consistently the fastest. For x86, c7a (AMD) is much faster than c7i (Intel) or any of the other c* instances.

(Disclosure: I work for AWS now.)