Re: [isabelle] sledgehammer in RC4

Hi Randy,

Am 10.11.2013 um 03:10 schrieb Randy Pollack <rpollack at>:

> I just installed Isabelle2013-1-RC4 on a fresh installation of Ubuntu
> 13.10, using the standard "download for Linux" from the Isabelle
> webpage.  I built the HOL image without any problem.
> Sledgehammer fails to find proofs that it found in the Isabelle2013
> version.  So I tried the simple example from the "First Steps" section
> of "Hammering Away" from the Isabelle documentation.  Only e and spass
> were being called.
> BTW, I fixed  Z3_NON_COMMERCIAL= yes, and did not get the ususal
> Isabelle warning saying to do that.
> What have I forgotten?

Which default provers end up being run depend on a number of factors. The algorithm has changed between 2013 and 2013-1RC*, to avoid running e.g. 5 provers on 4 cores. I'd need a bit more information from you to debug this:

1. How many cores does your machine have?

2. What is the value reported by ML {* Multithreading.max_threads_value () *} ?

3. Do you use Proof General or jEdit/PIDE?

4. How do you invoke Sledgehammer? Do you type "sledgehammer" in the editor window or use the new jEdit Sledgehammer panel?

5. What is the output of the "sledgehammer_params" command?

Thank you in advance.



This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.