Re: [isabelle] Isabelle2015-RC0 available for testing



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

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.

Jasmin





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