With darcs version from the evening of 20070530, some files take incredibly long to compile and memory usage explodes. On the last attempt to compile Fam.agda in this tarball, which I suspect would typecheck, I had to kill agda after about 20 minutes of compilation, with >75% of ram (512M on this machine) and a lot of swaping. It would have been oomkilled soon anyway.
If this isn't a memory leak somewhere, then there is a huge performance issue...
NB: if it's possible, try increasing the maximum size allowed for attachments, I couldn't upload this one.
Just for fun, I launched the compilation during the night and it was finished by morning, without having been oom-killed. It reported 136 unsolved metas, perhaps there is a link?
Here is the result of a profiling of agda when running on this program. It was obtained with -prof -auto-all to ghc and +RTS -p -RTS to agda.
One problem might be the size of the terms. Some debug printing revealed that some metavariables were instantiated with terms of more than 100,000 constructors. Metavariable instantiations are in normal form so one way to improve the situation is to reduce the size of the normal forms. There are two standard tricks:
- Make things abstract. Works for any definition, but once it's abstract you can never look inside.
- Wrap things in datatypes. Only works for type valued things. Possible to look inside by manually stripping the constructor.
It's possible that the eta-equality on records also carries a performance penalty.