[isabelle-dev] Interrupts Isabelle/ML

[Makarius]

After a2866dbfbe6b has come in this is one more attempt to draw attention 
to this important issue.  It has been on the list so many times that it 
seems to be ignored.


Here is the short version again (from the NEWS posted some weeks ago):

* Parallel and asynchronous execution requires special care concerning
interrupts.  Structure Exn provides some convenience functions that
avoid working directly with raw Interrupt.  User code must not absorb
interrupts -- intermediate handling (for cleanup etc.) needs to be
followed by re-raising of the original exception.  Another common
source of mistakes are "handle _" patterns, which make the meaning of
the program subject to physical effects of the environment.


The long version is in chapter 0 of the Isabelle/Isar implementation 
manual, see http://www4.in.tum.de/~wenzelm/test/implementation.pdf section 
0.5 in particular.


Tools that do not observe this specification cannot participate in the 
asynchronous interaction model.  (In Proof General it happens to work most 
of the time -- like nobody has ever noticed the serious race conditions of 
Poly/ML 5.2 until threads where used more heavily in Isabelle.)


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

   Quickcheck
   Nitpick
   Sledgehammer

The situation for Sledgehammer is more complex, since it still contains a 
separate management component for asynchronous tools that is based on an 
early implementation of mine, but needs to be replaced by a proper version 
the new document model.  I can't say when this will happen ... too many 
other things are preventing this.

Quickcheck and Nitpick should be easy to fix right now.  One merely needs 
to observe the standard pattern used in the sources elsewhere: grepping 
for Exn.is_interrupt should help, and looking at changes like 
69c6d3e87660.


People who don't want their tools to be adopted for the asynchronous 
interaction model should say so explicitly, so that they can be officially 
deactivated for Isabelle/jEdit.


 	Makarius