[isabelle-dev] Remaining uses of Proof General?

[Makarius]

On Mon, 5 May 2014, Thomas Sewell wrote:

>>  The basic assumption is that each proof task does not run too long, and if
>>  it does it is something to be improved in the application to make it more
>>  smooth.  In contrast, Proof General makes it more easy to produce huge and
>>  heavy proof scripts that can be hardly handled by anyone else later.
>> 
>
> Right. That seems to be the assumption that's being violated in the few 
> cases where people are still keen on ProofGeneral, for instance, in 
> Andreas' big complicated tactic applications.

One needs to understand two important things here: technology and 
psychology.

15 years ago, there were certain technological side-conditions both in the 
prover and in Emacs, which made Proof General what it is.  Later people 
got used to that and optimized their "workflow" accordingly.  Certain 
manual task scheduling became second nature to them.

5 years ago, the prover was quite different and the JVM + Scala + jEdit 
platform imposed other technological side-conditions of what can be 
done.  Again, people need to get used to that and optimize their 
workflow, but in addition one needs to unlearn old habits from Proof 
General,

This psychological factor makes it difficult to see the genuine technical 
problems that still need to be addressed.  As usual it helps to show the 
actual situation, either just the sources, or a video of the usual 
workflow, or a demonstration with personal presence.


> Let me make a proposal. I think that various users would appreciate it 
> if one of the worker threads was reserved for print jobs caused by 
> moving the cursor (highest priority tasks) and their dependencies 
> (assuming more than one worker thread). That would hopefully make it 
> easier to control the delay. If the user is cautious with moving the 
> cursor and if enough proof dependencies have been processed, the system 
> *should* be as responsive as PG. The delay would also be mostly 
> unaffected by the proof task runtime, only the print task runtimes, 
> which might be easier for an advanced user to manage.

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.


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


 	Makarius