[isabelle-dev] isabelle build

[Makarius]

On Tue, 7 Aug 2012, David Matthews wrote:

> Just to add that JinjaThreads runs quite happily in a relatively small 
> amount of memory with the latest SVN version of Poly/ML.  6-8 Gbytes are 
> fine.  Even in 32-bit mode it takes around 33 minutes.

Yet another run on Gentoo Linux (lxbroy2, 4cores, Xeon, 64bit platform), 
running in 32bit mode again:

ISABELLE_BUILD_OPTIONS="threads=4 parallel_proofs=2"

ML_PLATFORM="x86-linux"
ML_HOME="/home/polyml/polyml-svn/x86-linux"
ML_SYSTEM="polyml-5.5.0"
ML_OPTIONS="-H 1000"

Finished JinjaThreads (0:25:18 elapsed time, 1:28:22 cpu time, factor 3.49)


The process size was fluctuating between 3.0--3.9 GB.  It is in fact the 
first time that I see a 32bit process approaching 4GB on Linux.  So far 
Mac OS was slightly better with its 3.3-3.5 GB.


 	Makarius