[Agda] Agda interface generation memory consumption

[kahl at cas.mcmaster.ca]

Nils Anders Danielsson <nad at Cs.Nott.AC.UK> answered my question:

 > I could type check your problematic module
 > (Data.Algebra.Generalised.BisimCommutes) on my machine with less RAM. I
 > almost always use something like +RTS -M2G to limit the amount of heap
 > space allocated by Agda. In the case of your module I got the following
 > profile, with all the imports already type-checked, and the RTS options
 > -H2G and -M2G:

Thanks a lot!
(I found out that -s or -S produce the nice report you included.)

I now removed the postulate from the path to Semigroupoid,
and managed to get Data.Algebra.Generalised.Category type checked
(in 36 minutes), but only after splitting out
Data.Algebra.Generalised.BisimId (18 minutes).
Without the split, Data.Algebra.Generalised.Category0 runs out of heap
with my installation.

Also, I seem to have no way to show
Data.Algebra.Generalised.ConvSemigroupoid; splitting out first
Data.Algebra.Generalised.ConvOp and then
Data.Algebra.Generalised.ConvCommutes did not help;
all run out of heap.
(And the GHC RTS only gives me 2G of heap, even if I ask for 3G or 3.5G.
 I now believe that the out-of-memory crashes I had seen before
 occurred when Agda was trying to allocate more than 4G
 while running as a 32bit process in a 32bit userland.
 Without RTS options, memory consumption of agda processes grew
 to roughly twice of what I am seeing with the 2G restriction.)

I also tried to check
Data.Algebra.Generalised.ConvCommutes
without generating an interface file, and even that did not work in 2G.

(And on my laptop, I don't even have 2G!)

The development is now updated on:

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


I noticed that I cannot compile the lastest Agda development version
with my GHC-6.10.4 --- are you consciously abondoning GHC-6.10 already now?
GHC-6.12 apparently does not work on PowerPC  :-(


Wolfram