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

[Rafal Kolanski]

On 15/11/15 02:24, Makarius wrote:
> 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".

I never said "just do it". I said "thumbs up. That means the change
caused very significant positive effects and I second the desire to have
it looked at seriously in order to discover and mitigate any negative
effects. I just have none to report.