[isabelle-dev] Interrupt exceptions using the Par_List combinator get_some
makarius at sketis.net
Wed Aug 10 21:53:26 CEST 2011
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
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
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.
More information about the isabelle-dev