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_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
