[isabelle-dev] Remaining uses of Proof General?

[Thomas Sewell]

Thanks Makarius.

A few of us at NICTA have ported this change to our various versions of 
Isabelle and begun playing with it. It seems to improve the situation 
sometimes, though we haven't yet got a feel for when in particular it 
helps. In fact, we haven't really understood what the change does.

On 07/05/14 22:59, Makarius wrote:
> 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.
>

I completely agree that having too many options is a problem. There's no 
point having them if noone knows that they're there, or which ones to 
try. That said, I think it's a good path for performance adjustments 
which might or might not be helpful. I suspect you could get away with 
adding far more options than you plan to have in the end, and keep only 
the ones that end up with a quorum of users. I'm a bit of an optimist 
though.

> This sounds a bit too pragmatic and opportunistic to me.  What is 
> special about print tasks anyway, apart from their priority?  The 
> recent concept for asynchronous print functions makes print tasks 
> rather general, and there are more automated provers or disprovers in 
> that category than actual printing.
>
> What is even more important than prints, is the main protocol thread, 
> which presently needs to work against the whole farm of worker threads 
> to update certain administrative structures of the document model.  If 
> I knew a proper way to reduce the priority (or to pre-empt) worker 
> threads for that, I would do it.  But it probably needs some work by 
> David Matthews on the ML thread infrastructure.
>

Consider me an unashamed pragmatist. I see a similarity between 
task/thread scheduling in Isabelle and task/thread scheduling in 
operating systems. All modern operating systems are full of ad-hoc 
heuristics designed to bump up the priority of tasks that are likely to 
create I/O requests or update things for the user. A parallel "make", 
for instance, will run much faster if the OS prioritises the compile 
tasks that are still reading files ahead of the ones that have begin 
compiling and computing. This keeps the disk working throughout the 
build. Windows raises the priority of in-focus windows, and Mac OS X 
pushes the audio threads of apps up to the highest priority, etcetera.

I may have misspoken with regard to "print task". I guess I meant "task 
that will produce output which at some point the user has directly 
requested into their output panel, query panel etc". If we see the user 
as an external resource like a hard disk, these are the tasks we need to 
front-load to keep the external task running at full capacity. I see the 
some of the other output tasks, which possibly produce counterexamples 
or which produce squiggly lines which are possibly helpful, as lower 
priority.

Preempting long-running tasks would change the tradeoffs a lot. Another 
possibility would be to introduce a yield-point (cooperative 
multitasking) which a task can execute, which will possibly cause its 
execution to be delayed in favour of a higher priority task. Adding that 
to the tactic combinators would make nearly all Isabelle workloads much 
finer-grained.

Well, those are just my thoughts. Thanks for the adjustment, I hope it 
solves our responsiveness problems.

Best wishes,
     Thomas.