[Agda] [ANNOUNCE] Agda 2.6.2 release candidate 2

[mechvel at scico.botik.ru]

On 2021-06-06 00:07, Andrés Sicard-Ramírez wrote:
> Dear all,
> 
> The Agda Team is very pleased to announce the second release candidate
> (RC2) of Agda 2.6.2. We plan to release 2.6.2 in a few days.
> 


I have tested it on my application
   http://www.botik.ru/pub/local/Mechveliani/docon-A/3.2rc

under  MAlonzo, ghc-9.0.1, Ubuntu Linux 18.04.

It looks like working correct.
But the performance has reduced on  20%  relatively to  Agda-2.6.1 + 
ghc-8.8.3.

To keep the correspondence to 2.6.1, the keys --auto-inline 
--guardedness
are added to the making command.
The performance test for the polynomial arithmetic is made and run by

   > agda -c $agdaLibOpt --auto-inline --guardedness Pol/KTest
   > ./KTest

In  Pol/KTest   it is set  n = 12.
And its time (for pk) is  7.7 sec (on my 3 GHz machine) for 2.6.1 + 
ghc-8.8.3
- see the timing table and its column for pk.

2.6.2.rc2 + ghc-9.0.1  spends 20% more of time.

Setting there n = 13 also shows 20% overhead.

(There "kThreshold = 19" is a typo, in reality it is 18, and this 
difference must not be essential).

Also I have tested the polynomial arithmetic performance in Haskell for
ghc-8.8.3 and ghc-9.0.1.  The latter is  5%  slower.

20% is not so highly important, but some minor questions can arise.
I do not know, may be it worth to try various keys, may be, concerning 
inlining for `case_of_'
or such.
May be 2.6.2-rc2 applies different optimization keys ...

Regards,

------
Sergei