CI runner specs

Stream: CI

[Jireh Loreaux]

Can someone give me the (approximate) specifications for the CI runners? And how many do we have? I'm interested in what it would take to get my university to supply one or two.

[Bryan Gin-ge Chen]

I think @Gabriel Ebner might be the person to ping?

[Gabriel Ebner]

I've been trying to hand off the maintenance of the CMU machines to @Wojciech Nawrocki, so I'll let him answer that.

[Bryan Gin-ge Chen]

I just noticed Wojciech isn't subscribed to this stream, so he didn't get the ping. I'll send him a PM with a link.

[Wojciech Nawrocki]

@Jireh Loreaux the machines at CMU have 12-core Intel(R) Xeon(R) Gold 6126 CPU @ 2.60GHz CPUs, 32G RAM and about 40G of disk space each. I think they are dedicated rather than virtual. There are currently 8 of them. I believe that if the mathlib queues start getting too long, we would also be able to start up more.

[Wojciech Nawrocki]

There are also Freiburg machines, but it looks like they are not currently registered as CI runners for leanprover-community due to some technical issues.

[Bryan Gin-ge Chen]

We disabled the Freiberg machines since they were no longer able to reliably build mathlib without failing (see this thread). As far as I know we still haven't looked into the precise root cause.