On Mon, 5 May 2014, Makarius wrote:
Users running on batteries might also want a mode that restricts all
threads to the behaviour above.
Have you tried that with "threads = 1" (there is also a special treatment for
high-priority prints in that mode)? So far I guess that most people run with
defaults, without any idea of the tuning parameters.
See also:
changeset: 56875:f6259d6fb565
user: wenzelm
date: Tue May 06 16:05:14 2014 +0200
files: etc/options src/Pure/PIDE/command.ML
description:
explicit option parallel_print to downgrade parallel scheduling, which
might occasionally help for big and heavy "scripts";
In principle this is an instance of the "too many options" syndrome, but
here the implicit change of behaviour on 1 core is merely made explicit.
Moreover, according to the "waterbed-syndrome" in its positive sense, it
means that options added here inevitably cause other old/obsolete options
to be removed faster.
Makarius
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
