[Agda] [ANNOUNCE] Agda 2.6.2.1 release candidate

mechvel at scico.botik.ru mechvel at scico.botik.ru
Sun Dec 5 22:48:00 CET 2021


On 2021-11-30 00:43, Andreas Abel wrote:
> The Agda Team is pleased to announce a release candidate for Agda 
> 2.6.2.1:
> 
>     https://hackage.haskell.org/package/Agda-2.6.2.0.20211129/candidate
> 
> 2.6.2.1 will be mostly a bugfix release, and will build in the latest
> Haskell ecosystem (GHC 9.2.1, aeson-2.0, hashable-1.4,
> hashtables-1.3).
> For detailed comparison with 2.6.2, consult the changelog published
> with the candidate above.
> 
> Instructions how to test the candidate are available at:
> 
>     https://github.com/agda/agda/pull/5678
> 
> Please report any regressions over 2.6.2 at the Agda issue tracker.
> We plan to release Agda 2.6.2.1 next week, should not release-stopping
> regressions be reported.
> 

Can you, please, explain how to restrict the memory for compilation?
For the type checking, it works
   $ agda $agdaLibOpt $agdaFlags Foo.agda  +RTS -M7G -RTS

Then I try compilation (MAlonzo ...):

   $ agda -c $agdaLibOpt $agdaFlags Foo.agda  +RTS -M7G -RTS 
--ghc-flag="-rtsopts"

It reports things like
   [215 of 218] Compiling MAlonzo.Code.GenAlgebraZ45ZIV ( 
MAlonzo/Code/GenAlgebraZ45ZIV.hs,
    MAlonzo/Code/GenAlgebraZ45ZIV.o ),

and the `top' command shows the current memory usage of about  16 Gb 
instead of 7.
And the process that takes it is identified as  ghc.

My aim is to find out whether the project can be compiled on a  8 Gb  
machine.
I tried to append there
   --ghc-flag="+RTS" --ghc-flag="-M7G"

but this is not accepted.

Thanks,

------
Sergei


This is  Agda-2.6.2.0.20211129/candidate,
          Ubuntu Linux 18.04, ghc-9.2.1,  MAlonzo.


More information about the Agda mailing list