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

[Makarius]

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.)


 	Makarius