[isabelle-dev] NEWS:

[Lawrence Paulson]

This is a great achievement! And disk space is still important, especially on modern devices with SSDs. My machine has only 20 GB to spare.
Larry

> On 16 Mar 2016, at 22:33, Makarius <makarius at sketis.net> wrote:
> 
> *** System ***
> 
> * Poly/ML heaps now follow the hierarchy of sessions, and thus require
> much less disk space.
> 
> 
> This refers to Isabelle/c36a4495ba5f. Instead of a quick patch, it is the result of profound reforms of how heaps and processes are managed. This has become feasible after the dismissal of SML/NJ and old versions of Poly/ML. From now on we can follow new things provided by David Matthews more quickly.
> 
> 
> Here are some before/after numbers for the heaps directory for x86-linux:
> 
> build -a:               4GB ~> 0.8GB
> build -a -b:           23GB ~> 2.4GB
> build -a -b -d '$AFP': 96GB ~> 8.3GB  (without JinjaThreads)
> 
> The HOL image is really huge with 203MB. Without incorporating it, most sessions are rather small. Notable top entries > 100MB:
> 
> 230M HOL-Proofs
> 218M Collections
> 203M HOL
> 137M HOL-Library
> 
> 
> 	Makarius
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev