[isabelle-dev] Remaining uses of Proof General?
makarius at sketis.net
Wed May 7 14:59:01 CEST 2014
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.
date: Tue May 06 16:05:14 2014 +0200
files: etc/options src/Pure/PIDE/command.ML
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.
More information about the isabelle-dev