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



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.)

The current implementation is still very crude in this respect. It does not even "try as best as it can". It merely ignores failed commands, and often makes a mess while bumping into later parts of the text. An obvious approach is to take syntactic proof structure into account, using implicit 'sorry' as sketched above (and in fact making 'sorry' obsolete for end-users).

This is not totally trivial, since a proof might be so broken that the system cannot guess its structure anymore. So this important reform of the PIDE document model in that respect is related to proper indendation support in the editor, which is also lacking from the very start of Isabelle/jEdit. (It will be probably also the notable point in history, where hard tabulators are discontinued as "blanks", because they make the indentation unclear.)


A few months before every release in the past 3 years, I routinely check if it is now feasible to open that can of interactive structured error recovery. But again, I don't see it happining for the coming release, because so many changes in PIDE interaction have already accumulated that will take months to consolidate and polish.


	Makarius


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