Re: [isabelle] [Isabelle2013-1 RC] Scalability problem with re-entrant build of the whole distribution

On Fri, 25 Oct 2013, Florian Haftmann wrote:

When building the whole distribution once and then once again (build
-a), the build process blows up after excessive machine resource
consumption (something like java.lang.OutOfMemoryError: Java heap
space). I did not try to diagnose it by putting hands on the code but I
am quite sure that this happens due to the log file analysis in
Pure/Tools/build.scala Build/build_results/load_timings.

My build runs take place on lxbroy10.

Relevant settings might include:
ML_OPTIONS=--heap 500
ISABELLE_SCALA_BUILD_OPTIONS=-nowarn -target:jvm-1.5
-Xmax-classfile-name 130
ISABELLE_JAVA_SYSTEM_OPTIONS=-Dfile.encoding=UTF-8 -server

That is a huge 64-bit machine with 128 GB RAM, but the above are mostly defaults to have the system run almost everywhere. Something like ISABELLE_BUILD_JAVA_OPTIONS="-Xmx4096m -Xss2m" should make the JVM more comfortable.

I don't know any better ways to configure JVM resources. Maybe one needs to pay Oracle for that. It is a bit like Mac OS in the 1980/1990-ies: before starting the program you need to give a limit for its resource requirements, but guessing wrong causes severe problems.

Maybe the mechanism itself is just not suitable to scale to the overall
amount of tons of log files. Is there any option to skip the log parsing?

Just delete the log files manually, as Stefan did.


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