On Tue, 7 Apr 2015, Christian Sternagel wrote:
PS: I'm still waiting for
isabelle build -n -a -d '$AFP' -k qualified
to finish (but I guess proper checking, taking semantics into account, is
just expensive). Oops, while writing this email I obtained:
*** java.lang.OutOfMemoryError: Java heap space
0:03:32 elapsed time, 0:05:46 cpu time, factor 1.63
(Maybe because in parallel I am still waiting on
isabelle build -v -n -a -d '$AFP' -k hidden -k private
? Which seems to "hangs" at "Session Pure/RAW" now for several minutes.)
Maybe this is just the normal behaviour of the JVM under low-memory
conditions. I routinely have local settings like this:
ISABELLE_BUILD_JAVA_OPTIONS="-Xms1024m -Xmx4096m -Xss4m"
This can't be as aggressive by default, because it means it won't work at
all on small / 32bit machines.
Makarius
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
