[isabelle-dev] Sketch and explore [was: performance problems]

[Mathias Fleury]

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 <florian.haftmann at informatik.tu-muenchen.de> 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 <makarius at sketis.net> 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
>> isabelle-dev at in.tum.de
>> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
>> 
> <Sketch_and_Explore.thy><Test_Sketch_and_Explore.thy>
> 
>