[Agda] Size limit on generated code?

[Roly Perera]

Thanks Wolfram, those are all useful tips. (Unfortunately my laptop
only has 3.5GB, though.)

I've decided it will be faster to reimplement the bits I want to run
in Haskell. Not ideal but probably the best solution given that I want
to do a fair bit of interactive experimentation.

On 29 September 2014 00:45, Wolfram Kahl <kahl at cas.mcmaster.ca> wrote:
> 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