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

[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.

   * 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