[isabelle-dev] Interrupt exceptions using the Par_List combinator get_some

[Makarius]

On Mon, 25 Jul 2011, Makarius wrote:

> On Sun, 24 Jul 2011, Lukas Bulwahn wrote:
>
>>> In Isabelle/318ca53e3fbb it works half-way, when the outer execution 
>>> context is not a worker task itself, e.g. on the tty.
>>> 
>> For tool developers, this means as consequence, we either do not use 
>> Par_List.get_some or ensure by other means, that we know if the outer 
>> execution context is a worker task or not, when being invoked, right?
>
> You cannot really ensure a non-worker context in reality.  This is merely a 
> hint that experiments can be done on the raw tty at the moment.
>
> Of course I will revisit the issue again and more thoroughly, when I am back 
> from travel in 2 weeks.

The result of another round of refinement is now 
http://isabelle.in.tum.de/repos/isabelle/rev/2d16c693d536

It turned out to be a rather "soft" problem: interrupts need to be treated 
as a critical resource of the task queue.  No magic hardware issue this 
time.


I have also tried to reactivate some examples in 
src/HOL/Predicate_Compile_Examples, but could not disentangle the layers 
of temporarily disabled examples.

Please tell me if any problem with interrupts persist.  This depends a lot 
of actual production code using it.  You have happened to be the first or 
second serious user so far.


 	Makarius