[isabelle-dev] Jenkins maintenance

[Lars Hupel]

> I have just used the new Jenkins testboard for the first time, and was a
> bit disappointed by the very long runtimes: about 1.5h each for Isabelle
> and AFP.

This is slightly misleading, because the total time spent waiting for
both is typically 1:30 hours; Jenkins runs them in parallel if possible.
The last three or so testboard runs didn't spend time waiting in the queue.

> Mira set out to deliver Isabelle tests "In 10min!" (Bavarians need to
> think of the famous Stoiber speech here).
> 
> I am doing manual Isabelle tests on my own machin in approx. 30min,
> which is already a bit painful. 20min is OK, 10min would be delightful.

Here's my quick back-of-the-envelope calculation:

Our current testboard setup runs AFP with -j8 -o threads=2, that is, on
16 cores. It requires an elapsed time of 1:30 and 20:30 CPU hours.

Isabelle "build -a" runs with -j3 -o thread=2 (total 6 cores), with an
elapsed time of 1:20 and 6:45 CPU hours.

Let's just discount multithreading overhead for a bit here (it's two
threads per process anyway). We're getting a total of about 27 CPU
hours, give or take.

In order to process that full workload in 30 minutes, that would require
in the order of 50 cores with full load. We're close with a total of 44
cores. But for fairness, we're running the workload not on the full
number of cores, but rather just half.

In any case, I don't see how anything less than 30 minutes can be done
with reasonable hardware. And if at some point there are enough
improvements that it can be done on hardware, it's orthogonal to
Mira/Jenkins/whatever ...

Cheers
Lars