Re: [isabelle] Incomplete goal may cause proof methods of later goals to loop.
I'd just like to add that this problem can be compounded by some other
issues, such as one we mentioned before where a diverging "blast" can
slow down jEdit. On rare occasions I've had to go hunting for blasts and
fastforces in the future part of my theory just to get enough CPU back
to work on the problem I have.
Not sure what else to say about it, but if some improvement to the
prioritising of these speculative calculations could be made, I'd be all
On 22/04/14 23:22, Makarius wrote:
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 quite fast.
This archive was generated by a fusion of
Pipermail (Mailman edition) and