Re: [isabelle] Isabelle2015-RC0 available for testing



> On 17.04.2015, at 01:01, Makarius <makarius at sketis.net> wrote:
> 
> On Sun, 12 Apr 2015, C. Diekmann wrote:
> 
>> * when I type sledgehammer (not using the panel), it seems as it is
>> only tries cvc4 and remote_vampire, is it possible to add a bit more

This indicates that âmax_threadsâ is 2. By default, Sledgehammer will use only as many cores as are reported to it. âmax_threadsâ itself is set up through various options, about which I have little clue. If you have more than 2 cores on your machine, something is fishy.

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?

Jasmin





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