*To*: Jasmin Blanchette <jasmin.blanchette at gmail.com>*Subject*: Re: [isabelle] sledgehammer in RC4*From*: Randy Pollack <rpollack at inf.ed.ac.uk>*Date*: Sun, 10 Nov 2013 12:36:37 -0500*Cc*: isabelle-users <isabelle-users at cl.cam.ac.uk>*In-reply-to*: <26755B7F-E696-4A5D-9BE7-9BCFA0FF85B8@gmail.com>*References*: <CANofLeJJ8O2Y2ktXUER1AsH1F4CQsBB21PPbLMVVQa-UfwjgoQ@mail.gmail.com> <353FF788-2AA0-4188-8AAD-28E803A1F647@gmail.com> <CANofLeLVT7QWSUE4HhNy+kq9UuCe4J7gsXVEzma0x_SO5C03wQ@mail.gmail.com> <26755B7F-E696-4A5D-9BE7-9BCFA0FF85B8@gmail.com>*Sender*: rpollack0 at gmail.com

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

**Follow-Ups**:**Re: [isabelle] sledgehammer in RC4***From:*Gottfried Barrow

**Re: [isabelle] sledgehammer in RC4***From:*Jasmin Blanchette

**References**:**[isabelle] sledgehammer in RC4***From:*Randy Pollack

**Re: [isabelle] sledgehammer in RC4***From:*Jasmin Blanchette

**Re: [isabelle] sledgehammer in RC4***From:*Randy Pollack

**Re: [isabelle] sledgehammer in RC4***From:*Jasmin Blanchette

- Previous by Date: Re: [isabelle] sledgehammer in RC4
- Next by Date: Re: [isabelle] Isabelle2013-1-RC4 available for testing
- Previous by Thread: Re: [isabelle] sledgehammer in RC4
- Next by Thread: Re: [isabelle] sledgehammer in RC4
- Cl-isabelle-users November 2013 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list