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

I've just observed this effect below on the old Isabelle2013 on MacOS (Mavericks).

I even nondeterministically got "out of heap memory" and "too small initial heap size" while fiddling with the settings. The machine has 32G memory, and there were on the order of 10 log files only, so there's no way it actually ran out of memory parsing them.

Long story short: I still have no idea what got java so upset, but after a plain reboot everything worked just fine as usual with the default values.


On 06.11.2013, at 8:14 am, Makarius <makarius at> wrote:

> 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_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_JAVA_EXT=/home/haftmann/.isabelle/contrib/jdk-7u40/x86_64-linux/jre/lib/ext
>> 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.
>       Makarius


The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.

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