[isabelle-dev] Fwd: [Isabelle-ci] Build failure in Isabelle

[Tobias Nipkow]

On 08/08/2016 13:13, Manuel Eberl wrote:
> I've heard of negative thermal expansion in some materials, but I don't think
> RAM is subject to it. (scnr)
>
> In a more serious fashion: I don't see how ambient temperature could affect
> memory usage. I've run into "insufficient memory" and stack overflow problems in
> Isabelle several times lately, usually sporadically and irreproducibly.

On my laptop this happens fairly reliably for some time now with HOL-Proofs or 
related sessions. I played around with PolyML parameters, but to no avail.

Tobias

> Perhaps the times when 32 Bit Isabelle was enough for all applications are
> indeed over.
>
>
> Cheers,
>
> Manuel
>
>
> On 08/08/16 13:06, Makarius wrote:
>> On 08/08/16 11:14, Lars Hupel wrote:
>>> the latest build failure for the repository is spurious:
>>>
>>> *** exception Fail raised (line 83 of "./basis/PolyMLException.sml"):
>>> Insufficient memory
>>>
>>> This happened in HOL-Proofs.
>> I have tried Isabelle/1e7c5bbea36d once again with
>>
>>   ML_PLATFORM="x86-linux"
>>   ML_HOME="/home/makarius/.isabelle/contrib/polyml-5.6-1/x86-linux"
>>   ML_SYSTEM="polyml-5.6"
>>   ML_OPTIONS="-H 1000 --gcthreads 2"
>>
>> The result is:
>>
>> Finished HOL-Proofs (0:17:18 elapsed time, 0:33:38 cpu time, factor 1.94)
>>
>>
>> Is the test hardware in an air-conditioned server room? Otherwise we
>> might be actually testing the surrounding temperature or some other
>> environmental effects.
>>
>>
>>> Makarius, it may or may not be connected to
>>> the recent changes you did in proof reconstruction (994d1a1105ef).
>> This is merely for printing, which normally does not happen at all.
>>
>>
>> 	Makarius
>>
>> _______________________________________________
>> isabelle-dev mailing list
>> isabelle-dev at in.tum.de
>> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
>
>
>
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
>

-------------- next part --------------
A non-text attachment was scrubbed...
Name: smime.p7s
Type: application/pkcs7-signature
Size: 5135 bytes
Desc: S/MIME Cryptographic Signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20160808/721db256/attachment.bin>