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 > [email protected] > https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev _______________________________________________ isabelle-dev mailing list [email protected] https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
