[Agda] Agda interface generation memory consumption

[kahl at cas.mcmaster.ca]

In ``darcs changes'', I found some time ago:

 | Tue Jan 12 14:03:41 EST 2010  Nils Anders Danielsson
 | <nils.anders.danielsson at gmail.com>
 |   * Less aggressive eta expansion of record metas.
 |   + Should make code involving lots of records faster. We have a test
 |     case which runs [_\e2_][_\88_][_\bc_]5 times faster.
 |   + Implemented together with Ulf.


This is wonderful! Thanks a lot!

(With the teaching this term, it just took me until now to really try it out.)

I have such cases too, and they are not just test cases, but in the main
line of my development, of a category-based relation-algebraic approach to
graph transformation.

However, in many cases, it only means that I get to the out-of-memory crash
five times faster --- I documented the case that is currently my problem:

  http://sqrl.mcmaster.ca/~kahl/RATH/Agda/

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?



Wolfram