Hello Florian, > > since my old »Explorer« draft, although never meant to be something > beyond a proof of concept, seems to be used productively, I spent some > time to polish it up a little, based on rev. c15ee153dec1.
Thanks for doing that! I tried it for a few minutes and: * it would be nice if the proof could be enclosed with cartouches instead of quotes, but the proper fix is to change ATP_Util.maybe_quote, which in turn would also make it possible to have cartouche in Sledgehammer proof. * I don't like the idea that sketch and explore require an additional argument. I often use (a variant of) it on goals generated by refine_vcg (from Refine_Imperative_HOL). I guess I could call "sketch (tactic ‹all_tac›)", but I would prefer that no argument means no tactic call. On the other hand, I might have a strange use-case. > * Indentation does not consider any pre-existing indentation. Given that indentation is done purely on the Isabelle/jEdit side, I don't think there is any way to make this work. Cheers, Mathias > On 21. Mar 2019, at 16:48, Florian Haftmann > <[email protected]> wrote: > > Signed PGP part > Hi all, > > since my old »Explorer« draft, although never meant to be something > beyond a proof of concept, seems to be used productively, I spent some > time to polish it up a little, based on rev. c15ee153dec1. > > The situation is a little bit uncomfortable, since it is definitely > useful, particularly from a didactic point of view. But there are still > some oddities and pragmatisms in the code which do not justify a regular > integration into the distribution: > > * It does not use any specific logic, but cannot be based on Pure since > it relies on some sledgehammer printing functions (which could be > extracted as separate toolbox, of course). > > * Re-printing of proof method text is quite ad-hoc. > > * Indentation does not consider any pre-existing indentation. > > * Type annotations of printed terms could be more minimal. > > In the moment I feel inclined to put the matter into HOL-ex and than > proceed from that. > > In the meantime, I am open to feedback. > > Cheers, > Florian > > Am 12.09.18 um 08:23 schrieb Florian Haftmann: >>>> On 7 Sep 2018, at 19:18, Makarius <[email protected]> wrote: >>>> >>>> I can't try it out, since theory "Explorer" is missing. >>> >>> Attached. A very cool thing. >> >> Nice to see that old draft from 5 years ago. >> >> I would still agree that such a tool would be tremendously useful, but >> before going into the distro it would need technical improvement, i.e. >> more civilized approach toward Isar proof text generation, similar to >> Sledgehammer_Isar_Proof. >> >> Any opinions on that? >> >> Cheers, >> Florian >> >> >> _______________________________________________ >> isabelle-dev mailing list >> [email protected] >> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev >> > <Sketch_and_Explore.thy><Test_Sketch_and_Explore.thy> > > _______________________________________________ isabelle-dev mailing list [email protected] https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
