[isabelle-dev] Isabelle build timing on high-end hardware

Makarius makarius at sketis.net
Sat Jul 28 19:25:14 CEST 2018

On 02/07/18 15:21, Makarius wrote:
> 2 * Intel(R) Xeon(R) Gold 6148 CPU @ 2.40GHz;
> 2 NUMA nodes: distance factor 2.1 for memory access;
> each CPU with 20 cores and hyper-threading: total of 80 hardware threads
> 256 GB SSD
> Ubuntu Linux 16.04

Here are more timing results on that great machine of some Isabelle users:

  ML_OPTIONS="--minheap 1500"

isabelle build -o threads=6 -j10 -a -N -d '$AFP' -f -x HOL-ODE-Numerics
-X slow
0:36:19 elapsed time, 19:13:18 cpu time, factor 31.75

Note that the sessions starting from HOL-ODE-Numerics are relatively
slow, but insignificant for a meaningful test: ignoring them like the
"slow" group leads to very good results, below the critical "Paris
Commuter constant".

It is even slightly better than the 45min from 2012, when "isabelle
build" was new and that expression came up in Paris Sud. Shortly
afterwards we've had a lot of activity on Isabelle + AFP, as a
consequence of renovations of Isabelle/Pure/HOL + libraries -- when
testing was fun.


More information about the isabelle-dev mailing list