[isabelle-dev] isabelle build

Makarius makarius at sketis.net
Wed Aug 8 13:32:04 CEST 2012

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_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.


More information about the isabelle-dev mailing list