[Agda] Type-checker evaluator performance

[Wolfram Kahl]

Hi Liam,

  I am not addressing your real concern, but this may still
give you better chances of having your stuff type-checked in general:

 > I found that Agda would just get OOM killed before
 > finishing, and it would take at least 10 minutes before getting
 > OOM-killed, using all 8GB of my RAM and 4GB of my swap.

I recommend to NEVER run Agda without specifying the heap,
e.g.:

  agda +RTS -M6G -H6G -A128M -S -RTS -i . -i $(agdalib) MyModule.lagda

(Also run htop in another terminal to see what is going on.
    http://hisham.hm/htop/
)

-M6G   Maximal heap.
   With certain workloads, Agda will use any size of heap,
   even though it might also succeed with smaller size.
   And it does not know about your RAM and swap sizes...
   So even though your run used all of your 12G of RAM+swap,
   it may still succeed with -M6G. (But it also may not...)

   If you kill your firefox first, you may be able to go to 6.5G
   or even 7G. If you work without desktop environment, and preferably also without X11,
   perhaps even 7.2G to 7.5G.
   A stopped firefox can be pushed out into swap, but a live firefox will fight back.
   (A swapped-out firefox takes ages to swap back in, so better kill it,
    and restore session later.)
   If you give Agda -M7.2G in your normal environment,
   it will push out everything else (that does not fight back sufficiently) into swap,
   and if it succeeds, then run mostly happily.
   But don't move your mouse nor expect reactions from your terminals and window managers.
   If you don't limit Agda's heap: Once Agda starts swapping its own pages,
   you can forget it: Kill it.

-H6G  Start heap: If your Agda process is going to be big anyway, give it that start heap.
   You will see that it does not ask for all of it from the OS immediately,
   but only when it finds a use for it.
   For some small tasks (I believe including the standard library),
   Agda never uses a large heap.
   But if it does need a large heap, and you specified a smaller start heap
   (e.g. by not passing -H), the GHC RTS will waste quite some time growing it
   in small increments.

-A128M  Allocation area: Perhaps surprisingly, this makes my Agda runs much faster,
   by taking out the nervousness from the garbage collector.
   On my 16G machines, I normally run +RTS -M10G -H10G -A1G -S -RTS.

-S (only when running from the command line):
  See how much heap is live after each garbage collection.
  If you see it doing major (i.e., generation 1) garbage collections all the time,
  just below the max heap size, it is spending fmost of its time garbage collecting,
  and not getting any work done; then it is normally only going to be a question of time
  (minutes to hours) until it runs out of heap, so you might just as well kill it,
  and restart it with more heap if possible.
  Another pattern I am seeing occasionally: It grows the live heap extremely slowly,
  doing only minor collections for hours. This tends to be deadly;
  I have had it run for a week until it ran out of 50GB heap.

I have recently only used Agda as 64-bit executable; I have modules that need 5G,
6G, 8G, 9G, 10G, 11G, 13.5G. I have occasionally run Agda in heaps as large a 256G,
but so far have never seen anything typecheck that didn't also check with just 14G.


Hope this helps!


Wolfram