*** System *** * The command-line tool "isabelle build" supports option -N for cyclic shuffling of NUMA CPU nodes. This may help performance tuning on Linux servers with separate CPU/memory modules.
* The system option "threads" (for the size of the Isabelle/ML thread farm) is also passed to the underlying ML runtime system as --gcthreads, unless there is already a default provided via ML_OPTIONS settings. This refers to Isabelle/8eb6365f5916. Here are some examples on lxbroy10: ML_PLATFORM="x86-linux" ML_HOME="/home/isabelle/contrib/polyml-5.6-1/x86-linux" ML_SYSTEM="polyml-5.6" ML_OPTIONS="-H 2000" isabelle build -a -j4 -o threads=6 0:38:38 elapsed time, 9:37:29 cpu time, factor 14.94 isabelle build -a -j4 -N -o threads=6 0:35:01 elapsed time, 8:28:11 cpu time, factor 14.51 isabelle build -a -j4 -N -o threads=4 0:40:11 elapsed time, 8:12:04 cpu time, factor 12.24 isabelle build -a -j8 -N -o threads=4 0:36:30 elapsed time, 8:26:39 cpu time, factor 13.88 I did not expect such fairly good results on that old machine. For me, 30min defines an upper bound of ergonomic testing. On my own machine, I usually get approx. 28-32min. The last variant with -j8 may have a benefit in testing Isabelle + AFP simultaneously, but I did not try it yet, because lxbroy10 is presently too busy. Makarius _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev