[isabelle-dev] [isabelle] the sound of a sledgehammer
makarius at sketis.net
Fri Feb 15 14:48:16 CET 2013
On Fri, 15 Feb 2013, Jasmin Christian Blanchette wrote:
> With 2 s of 1 CPU, it's possible to do quite a bit with Sledgehammer
> already (with one prover -- probably the lightning-fast Z3).
A few more marginal aspects:
* New mid-range hardware already has 8 CPUs on average, maybe 16 within
2 years (depending on market side-conditions).
* External provers like Z3 impose some overhead to invoke on Windows,
although it is not as bad as it used to be.
* Remote provers might be an alternative, as long as the perl
wrapper is bypassed and replaced by somthing based on
Invoke_Scala.method in ML (which happens to works only in
Isabelle/jEdit at the moment).
> Incidentally, most of the noncompressible overhead comes from picking up
> all the 10 000 or so facts from the context before filtering them,
> repeatedly for each Sledgehammer invocation. It's hard to do better
> there without using hacks or enriching the theories with
> Sledgehammer-specific data (think "Skolem cache"…).
That is an important observation. Heavy gear has long warm-up. So if we
take the "multi-target" approach seriously, sledgehammer could be offered
all candidate positions in the text for checking and do some smart things
by itself, to re-use the context somehow. (That is probably for a later
stage of sophistication of what we are sketching here.)
More information about the isabelle-dev