Re: [isabelle] Incomplete goal may cause proof methods of later goals to loop.



Le Tue, 22 Apr 2014 14:09:19 +0200, Makarius <makarius at sketis.net> a écrit:

On Tue, 22 Apr 2014, Lawrence Paulson wrote:

Without reopening the “what is a bug” debate, I need to say that this
sort of thing is inevitable with the approach taken by Isabelle/jEdit,
in attempting to process everything, parsing errors and all. If you type
in a syntactically incorrect proof, it tries to recover as best it can.
In this case, it ignores the syntactically incorrect “show” command,
causing the behaviour you observe. An alternative would be to silently
insert “sorry” in order to complete the previous proof, preventing that
behaviour but having other undesirable consequences.

("Bug" is indeed a meangingless word, and I can't imagine anybody
attaching that label to this thread.)

The general problem here is how to recover from errors (or
non-termination) while the user is editing some unfinished proof text.
(Really proof *text* and not proof *script* because we are in the lucky
situation that Isar proofs have a lot of explicit structure.)


I remember Coq has a different way to handle this: there are explicit forward and backward (in proof state) commands. The processed part of a proof is not editable and one have to go backward to edit it, then go forward again and resume up to the last proof statement. This is sometime tedious, while clean.

That's a way too much different compared to what Isabelle users are accustomed to. Personally, it happens I think about the Coq way when I feel Isabelle process too much of invalid text during editing, while in other cases, I enjoy the reactivity of feedback from Isabelle while editing.

May be an idea could be to have a keystroke to quickly enable/disable “Continuous checking”… a keystroke, so that this would remain handy while editing: no need to leave the keyboard to go from and to the mouse to check/uncheck the option and no need to have the theories panel always visible (otherwise needed, as the option is located on this panel).


--
“Syntactic sugar causes cancer of the semi-colons.” [1]
“Structured Programming supports the law of the excluded muddle.” [1]
[1]: Epigrams on Programming — Alan J. — P. Yale University





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