[Agda] [ANNOUNCE] Agda 2.6.2 release candidate 2

mechvel at scico.botik.ru mechvel at scico.botik.ru
Tue Jun 8 14:36:56 CEST 2021


On 2021-06-06 17:43, Martin Escardo wrote:
> 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.
> 


Martin, thank you.
I shall try all this.

As I understand,  -foptimise-heavily  is only for the `cabal install' 
command
when making Agda,
and  --auto-inline  is only for the `agda' command when type checking 
.agda modules
(please, correct me if this is not so).

------
Sergei



> 
> 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.
>> [..]


More information about the Agda mailing list