[Agda] Size limit on generated code?

[Wolfram Kahl]

On Sun, Sep 28, 2014 at 05:00:14PM +0800, Roly Perera wrote:
> After a couple of days of experimentation, I've concluded it's
> impractical to compile binaries from my test cases. Compilation takes
> up to 30 minutes,

This is ``only'' a scheduling problem...

> and often fails unpredictably with out-of-memory
> some chunk of the way through.

Right now part of the problem is that Agda remains running,
and active, during GHC compilation, and competes with GHC for heap space.
you first of all want to pass heap-limiting options to GHC
(+RTS -M3G -H3G -RTS) (after having passed something similar to Agda),
which at least keeps both of them within predictable bounds.
(Keeping both processes out of swap also makes things go a lot faster.
 keep htop running in a visible terminal whenever you use Agda.
)
This approach has been sufficient fo me so far with 16GB of RAM,
but not by a wide margin...

If this is not enough, then as long as Agda does not offer a
more direct remedy, identify the GHC command issued by Agda,
kill Agda after it started that command, and restart that command
manually, without running Agda --- and likely with more heap.


Hope this helps!


Wolfram


P.S.: See also http://code.google.com/p/agda/issues/detail?id=1163