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