*** 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:
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
isabelle-dev mailing list