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



This refers to fa80d47c6857.

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.

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?

My build runs take place on lxbroy10.

Relevant settings might include:
ISABELLE_POLYML=true
ML_IDENTIFIER=polyml-5.5.1_x86-linux
ML_OPTIONS=--heap 500
ISABELLE_SCALA_BUILD_OPTIONS=-nowarn -target:jvm-1.5
-Xmax-classfile-name 130
ISABELLE_BUILD_JAVA_OPTIONS=-Xmx1024m -Xss1m
ISABELLE_JAVA_EXT=/home/haftmann/.isabelle/contrib/jdk-7u40/x86_64-linux/jre/lib/ext
ISABELLE_JAVA_SYSTEM_OPTIONS=-Dfile.encoding=UTF-8 -server

	Florian

-- 

PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de




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