[Agda] [ANNOUNCE] Agda 2.6.2 release candidate 2

[mechvel at scico.botik.ru]

On 2021-06-06 19:01, Nils Anders Danielsson wrote:
> On 2021-06-06 15:11, mechvel at scico.botik.ru wrote:
>> But the performance has reduced on  20%  relatively to  Agda-2.6.1 + 
>> ghc-8.8.3.
> 
>> 2.6.2.rc2 + ghc-9.0.1  spends 20% more of time.
> 
> If I understood you correctly you used two different versions of GHC.
> Can you rerun the test using one version of GHC?


Now I have installed  Agda-2.6.2.rc2 + master-lib-june-5  made under  
ghc-8.8.3.

And the example KTest runs 20% faster than in the same Agda made under 
ghc-9.0.1.
The example is
     http://www.botik.ru/pub/local/Mechveliani/docon-A/3.2rc/

  > cd source
  > agda $agdaLibOpt --auto-inline --guardedness +RTS -M15G -RTS 
Pol/KTest.agda
  > ./KTest

(may be  -M7G  is sufficient, but not the default one).

This refers to  Pol/KTest.agda,
the table
   {- Timing for  Agda-2.6.1, MAlonzo, ghc-8.8.3, Ubuntu-Libux 18.04,
      ....
   -}
The rows of  n = 12, 13,  in this table and the column of  pk.

First set the value in the line of  n = ...,
then command
      > agda $agdaLibOpt ... Pol/KTest.agda
      > ./KTest

When this Agda is made under ghc-8.8.3,
their times (on my machine) are
                                  7.7 sec,  24.6 sec.

When it is made under ghc-9.0.1, their times are
                                  9.5 sec,  29.6 sec.


> It should not matter what version of GHC you use to compile Agda, only
> which version you use to compile the Haskell code that is generated 
> from
> your Agda development.

   > which ghc
reports
   /home/mechvel/ghc/8.8.3/inst0/bin/ghc,

and  ghc-9.0.1 is not currently visible.
So, I think that ghc-8.8.3 is applied at all the stages
(if only Agda (MAlonzo?) does not apply any its local and hidden ghc).

For any occasion, I measure the time like this:

  > time ./KTest
  deg = 4096
  check = (0)
  |mons| = 4097
  coefSum = <79293 mod 99991>
  7.686u 0.183s 0:07.87 99.8%	0+0k 0+0io 0pf+0w

Then I round the first number to  7.7  and put it to the table.
It is important not to run any other expensive processes during this 
computation
(for example, not to run movies on the Web).
?

I have an impression that using  ghc-9.0.1  slows down running on 20%.
But I am no so sure.

It would be nice if someone repeats this experiment.
For all the source and instruction are given here.

And I do not know now whether it worth to make Agda-2.6.2.rc2 under 
ghc-9.0.1.

Regards,

------
Sergei