[isabelle-dev] NEWS: isabelle build performance tuning

[Makarius]

*** 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