> 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 _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev