Re: [isabelle] Incomplete goal may cause proof methods of later goals to loop.
On Tue, 22 Apr 2014, Lars Noschinski wrote:
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
I also do systematic "overburning" of CPU cycles in batch mode, it gives
me (real) warp factor 9.6 for 8 real cores (Intel Xeon from 2009) --
hyperthreading actually has a purpose. Concerning the "factor" one needs
to be careful, though: the figure given in Isabelle build on the spot is
merely the relative burn-factor of CPU cycles, and that is a quite
distorted version of the true speed-up factor compared to sequential mode.
So yes, one could probably make this a general rule of thumb: interactive
mode refers to physical CPU cores and batch more to the maximum number of
virtual CPU cores, even more.
I usually get that effect by having the persistent default options as
described before, which will be also the default in the next release.
For batch builds I then give a generous -j4 to the implicit -o threads=4.
In this "4x4" mode (which means "4-wheel drive" in French), I get the
"sound of speed" in my office from the CPU fans, and Isabelle + AFP built
This archive was generated by a fusion of
Pipermail (Mailman edition) and