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-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Reply via email to