[Agda] Agda interface generation memory consumption

[Nils Anders Danielsson]

On 2010-02-10 01:50, kahl at cas.mcmaster.ca wrote:
> 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/

Thanks for the example.

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:

  117,981,545,772 bytes allocated in the heap
    6,466,725,572 bytes copied during GC
    1,684,936,324 bytes maximum residency (13 sample(s))
        7,594,984 bytes maximum slop
             2047 MB total memory in use (16 MB lost due to fragmentation)

   Generation 0:   401 collections,     0 parallel, 35.80s, 35.92s elapsed
   Generation 1:    13 collections,     0 parallel, 89.27s, 89.53s elapsed

   INIT  time    0.00s  (  0.00s elapsed)
   MUT   time  231.70s  (233.72s elapsed)
   GC    time  125.07s  (125.45s elapsed)
   EXIT  time    0.00s  (  0.00s elapsed)
   Total time  356.77s  (359.17s elapsed)

   %GC time      35.1%  (34.9% elapsed)

   Alloc rate    509,202,935 bytes per MUT second

   Productivity  64.9% of total user, 64.5% of total elapsed

The total time needed to type check your example is still rather high,
though.

--
/NAD