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
I have experimented with this a bit in the vicinity of Isabelle2016-RC.
The precise versions are as follows:
HOL-AFP still works with x86-linux, leading to a heap image of 577M. Here
are more details:
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_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 ...
ML> Exception- SysErr ("Cannot allocate memory", SOME ENOMEM) raised
This archive was generated by a fusion of
Pipermail (Mailman edition) and