<div dir="ltr">Thanks Wolfram, that's really useful.<div><br></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">What RTS options did you use?</blockquote><div><br></div><div>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.</div><div>Best,</div><div>Matthew</div><div> </div></div><br><div class="gmail_quote"><div dir="ltr" class="gmail_attr">On Fri, May 3, 2019 at 10:52 AM Wolfram Kahl <<a href="mailto:kahl@cas.mcmaster.ca">kahl@cas.mcmaster.ca</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">On Thu, May 02, 2019 at 10:37:36AM +0800, Matthew Daggitt wrote:<br>
> The standard library has now reached the point where it's taking ~7GB of<br>
> RAM to check<br>
<br>
How did you measure? htop only tells you how much memory it uses, not<br>
how much it needs. The GHC run-time system happily continues<br>
allocating if you let it, hoping it never has to collect garbage...<br>
<br>
What RTS options did you use?<br>
<br>
Adding the options<br>
<br>
  +RTS -s -RTS<br>
<br>
gives you ``maximum residency'' which is most likely a lower bound for<br>
the heap you really need.<br>
<br>
Later messages said that checking std-lib works with:<br>
<br>
  +RTS -M1.5G -RTS<br>
<br>
I would then recommend to use:<br>
<br>
  +RTS -M1.5G -H1.5G -A128M -RTS<br>
<br>
Perhaps further fiddling with the allocation area size can make it<br>
faster, but this rough magnitude should already be much faster than<br>
the default.<br>
<br>
And for knowing more about what is going on:<br>
<br>
  +RTS -M1.5G -H1.5G -A128M -S -RTS<br>
<br>
In Emacs on a 16G machine I currently have:<br>
<br>
 '(agda2-program-args<br>
   (quote<br>
    ("+RTS" "-K256M" "-H6G" "-M6G" "-A128M" "-S/var/tmp/kahl/AgdaRTS.log" "-RTS" "-i" ".")))<br>
<br>
(And then I run<br>
<br>
  tail -f /var/tmp/kahl/AgdaRTS.log<br>
<br>
 in a terminal to see how the heap moves while nothing moves in the<br>
 emacs interaction...<br>
)<br>
(``-K256M'' for the stack only because I need it.)<br>
<br>
<br>
On an 8GB machine, I would normally use no more than 5G of heap, and for<br>
routine use and with small projects probably 2G.<br>
<br>
<br>
For everybody venturing beyond simple exercises:<br>
<br>
  NEVER RUN AGDA WITHOUT<br>
<br>
    +RTS -M<<some number>>G -RTS<br>
<br>
  !!! (Including from within Emacs!)<br>
  And read:<br>
    <a href="https://downloads.haskell.org/~ghc/latest/docs/html/users_guide/runtime_control.html#rts-options-to-control-the-garbage-collector" rel="noreferrer" target="_blank">https://downloads.haskell.org/~ghc/latest/docs/html/users_guide/runtime_control.html#rts-options-to-control-the-garbage-collector</a><br>
<br>
  If you called Agda without -M and it starts swapping, kill it --- no<br>
  point in waiting.<br>
<br>
<br>
Wolfram<br>
</blockquote></div>