[Agda] Performance tips and profiling memory usage

[Matthew Daggitt]

Thanks Wolfram, that's really useful.

What RTS options did you use?


None. The ones you suggested did indeed speed up type checking by 20%,
thanks! Maybe you could add a small page to the documentation with some
general suggestions? Or at least a link to the Haskell RTS documentation.
I'd never even heard of the RTS options before.
Best,
Matthew


On Fri, May 3, 2019 at 10:52 AM Wolfram Kahl <kahl at cas.mcmaster.ca> wrote:

> 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
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20190503/7aa1a102/attachment.html>