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

[Makarius]

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