[Agda] stack overflow when type check

Sergei Meshveliani mechvel at botik.ru
Tue Apr 30 08:18:30 CEST 2013


On Sun, 2013-04-28 at 17:24 -0500, Andrés Sicard-Ramírez wrote:
> On Sun, Apr 28, 2013 at 12:28 PM, Sergei Meshveliani <mechvel at botik.ru> wrote:
> > [..]
> >              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
> > [..]
> > 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 )
> 


It works. Thank you.
Certain details:
1) before `customize-group',  it also needs  `load-library',
2) +RTS, -K200m, -RTS   are set in different fields, not in one line.

Regards,

------
Sergei



More information about the Agda mailing list