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
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
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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and