Re: [isabelle] [Isabelle2013-1 RC] Scalability problem with re-entrant build of the whole distribution
- To: Florian Haftmann <florian.haftmann at informatik.tu-muenchen.de>
- Subject: Re: [isabelle] [Isabelle2013-1 RC] Scalability problem with re-entrant build of the whole distribution
- From: Makarius <makarius at sketis.net>
- Date: Tue, 5 Nov 2013 22:14:22 +0100 (CET)
- Cc: USR Isabelle Mailinglist <isabelle-users at cl.cam.ac.uk>
- In-reply-to: <526ACD97.email@example.com>
- References: <526ACD97.firstname.lastname@example.org>
- User-agent: Alpine 2.00 (LNX 1167 2008-08-23)
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
My build runs take place on lxbroy10.
Relevant settings might include:
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
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