[isabelle-dev] NEWS: limited name space accesses

Christian Sternagel c.sternagel at gmail.com
Fri Apr 17 20:14:36 CEST 2015


On 04/17/2015 12:04 AM, Makarius wrote:
> 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"

Thanks for the hint! This even worked with two "checks" running in 
parallel (each of which finished in less than 4 minutes).

cheers

chris




More information about the isabelle-dev mailing list