Re: [isabelle] Isabelle2015-RC0 available for testing



2015-04-20 18:26 GMT+02:00 Jasmin Blanchette <jasmin.blanchette at inria.fr>:
>
>> On 20.04.2015, at 16:19, C. Diekmann <diekmann at in.tum.de> wrote:
>>
>>> Incidentally, this behavior of Sledgehammer is nothing new. Is the issue really new with Isabelle2015-RC0? What happens if you write
>>>
>>>   ML {* Multithreading.max_threads_value () *}
>>>
>>> in Isabelle2014 vs. Isabelle2015-RC0?
>>
>> Both report "2". I have a dual core cpu with 2 physical cores and
>> thanks to hyperthreading two additional virtual cores. /proc/cpuinfo
>> lists 4 processors.
>
> Then I presume Sledgehammer also invoked only two ATPs in Isabelle2014?

Yes

> Irrespective of this, you probably want to check the Isabelle system manual to find out how to change the number of threads. 2 is perhaps needlessly low.

Thanks for the pointer.

  Cornelius




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