[Agda] stack overflow when type check

Andrés Sicard-Ramírez andres.sicard.ramirez at gmail.com
Mon Apr 29 00:24:33 CEST 2013


On Sun, Apr 28, 2013 at 12:28 PM, Sergei Meshveliani <mechvel at botik.ru> wrote:
> People,
> when I compile as
>              agda -c $agdaLibOpt $agdaRTS +RTS -K200m -RTS  AlgTest.agda
>
> it works. But when I type-check one of its used modules in  interactive
> environment,  it reports
>                          stack overflow
>
> (the module is of 500 non-empty lines).
>
> What may be a way out? How to increase  stack  in the dialogue?

I adapted an old answer by Nils to the current version of Agda (untested):

Type M-x customize-group RET agda2 RET, then add the following
three entries to "Agda2 Program Args":

+RTS
-K200m
-RTS

(see also http://code.google.com/p/agda/issues/detail?id=714#c3 )

-- 
Andrés


More information about the Agda mailing list