[Agda] [ANNOUNCE] Agda 2.5.1 release candidate 2

Sergei Meshveliani mechvel at botik.ru
Thu Apr 14 15:42:48 CEST 2016


On Thu, 2016-04-14 at 08:25 -0500, Andrés Sicard-Ramírez wrote:
> On 14 April 2016 at 06:38, Sergei Meshveliani <mechvel at botik.ru> wrote:
> > 3. I try
> >    agda -c $agdaLibOpt +RTS -M9G -RTS  Foo.agda
> >
> >    ./Foo +RTS -M2G -RTS
> >
> > , and it reports   "link with the -rtsopts".
> 
> Did it work before?
> 
> > Please, how precisely needs one to use  -rtsopts ?
> 
> The -rtsopts option should be used by the GHC backend when generating
> the Foo executable.
> 

I am sorry.
I recall now how to use it. This is to add  
                                  
         --ghc-flag=-rtsopts

to the  `agda -c'  command.
This makes it "linking with -rtsopts".

Regards,

------
Sergei






More information about the Agda mailing list