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 _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev