[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