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