[Agda] [ANNOUNCE] Agda 2.6.2 release candidate 2

[Martin Escardo]

You also need to install agda, if you use cabal, with -foptimise-heavily.

The omission of this option adds 25% to the type checking time.

The omission of the option --auto-inline, mentioned earlier, also adds 25%.

So the omission of both adds 50%.

The omission of these two options is now the default.

This is the case, at least, in one of my Agda developments, whose type
checking time goes from 4 to 6 minutes.

So you need to add them both to regain the performance of Agda 2.6.1. At
least I do.

M.

On 06/06/2021 14:11, mechvel at scico.botik.ru wrote:
> 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
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda

-- 
Martin Escardo
http://www.cs.bham.ac.uk/~mhe