[isabelle-dev] Interrupts Isabelle/ML

[Makarius]

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 3.7.1.1 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 
synchronization.


> 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 
> get
>
>    *** Interrupt
>    *** Exception- TOPLEVEL_ERROR raised
>    Exception- TOPLEVEL_ERROR raised
>    ML>

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 
"Interrupt" exception.


 	Makarius