[isabelle-dev] Proposal to use hierarchical heaps with Poly/ML

Rafal Kolanski xs at xaph.net
Fri Nov 13 06:45:30 CET 2015

On 12/11/15 16:45, Japheth Lim wrote:
> [...]
> A lot of space could be saved if Isabelle saves heaps in this way. For
> our L4.verified project we found a 7× reduction in size.

I would like to add that the 7x reduction is from 50GB for a full build
of all our heaps (i.e. regression test). This allowed me to keep using
my 250GB SSD, whereas previously I was struggling with space issues for
weeks. When Japheth committed this little change, my jaw just about hit
the floor.

No adverse effects so far. Thumbs up.

Rafal Kolanski.

More information about the isabelle-dev mailing list