[isabelle-dev] Remaining uses of Proof General?

Makarius 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.

See also:

changeset:   56875:f6259d6fb565
user:        wenzelm
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 mailing list