[isabelle-dev] Proposal to use hierarchical heaps with Poly/ML
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
No adverse effects so far. Thumbs up.
More information about the isabelle-dev