Re: [isabelle] Isabelle2016-RC3 -- jEdit build fails when session loaded from different directory



On Thu, 4 Feb 2016, Christian Sternagel wrote:

On 02/03/2016 09:40 PM, Makarius wrote:

Applications that really need more GBs -- presumably l4.verified is the
only one on the planet -- there is no other way than to move on to
bigger machines and the 64bit model.

Make this at least 2. IsaFoR already fails to build its session HOL-AFP
(which just brings together all the necessary theories from the AFP) in
32bit mode.

I have experimented with this a bit in the vicinity of Isabelle2016-RC. The precise versions are as follows:

IsaFoR:   61d9e42449c2
Isabelle: dfb70abaa3f0
AFP:      522c6c87f51e


HOL-AFP still works with x86-linux, leading to a heap image of 577M. Here are more details:

ML_PLATFORM="x86-linux"
ML_OPTIONS="-H 1500 --gcthreads 12"
isabelle build -b -o threads=12
Finished HOL-AFP (0:06:21 elapsed time, 0:47:49 cpu time, factor 7.53)

ML_PLATFORM="x86-linux"
ML_OPTIONS="-H 1500 --gcthreads 6"
isabelle build -b -o threads=6
Finished HOL-AFP (0:07:34 elapsed time, 0:37:10 cpu time, factor 4.91)


Trying "make all" of IsaFoR produces this result:

Building QTRS ...
Finished QTRS (0:02:02 elapsed time, 0:07:36 cpu time, factor 3.73)
Building Check-NT ...
Finished Check-NT (0:05:17 elapsed time, 0:22:26 cpu time, factor 4.24)
Building Processors ...

Processors FAILED
ML> Exception- SysErr ("Cannot allocate memory", SOME ENOMEM) raised
Proof-Checker CANCELLED
CeTA CANCELLED
Code CANCELLED


	Makarius




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.