Losing sync with interrupt

[Makarius]

Using GNU emacs 22.1.1 on Ubuntu 7.10, the editor easily looses sync after stopping an unprocessed queue of commands.

For example, visit Isabelle/src/HOL/Lambda/ParRed.thy and assert the whole buffer. While the queue is being processed, but partly in "purple", pressing Stop button makes the prover choke on strange "<tool-bar> <interrupt>" sequences showing up in the *isabelle* buffer. Typing RETURN here helps a bit, but synchronization is usually lost.

In other situations, it *is* possible to interrupt safely. E.g. in Isabelle/src/HOL/Lambda/Eta.thy lemma square_beta_eta, the line marked as (*23 seconds?*).

[David Aspinall]

Can't reproduce at the moment because of error in Isabelle CVS Lambda.thy:

*** Outer syntax error (line 20 of "/home/da/cvs/isabelle/HOL/Lambda/Lambda.thy"): command expected,
*** but keyword :: (line 20 of "/home/da/cvs/isabelle/HOL/Lambda/Lambda.thy") was found
*** At command "theory".

Question: is this loss of sync happening when interrupt occurs while included files are being loaded (as in this case)? This may have a different behaviour to interruption within a file.

[David Aspinall]

OK, I can reproduce this (error in Isabelle CVS was of course caused by using Isabelle2007 to process file).

First, notice that strange output you seen in the *isabelle* buffer is an effect of the comint package, in both Emacs and XEmacs (latest versions): try C-c C-c or the Signals menu to see this, even in a *shell* buffer. Presumably this is a feature to show the user where/that they interrupted. I have disabled this effect in Proof General now (at the risk of becoming comint version specific; now we have to test on old Emacsen again, sigh).

Second, notice that interrupts which occur actually when the prover is not busy (but between commands) can cause sync problems already, also in XEmacs. The torture test file I've added at etc/isar/InterruptTest.thy.gz demonstrates this with some long commands that consume more CPU in Emacs than in Isabelle.

Fixing this requires some additional machinery to handle interrupts locally so that the queue is properly aborted.

[David Aspinall]

No time to complete this now; attaching partial patch and bumping to 3.7.1.

[David Aspinall]

Add a route for the code to signal interrupt to itself, without relying on an interrupt message in the proof shell.

[David Aspinall]

This is quite tricky.

It turns out that (perhaps due to changes in Isabelle over recent years) when input is sent to Isabelle and then the process is interrupted, and there may or may not be an interrupt message, and the input may or may not be processed. These cases can be seen using the suggested file, which causes expensive parse operations. You can also see this in the tty interface.

Previously the interpreter reliably printed interrupted messages whenever a signal was sent, which was very helpful to the interface.

Proof General needs a bit of rewiring to deal with these swallowed interrupts.

[David Aspinall]

In fact, some interrupts are simply lost altogether by Isabelle: try a theory with a lengthy imports statement if C-c C-c is pressed just after the loading theory... message appears, the interrupt is swallowed and Isabelle carries on regardless!

[David Aspinall]

OK, the behaviour in PG is now improved so that it notices "pending" interrupts: those that have been requested by the user but not acted upon by the prover. In the case that a command completes and there is a pending interrupt, the queue will be terminated.

However, this does not completely fix the ugly case when Isabelle fails to send a prompt when it has been interrupted during processing a command. PG cannot tell the difference now between a prover that is busy and simply not returning output from the stuck state that Isabelle enters. Sending further interrupts does not trigger any output either, so the user can only revive by sending input in the shell buffer. The assumption now is that a command has succeeded, so this regains sync I believe.

Closing this bug as it is clearly an issue with interrupt handling in Isabelle. My testing has been with Isabelle2009.