Re: [isabelle] Isabelle2013-1-RC1 available for testing

On Tue, 8 Oct 2013, Christian Sternagel wrote:

I find that on my machine (running the notorious 64bit Fedora 19 with Gnome) when using the Sledgehammer panel, very often (it feels like the majority of cases) after clicking "Apply", "Cancel" has no effect (the whole buffer is grayish highlighted).

This should be different in Isabelle2013-1-RC2, and hopefully better.

In such cases sometimes clicking "Apply" again actually cancels the ATPs, but sometimes only restarting Isabelle/jEdit helps (or maybe I would have to wait longer than 1 minute).

In such cases of uncertainty I merely reload the current buffer (F5), which is normallly sufficient. This operation is somehow reminiscent of proof-tract-buffer in Proof General :-)

For sledgehammer in particular, the "interaction state" is tied to the syntactic command span in the text. So if that is edited or removed any associated operations on the prover side should be canceled. The "Locate" button reveals the command that is associated with the current query process.


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.