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

[Makarius]

On Fri, 13 Nov 2015, Rafal Kolanski wrote:

> 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.

I usually trust David Matthews doing great things.

Just formally, any change to make it into the official producation quality 
version of Isabelle needs some extra efforts.  It happens routinely that 
old questions in the vicinity of a new feature need to be revisited.  If 
this is not done, there is a slow degration of overall structural 
integrity of the system.

One needs to resist from an attitude like "works for me, all great, no 
problems, just do it".


 	Makarius