[isabelle-dev] Isabelle2009 fails to handle interrupts
makarius at sketis.net
Thu Aug 27 16:16:00 CEST 2009
On Mon, 17 Aug 2009, David Aspinall wrote:
> I don't believe this is PG's fault. I can reproduce problems in tty mode.
> With the previous version, you sent C-c C-c and it reliably interrupted and
> printed "*** Interrupted". With Isabelle2009 interrupts may get ignored or
> go unreported and output and the following prompt may or may not appear.
> I've added some workaround but it's not easy to tell between a busy prover
> and one that's been interrupted and stopped sending output but is too
> secretive to tell you about it!
What exactly did you try here? Is this just use_thy "ParRed" with some
erratic C-c key presses?
Anyway, the exact interrupt behaviour has always been in flux, depending
both on changes in the various ML systems (SML/NJ, Poly/ML 4.x, Poly/ML
5.x) and changes in the Isar toplevel. Let's assume Poly/ML 5.2.1 for
now, to simplify the discussion.
First of all, there are always situations where interrupts can be ignored,
but this should not cause any messages or silent stopping of a command. In
a sense, you can understand an external interrupt as a *hint* to some of
the running command transactions to fail with a proper error eventually.
There is one exception: sometimes faulty ML code explicitly handles the
internal Interrupt exception without reraising it to make it appear on the
toplevel. This is usually caused by the infamous "handle _" which should
never occur in user code; the "try" and "can" combinators will do it
Such misinterpreted interrupts might cause strange behaviour, but
editor/toplevel state synchronization should not be lost.
More information about the isabelle-dev