[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