[isabelle-dev] Remaining uses of Proof General?
makarius at sketis.net
Mon May 5 11:23:05 CEST 2014
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
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
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
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.
More information about the isabelle-dev