Re: [isabelle] Incomplete goal may cause proof methods of later goals to loop.



On 22.04.2014 14:47, Makarius wrote:
> That is a relatively weak CPU, but Intel makes it appear stronger via
> hyperthreading, thus it gets somewhat overloaded and burns a lot of
> CPU cycles (literally, by turning them into heat).
You have now often recommended reducing the number of threads to the
number of real physical cores. Does this hold for interactive mode only?
Because on my machine (a quadcore with 8 virtual cores), there are
several theories in the AFP with a speedup factor around 5 or even 6; so
at least raw throughput sometimes profits from the virtual cores on
Isabelle workload.

  -- Lars




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