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

[Tobias Nipkow]

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.

Tobias

> Christian
> 
> 
> 
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
>