Re: [isabelle] 2013-1-RC1: proof method suggested try or try0 no longer overwrites 'try' keyword

On Fri, 4 Oct 2013, Christoph LANGE wrote:

2013-10-03 20:04 Christoph LANGE:
in Isabelle 2013 when I wrote "statement try", or try0, and try found a
proof, clicking on this proof in the output panel replaced the "try"
keyword in the edited source by the proof.  This is no longer the case
in 2013-1-RC1.  Instead the proof (e.g. "by blast") is placed after the
"try", which remains.

After some more playing I'm starting to realise that this might be a
_feature_.  Suppose you try to prove something with Sledgehammer, and it
suggests several possibilities, which you would then minimise, all
possibilities are retained in the document until you finally decide for
one proof.  However you would have to clean up yourself all those
alternatives you don't like.

There is indeed a slight change of the behaviour in "sendback" text produced by commands like sledgehammer, nitpick, try0 etc. Before Isabelle2013-1 there was no specific support for what is now called "query operation", and there were some temporarary approximations to a workflow where you insert commands in the buffer and get them replaced eventually.

With the implicit "auto sledgehammer" and explicit "slegdehammer panel" you normally don't put query commands in the buffer anymore, and the editing behaviour has been adapted accordingly. Thus you gain a lot, but you loose a little bit with commands that still don't have their own query panel, such as 'try0'. (Supporting both the old and the current behaviour turned out to lead in an unmaintainable confusion of the code, which would inevitably lead to bad system rather soon.)

Looking ahead even a bit further, the next stage is to support more structured editing of the text with assistance by the prover and the editor. Then the replacement policies would be determined by the text itself, not funny properties in the sendback messages we still see today.


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