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

[Christian Urban]

On Sunday, February 17, 2013 at 17:06:46 (+0100), Tjark Weber wrote:
 > On Fri, 2013-02-15 at 13:37 +0100, Tobias Nipkow wrote:
 > > >   * 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.
 > 
 > My gut feeling is that already today, I would prefer s/h to run
 > automatically on every intermediate proof state if this didn't
 > interfere with my editing. Why should the many cores in my machine sit
 > idle? 

Well I am all for it, as long as there is also a way 
to switch it on and off on demand. I sometimes work
in a quite environment where my Mac Book Air should
not emit noise like on an airport and be hot like
a potato. In such circumstances I am quite happy
if my CPUs waste a bit of idle time. ;o)

Christian