[isabelle-dev] [isabelle] the sound of a sledgehammer
webertj at in.tum.de
Sun Feb 17 17:06:46 CET 2013
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.
More information about the isabelle-dev