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
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
