<html>
<head>
<meta content="text/html; charset=windows-1252"
http-equiv="Content-Type">
</head>
<body bgcolor="#FFFFFF" text="#000000">
<p><font size="+1">I've heard of negative thermal expansion in some
materials, but I don't think RAM is subject to it. (scnr)</font></p>
<p><font size="+1">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.</font></p>
<p><font size="+1">Perhaps the times when 32 Bit Isabelle was enough
for all applications are indeed over.</font></p>
<p><font size="+1"><br>
</font></p>
<p><font size="+1">Cheers,<br>
</font></p>
<p><font size="+1">Manuel<br>
</font></p>
<br>
<div class="moz-cite-prefix">On 08/08/16 13:06, Makarius wrote:<br>
</div>
<blockquote
cite="mid:d786e6c3-5787-f1a8-d34a-baff3572fc1a@sketis.net"
type="cite">
<pre wrap="">On 08/08/16 11:14, Lars Hupel wrote:
</pre>
<blockquote type="cite">
<pre wrap="">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.
</pre>
</blockquote>
<pre wrap="">
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.
</pre>
<blockquote type="cite">
<pre wrap="">Makarius, it may or may not be connected to
the recent changes you did in proof reconstruction (994d1a1105ef).
</pre>
</blockquote>
<pre wrap="">
This is merely for printing, which normally does not happen at all.
Makarius
_______________________________________________
isabelle-dev mailing list
<a class="moz-txt-link-abbreviated" href="mailto:isabelle-dev@in.tum.de">isabelle-dev@in.tum.de</a>
<a class="moz-txt-link-freetext" href="https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev">https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev</a>
</pre>
</blockquote>
<br>
</body>
</html>