On Fri, 15 Feb 2013, Tobias Nipkow wrote:
Am 15/02/2013 13:12, schrieb Makarius:
* Sledgehammer has some kind of "home panel" which gives an overview of
results and some global controls.
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.
This is in contrast to auto-solve and quickcheck, both of which have a low
overhead. Conceivably one could configure a s/h-very-light, which would be
launched spontaneously.
So that is one of the "controls", to tell if it acts spontaneously or by
pushing a button in the panel. Heavy gear like Sledgehammer can be
non-spontaneous by default.
Makarius
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
