Email Gateway (Aug 19 2022 at 13:04): Email Gateway (Aug 19 2022 at 13:04):From: Christian Sternagel <c.sternagel@gmail.com>
Dear all,
I started a build where with -v I got
ISABELLE_BUILD_OPTIONS=""
ML_PLATFORM="x86-linux"
ML_HOME="/usr/local/Isabelle2013-2/contrib/polyml-5.5.1-1/x86-linux"
ML_SYSTEM="polyml-5.5.1"
ML_OPTIONS="-H 500"
and my ~/.isabelle/Isabelle2013-2/etc/settings is
init_component "/usr/local/afp-2013-12-02/"
ISAFOR="$HOME/rewriting/IsaFoR/"
Z3_NON_COMMERCIAL="yes"
My processor is an i7-3630QM (4 cores, 8 threads; which are reported as
8 cores in /proc/cpuinfo ). So I would expect that by default 8 threads
are used by "isabelle build". However, I get messages like the following
Timing <session-name> (4 threads, 44.314s elapsed time, 158.450s cpu
time, 34.924s GC time, factor 3.58)
Finished <session-name> (0:00:57 elapsed time, 0:02:56 cpu time,
factor 3.08)
Indicating that only 4 threads are used. When I do the same thing on a
different machine with an i7-3520M (2 cores, 4 threads) the
corresponding messages are also saying "4 threads".
So my question is, how is the number of threads determined when
ISASBELLE_BUILD_OPTIONS is empty?
cheers
chris
Email Gateway (Aug 19 2022 at 13:17):From: Christian Sternagel <c.sternagel@gmail.com>
That was it, thanks! - cheers chris
Email Gateway (Aug 19 2022 at 13:34):From: Makarius <makarius@sketis.net>
(This thread is still left-over from last year.)
The main input parameter for Isabelle/ML to determine the number of worker
threads is the system option "threads". It is used both for batch build
and Isabelle/Scala interaction (e.g. Isabelle/jEdit).
In $ISABELLE_HOME_USER/etc/preferences you can see your local persistent
preferences, i.e. what you typically edit via Isabelle/jEdit Plugin
Options. I guess that you just have threads = "4" there.
Makarius
Last updated: Apr 24 2024 at 01:07 UTC