[isabelle-dev] Remaining uses of Proof General?
makarius at sketis.net
Thu May 8 12:25:19 CEST 2014
On Thu, 8 May 2014, Thomas Sewell wrote:
>> 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.
The important point is that a system like Isabelle cannot be built on the
basis of pragmatism. It is occasionally helpful to recall the cultural
foundations on which one is standing.
The system can be used pragmatically, or rather practically, of course.
> 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
Definitely. I've introduced the slogan of "Isabelle as logical operating
system" already in 2007, when the parallel batch mode with its ML threads
was still new. Many years later that has become reality in PIDE
interaction, but it was much harder to get there than anticipated. In
recent years I have become more cautious in the ambitions of what the
system is meant to do. It is already too far ahead of anything else in the
ITP world, and hardly anyone understands how it really works.
> 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.
Luckily Isabelle no longer depends on "make" and its many historical
problems. The Isabelle build tool is fast, because it does not access all
these files over and over again. Thus the need for extra tricks is
avoided, by giving up old habits from the 1970-ies.
> 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
That sounds rather obvious, but also like even more complication. David
Matthews has provided a nice simplified version of pthreads in Poly/ML.
He could probably do more, but even on the more complex JVM the influence
on thread scheduling is limited.
My canonical approach in such situations is to ask: Is there a way to
avoid the need for all that extra weight? It requires looking at concrete
applications carefully, to "disprove" their approach as something that
could be done differently, with less impact on resources.
That is not pragmatic, but it is how genuine scientific progress usually
More information about the isabelle-dev