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

[Tjark Weber]

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? It seems perfectly reasonable to spend a few billion CPU cycles
if that occasionally saves a minute or two of human time.

Architecturally, some kind of incremental mode for s/h (as suggested by
Jasmin) could reduce the performance overhead.

Best regards,
Tjark