Re: [isabelle] sledgehammer in RC4

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.



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