[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