[Agda] [ANNOUNCE] Agda 2.6.2.1 release candidate

mechvel at scico.botik.ru mechvel at scico.botik.ru
Mon Dec 6 12:24:52 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.
> 


I have tested it on my library for computer algebra (large enough).
Mainly, it looks all right.

There are the following points.
1) The question of how to restrict memory for compilation (reported a 
day ago).
2) The regression effect remains for  ghc-8.8.3 --> ghc-9.*.

The second was reported about an year ago:
   Agda-2.6.2 with ghc-9.*  produces 25% slower code  than Agda-2.6.2 
with ghc-8.8.3.

I mean the performance of the executable produced by
   agda -c $agdaLibOpt $agdaFlags Foo.agda  +RTS -M7G -RTS 
--ghc-flag="-rtsopts",

   $agdaFlags = --auto-inline --guardedness

Similarly
   Agda-2.6.2.0.20211129 with ghc-9.*  is 25% slower than  Agda-2.6.2 
with ghc-8.8.3.

Regards,

------
Sergei


More information about the Agda mailing list