[Agda] type check performance

[Wolfram Kahl]

On Tue, Mar 31, 2015 at 03:15:25PM +0200, Nils Anders Danielsson wrote:
> On 2015-03-31 14:32, Sergei Meshveliani wrote:
> >Also the `top' command shows that  ghc  sometimes takes  98%  of the
> >16Gb memory despite this  -M10G.
> 
> The RTS options supplied to Agda are not forwarded to GHC. You can use
> --ghc-flag to set GHC flags:
> 
>   agda ... --ghc-flag=+RTS --ghc-flag=-M10G --ghc-flag=-RTS

With that, Agda remains running while GHC is running, too...
(The Agda process even remains quite active, but I don't know why.)
What I do to avoid having Agda and GHC fight for memory is passing

  --ghc-flag="-abort"

to Agda --- GHC implements the flag "-abort" by not recognising it ;-) .
After Agda finishes and GHC bails out on the "-abort", I call GHC
separately with a commend line derived from that displayed by Agda,
with appropriate RTS arguments added.


Wolfram