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

  ML_OPTIONS="-H 2000"
  ISABELLE_USEDIR_OPTIONS="-i false -d false -M 4"
  HOL_USEDIR_OPTIONS="-p 2"

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.


	Makarius





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