[isabelle-dev] Interrupts Isabelle/ML

[Makarius]

On Fri, 5 Nov 2010, Makarius wrote:

> Right now (96c37a685a13) the following tools limit themselves to the old 
> Proof General / TTY model:
>
>  Quickcheck
>  Nitpick
>  Sledgehammer

Thanks to Jasmin for addressing this for Nitpick in 36b7ed41ca9f. The 
follow-up to 96c37a685a13 for Quickcheck is still missing, though.

Generally, the main point about the interrupt discipline is to allow the 
system to "reset" command transaction in a clean manner.  It *is* possible 
to handle interrupts very briefly, to cleanup global resources etc.  It is 
also possible to print a final message, if that does not involve any 
serious computations that take long (or forever), or could fail otherwise. 
This is similar to other signal handlers in other programming 
environments.

Here is an example pattern:

   f x handle exn =>
     if Exn.is_interrupt exn then
       (writeln "oops"; cleanup_quickly (); reraise exn)
     else reraise exn;

Since the transaction is officially being reset, the above message might 
never reach the user in the async. document model, but PG/TTY will show it 
nonetheless.


Whatever is being done with interrupts, the ML code should make it 
immediately clear that there is no problem.  These things need to be 
inspected over and over again -- recently I've found again many mistakes 
in my own sources, and those of David Matthews (Poly/ML basis library).


 	Makarius