[isabelle-dev] [isabelle] the sound of a sledgehammer
nipkow at in.tum.de
Mon Feb 18 08:11:36 CET 2013
Am 17/02/2013 19:41, schrieb 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)
There should be an energy saving mode switch for people on battery. It should
disable all spontaneous computations.
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
More information about the isabelle-dev