Email Gateway (Aug 19 2022 at 12:06): Email Gateway (Aug 19 2022 at 12:06):From: Christoph LANGE <math.semantic.web@gmail.com>
Hi Makarius,
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.
Cheers,
Christoph
Email Gateway (Aug 19 2022 at 12:10):From: Christoph LANGE <math.semantic.web@gmail.com>
2013-10-03 20:04 Christoph LANGE:
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.
Cheers,
Christoph
Email Gateway (Aug 19 2022 at 12:17):From: Makarius <makarius@sketis.net>
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.
Makarius
Last updated: Apr 25 2024 at 08:20 UTC