These speedups are certainly very impressive! I have wondered what sort of factor could be achieved with enough cores, but was never persistent enough in trying to borrow hardware from people who had it.
Larry > On 2 Jul 2018, at 14:21, Makarius <makar...@sketis.net> wrote: > > 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 _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev