[isabelle-dev] NEWS: limited name space accesses

[Makarius]

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