Re: [isabelle] Difficulties with "setsum" (Alfio Martini)



On Fri, 24 Apr 2015, Alfio Martini wrote:

Even with dont_try0 as a sledgehammer parameter, I get the same old timeout
results both
with Isa2014 and Isa2015-RC1. I havenÂt tried with Isa2015RC2 yet,

Operating System: Windows 8.1, 64-bit operating system
Ram Memory: 8GB
Processor: intel i5-3230M, 64 bit processor

That CPU has 2 cores and hyperthreading, i.e. 4 virtual cores. Can you try this:

  ML "Multithreading.max_threads_value ()"

There is some chance that it gives 4, because Cygwin is not reliable in reporting virtual CPU cores. Since starting external processes in parallel imposes an extra load on Cygwin, it might explain the timeout of the provers.

The Isabelle/jEdit plugin options offer the possibility to set "threads" explicitly, e.g. to 2. Does this change the situation?


	Makarius


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