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-...@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


Attachment: smime.p7s
Description: S/MIME Cryptographic Signature

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

Reply via email to