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
_______________________________________________
Isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
