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

[Makarius]

Just for the fun of it, here are some timings on truly high-end
hardware: some colleagues have upgraded recently and granted me access
to make some tests.

The results may help others in their hardware decisions.

Here is an Executive Summary:

  * Intel Xeon performs better than AMD
  * fewer NUMA nodes are better
  * SSD file-systems help to save and load heap images fast


Here are some details:

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


Isabelle/eb53f944c8cd + AFP/f7e9efc65d82
ISABELLE_BUILD_OPTIONS="threads=6"


* 64bit: ML_OPTIONS="--minheap 3g --maxheap 30g"

Finished HOL (0:02:21 elapsed time, 0:07:13 cpu time, factor 3.07)

isabelle build -j10 -a -N -f
0:13:37 elapsed time, 5:12:16 cpu time, factor 22.91
0:18:02 elapsed time, 5:57:58 cpu time, factor 19.85

isabelle build -j10 -a -N -f -x HOL-Proofs
0:15:24 elapsed time, 5:11:24 cpu time, factor 20.20
0:14:12 elapsed time, 4:45:27 cpu time, factor 20.10

isabelle build -j10 -g main -N -f
0:07:56 elapsed time, 0:43:58 cpu time, factor 5.53
0:08:07 elapsed time, 0:44:33 cpu time, factor 5.48


* 32bit: ML_OPTIONS="--minheap 1500"

Finished HOL (0:02:10 elapsed time, 0:06:42 cpu time, factor 3.10)

isabelle build -j10 -a -N -f
0:11:13 elapsed time, 3:24:13 cpu time, factor 18.20
0:12:05 elapsed time, 4:07:12 cpu time, factor 20.45

isabelle build -j10 -a -N -f -x HOL-Proofs
0:09:13 elapsed time, 3:37:16 cpu time, factor 23.55
0:09:02 elapsed time, 3:27:56 cpu time, factor 22.99

isabelle build -j10 -g main -N -f
0:07:02 elapsed time, 0:39:45 cpu time, factor 5.64
0:07:02 elapsed time, 0:39:28 cpu time, factor 5.61


isabelle build -j4 -o threads=10 -g main -N -f
0:06:17 elapsed time, 0:46:10 cpu time, factor 7.34
0:05:58 elapsed time, 0:45:26 cpu time, factor 7.60

isabelle build -j6 -o threads=8 -g main -N -f
0:06:40 elapsed time, 0:43:18 cpu time, factor 6.49


When trying out changes of Pure or HOL, I usually test "-g main" first:
it consists of HOL, HOL-Algebra, HOL-Analysis,
HOL-Computational_Algebra, HOL-Library, HOL-Number_Theory,
HOL-Probability, HOL-SPARK, HOL-Word, HOLCF. Afterwards there is a high
chance that all of Isabelle works.

The numbers above are really good for that: 6min and 12min respectively.
These are "quasi-interactive" builds as they should be today.


	Makarius