[isabelle-dev] Remaining uses of Proof General?

[Makarius]

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

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

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


 	Makarius