[Agda] Performance tips and profiling memory usage

[Wolfram Kahl]

On Thu, May 02, 2019 at 10:37:36AM +0800, Matthew Daggitt wrote:
> The standard library has now reached the point where it's taking ~7GB of
> RAM to check

How did you measure? htop only tells you how much memory it uses, not
how much it needs. The GHC run-time system happily continues
allocating if you let it, hoping it never has to collect garbage...

What RTS options did you use?

Adding the options

  +RTS -s -RTS

gives you ``maximum residency'' which is most likely a lower bound for
the heap you really need.

Later messages said that checking std-lib works with:

  +RTS -M1.5G -RTS

I would then recommend to use:

  +RTS -M1.5G -H1.5G -A128M -RTS

Perhaps further fiddling with the allocation area size can make it
faster, but this rough magnitude should already be much faster than
the default.

And for knowing more about what is going on:

  +RTS -M1.5G -H1.5G -A128M -S -RTS

In Emacs on a 16G machine I currently have:

 '(agda2-program-args
   (quote
    ("+RTS" "-K256M" "-H6G" "-M6G" "-A128M" "-S/var/tmp/kahl/AgdaRTS.log" "-RTS" "-i" ".")))

(And then I run

  tail -f /var/tmp/kahl/AgdaRTS.log

 in a terminal to see how the heap moves while nothing moves in the
 emacs interaction...
)
(``-K256M'' for the stack only because I need it.)


On an 8GB machine, I would normally use no more than 5G of heap, and for
routine use and with small projects probably 2G.


For everybody venturing beyond simple exercises:

  NEVER RUN AGDA WITHOUT

    +RTS -M<<some number>>G -RTS

  !!! (Including from within Emacs!)
  And read:
    https://downloads.haskell.org/~ghc/latest/docs/html/users_guide/runtime_control.html#rts-options-to-control-the-garbage-collector

  If you called Agda without -M and it starts swapping, kill it --- no
  point in waiting.


Wolfram