[isabelle-dev] Interrupts Isabelle/ML
makarius at sketis.net
Fri Nov 12 11:46:44 CET 2010
On Wed, 10 Nov 2010, Jasmin Christian Blanchette wrote:
> At least with "urgent_message", the message was immediately overwritten
> by the exception error, even in Proof General; so I gave up the idea on
> showing any message upon user interruption.
This might also depend on the PG version, but I did not try it out. The
versions that are currently in use are 220.127.116.11 and 4.0. The PG message
model has always been somewhat undecidable. Urgent messages sometimes
work for you, sometimes against you. I have seen situations where a
urgent message did get precedence over errors, but that caused a loss of
> In the new interface, one could imagine seeing continual progress from
> diagnosis tools such as Quickcheck and Nitpick. This is something we
> could look into once the new interface is in place.
Output is already "continous" in the sense that the message slot of a
running transaction is updated incrementally, without waiting for a
strange "prompt" or something. (The prompt has been abolished anyway.)
Once a transation is reset via interrupt, the behaviour is not fully
defined yet. I am already glad to get to the point where frequent
asynchronous signalling does not cause commands halt and catch fire.
> I don't know if it's related, but sometimes running Mirabelle I get
> spontaneous "Interrupt" exceptions, which spoil the Mirabelle run.
> Anyway, it would be nice if the "Interrupt" had more information as
> argument -- e.g., did a user press Stop in Proof General, or did the
> Poly/ML process run out of some resource or something. Currently I just
> *** Interrupt
> *** Exception- TOPLEVEL_ERROR raised
> Exception- TOPLEVEL_ERROR raised
I have no idea, could be something like out-of-memory. Poly/ML does not
provide more details, and cannot easily do so without introducing new
challanges to user code. Right now everything is routed through the one
More information about the isabelle-dev