[isabelle-dev] NEWS:
Makarius
makarius at sketis.net
Wed Mar 16 23:33:17 CET 2016
*** 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
More information about the isabelle-dev
mailing list