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

[Rafal Kolanski]

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.