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



On Fri, 5 Feb 2016, Makarius wrote:

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

Here are the results of further experiments. For Isabelle2016, I've introduced certain "trim_context" operations that are mentioned in the NEWS as follows:

* Heap images are 10-15% smaller due to less wasteful persistent theory
content (using ML type theory_id instead of theory);


For HOL-AFP this yields on x86-linux:

Finished HOL (0:02:58 elapsed time, 0:10:58 cpu time, factor 3.69)      218M
Finished HOL-Lib (0:01:24 elapsed time, 0:05:45 cpu time, factor 4.10)  281M
Finished HOL-AFP (0:07:37 elapsed time, 0:37:15 cpu time, factor 4.89)  577M


Disabling the mechanism here https://bitbucket.org/isabelle_project/isabelle-release/src/f4baefee57768cf00b1a9e003770c7573b5d7378/src/Pure/thm.ML?at=default&fileviewer=file-view-default#thm.ML-410
yields the following:

Finished HOL (0:03:06 elapsed time, 0:11:21 cpu time, factor 3.66)      245M
Finished HOL-Lib (0:01:26 elapsed time, 0:05:54 cpu time, factor 4.11)  315M
Finished HOL-AFP (0:08:30 elapsed time, 0:39:52 cpu time, factor 4.69)  643M


Interestingly, the main HOL image has the same size of 218M in Isabelle2015. So the extra space provided by the system has been exactly consumed by the application -- this is a perfectly normal situation in Isabelle development.

I guess that on average bigger applications did not grow that much. For HOL-AFP, though, there seems to be a substantial increase in imports compared to Isabelle2015, but I did not check this systematically.

	Makarius




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