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

[Manuel Eberl]

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.

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

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20160808/4e621708/attachment-0002.html>