Re: [isabelle] sledgehammer in RC4



Hi Jasmin,

You gave me useful information, and I can now get sledgehammer working for me.

There seems to be some problem with remote_z3:

   sledgehammer_params [provers = remote_z3]
   lemma "[a] = [b] \<Longrightarrow> a = b"
   sledgehammer

gets the response:

   Sledgehammer: "remote_z3" on goal
   [a] = [b] \<Longrightarrow> a = b
   A prover error occurred:
   Solver "remote_z3" failed. [...]

while:

   sledgehammer_params [provers = z3]
   lemma "[a] = [b] \<Longrightarrow> a = b"
   sledgehammer

gets the expected response.  Also something strange about remote_e_sine:

   sledgehammer_params [provers = remote_e_sine]
   lemma "[a] = [b] \<Longrightarrow> a = b"
   sledgehammer

gets the response:

   Sledgehammer: "remote_e_sine" on goal
   [a] = [b] \<Longrightarrow> a = b
   Timed out.

while:

   sledgehammer_params [provers = spass remote_e_sine]
   lemma "[a] = [b] \<Longrightarrow> a = b"
   sledgehammer

gets the expected response.  So remote_e_sine works under some
circumstances and not under others.  This seems to be repeatable.

BTW, how does Multithreading.max_threads_value get set to 2, can I
change it, and would that do any good?  You and Makarius probably
understand this point better than I: a modern "dual core" Intel
machine has 4 hardware threads.

Thanks,
Randy
--

On Sun, Nov 10, 2013 at 10:36 AM, Jasmin Blanchette
<jasmin.blanchette at gmail.com> wrote:
> Hi Randy,
>
>> I'm running in a VBox virtual machine on a MacPro that has 2 cores
>>
>>> 1. How many cores does your machine have?
>> The VM is set with 2 CPUs
>>
>>> 2. What is the value reported by ML {* Multithreading.max_threads_value () *} ?
>> 2
>
> OK, that explains it.
>
> Earlier versions of Sledgehammer ran at most 2 local ATPs (for a 2-CPU system) + a number of remote ATPs in that case, since remote ATPs do not put a heavy load on the local machine. However, this lead to some weird effects when using jEdit's new Sledgehammer tab, which users the thread scheduling of PIDE instead of Sledgehammer's somewhat deprecated solution. (Namely, two or three rounds of running ATPs would be necessary, doubling or trippling the effective time out and leading users to wonder what's going on.) It would be possible to have different defaults for Proof General and jEdit, but Sledgehammer already has too many modes, so I'd rather not go that way. Also, I am betting on the trend toward 4-/8-core systems and jEdit to continue.
>
> The default provers invoked can be changed in Proof General using the Isabelle menu. This is preserved across sessions, so you should need to do it only once. An alternative is to put
>
>     sledgehammer_params [provers = e spass remote_vampire remote_z3]
>
> at the top of your theory (or in one of your base theories).
>
> I hope this helps.
>
> Regards,
>
> Jasmin
>
>




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