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
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
