Re: [isabelle] HOL for x86_64 Linux?
On Fri, 16 May 2008, Rafal Kolanski wrote:
> If you have multiple cores, there's some theory loading stuff isabelle can
> parallelise. In Proof General: set Isabelle->Settings->Max Threads to however
> many cores you have.
> Use the -M option of isabelle usedir. Here's the line from my
> ~/isabelle/etc/settings for four cores:
> ISABELLE_USEDIR_OPTIONS="-M 4 -p 1 -v true -V outline=/proof,/ML"
> This will give you funky numbers like:
> Building HOL ...
> Finished HOL (0:02:35 elapsed time, 0:02:58 cpu time)
> (2.4GHz intel Q6600)
> Welcome to the 64-bit world, and I hope there's more parallelism coming from
> the Isabelle creators :)
More parallelism is definitely coming, but this is orthogonal to the 64bit
platform. In fact, Poly/ML on x86_64 is almost 2 times slower than the
x86 version, because the internal word size is uniformly 64bit.
See http://isabelle.in.tum.de/devel/stats/at-mac-poly-5.1-para.html for
some performance charts for a quad-core 32bit Mac using
ISABELLE_USEDIR_OPTIONS="-i false -d false -M 4"
Right now, 64bit only helps if significantly more heap space than 2GB is
being used, or if you happen to need more stack space than 64MB. Otherwise
plain x86 mode is adequate even on x86_64 machines.
This archive was generated by a fusion of
Pipermail (Mailman edition) and