[isabelle-dev] [isabelle] the sound of a sledgehammer

[Tobias Nipkow]

Am 15/02/2013 13:12, schrieb Makarius:
> On Do, 2013-02-14 at 17:22 +0000, Lawrence Paulson wrote:
>> In a dream scenario, one might imagine opening a document containing a number
>> of occurrences of "sorry", and each one of these occurrences would be given to
>> counterexample finders and to sledgehammer, without any specific user
>> intervention. Then somehow any counterexamples or proofs that were found would
>> be noted somehow, and the user could inspect these.
>>
>> I recognise this idea isn't even half baked. But I know that you want to look
>> at these problems differently from just saying, "how did it work in Proof
>> General"? And the idea of having a whole bunch of gaps checked (as it were)
>> simultaneously is very appealing.
> 
> On Fri, 15 Feb 2013, Lawrence Paulson wrote:
>> Another idea is to implement sledgehammer a pop-up window tied to a particular
>> place, which eventually will receive sledgehammer's result. Then you could
>> continue editing the document freely, without interfering with the
>> sledgehammer execution.
> 
> Yes, this sounds all pretty close to the "asynchronous agent" scenario from
> several years ago, and it is in a sense all somehow obvious when we look
> critically at what happens to be there in the Proof General tradition vs.
> state-of-the-art IDEs for other languages.
> 
> Summary of this thread so far:
> 
>   * Sledgehammer has some kind of "home panel" which gives an overview of
>     results and some global controls.
> 
>   * Sledgehammer spontaneously acts asynchronously of certain open
>     problems in the text, depending on certain parameters like time outs.

Triggering s/h via "sorry" (or some other explicit means) is perfectly
reasonable, but having the IDE invoke s/h based on time outs and guesses should
be avoided: the success rate is low and it consumes a lot of resources.

This is in contrast to auto-solve and quickcheck, both of which have a low
overhead. Conceivably one could configure a s/h-very-light, which would be
launched spontaneously. In fact, for some time I had toyed with the idea of
upgrading auto-solve to take additional properties into account, like
commutativity of operators. s/h-very-light might be that auto-solve++.

Tobias

>   * Sledgehammer is not disturbed by the user editing.  It might
>     eventually give up on problems that have become obsolete, since they
>     have been long deleted from the text.
> 
> You mention explicit 'sorry' above, which is fine as 0-th approximation. There
> could be also explicit markers for certain tools, they don't have to be in the
> text at all.  It should be reasonably easy to add them to the "model" of the
> buffer, a bit like existing jEdit markers but not restricted to line-boundaries.
> 
> 
>     Makarius
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev