[Agda] [ANNOUNCE] Agda 2.6.2 release candidate

[Andrés Sicard-Ramírez]

Hi Sergei,

Thank you for your feedback.

On Sat, 5 Jun 2021 at 15:29, <mechvel at scico.botik.ru> wrote:
> And in this candidate for Agda-2.6.2 + ghc-9.0.1
> 24G is not sufficient to type-check this in any reasonable time.

>From CHANGELOG.md:

* New option `--auto-inline` turns on automatic compile-time inlining
  of simple functions. This was previously enabled by default.

  Note that the absence of automatic inlining can make typechecking
  substantially slower.


I could type-check your program in 8 min, on GHC 8.10.4, using Agda
2.6.2 RC2 and the experimental branch of the standard library by
running:

    `agda --auto-inline +RTS -M7G -RTS Pol/Karatsuba.agda`

(I couldn't type-check your program without using the `--auto-inline` option.)

Best,

-- 
Andrés