[Agda] Agda interface generation memory consumption

[Dan Doel]

On Tuesday 09 February 2010 8:50:37 pm kahl at cas.mcmaster.ca wrote:
> I have been able to discern that the memory explosion happens after type
> checking is complete, while generating the interface file.
> This seems to manifest itself as a relatively short-lived, very sharp spike
> in memory consumption, and I haven't been able yet to get a good picture of
> it using heap profiling. (It seems that heap profiling tends to get less
> precise towards the end.)
> 
> Do you Agda experts know what is going on there?

I don't have a solution, but I have an additional 'test case' if the 
implementers want one, although it's essentially the same one as the last time 
this came up.

  http://code.haskell.org/~dolio/agda-share/categorica/Category/Product.agda

It needs a few other modules from the repository as can be seen. I've done a 
little work translating things to universe polymorphism rather than --type-in-
type, but it isn't complete, so I think only the modules that Category.Product 
depends on are valid.

Anyhow, I've actually been able to complete my proof that

  A × (B × C) ≅ (A × B) × C

this time, which I think is an improvement over the last time I attempted 
this. However, loading the complete module still takes 75% of my 2 GB of RAM. 
And now that it's been mentioned, the majority of the loading time does seem 
to happen after type checking. If I have a type error, it typically gets 
caught after perhaps 20 seconds, but actually loading the module probably 
takes 2 - 3 minutes. So most of the work must happen after the module has 
passed type checking.

Cheers,
-- Dan