[Agda] [ANNOUNCE] Agda Standard Library v2.1 - release candidate 2

[mechvel at scico.botik.ru]

Let me add a certain general note.
I have an impression that the compiled code of applications written in 
Agda
currently runs 3/2 times slower than it was 5-7 yeas ago.
My tests contain the records like

---------------------------------------------------------------------
Agda-2.6.2, MAlonzo, ghc-8.8.3, Ubuntu-Libux 18.04, 3 GHz machine,  (~ 
2019)
-M7G  for memory.
Agda-2.6.3, ghc-9.2.1, 9.2.7.               (~ 2022).
Agda-2.6.4.3, ghc-9.0.2, lib-2.1.rc1,rc2    (July 2024).

A certain computation with univariate polynomials over the coefficients 
in (Integer modulo p)
programmed in two methods.

The test for different  n = deg f  for  f  having n+1 (nonzero 
monomials)
(that is put m = 1).
Comparing the time for the two methods for n = 1000, 2000, ...

               time[sec]
   n   | p-p,     | pₖ-pₖ,    | deg p | l(mons) | coefSum
       | deg p,   | deg pₖ,   |       |         |
       | length p | length pₖ |       |         |
--------------------------------------------------------
  1000 |    2.53  |     0.82  |  2000 |   1999  | <97043>
            3.75  |     1.17                               - 2.6.3
                        2.2
  ...
  4000 |   41.5   |     7.5   |  8000 |   7999  | <99057>
           53.1   |     9.4                                - 2.6.2.1 + 
ghc-9.2.1
	  66.9 ? |    11.3                                - 2.6.4 + ghc-9.2.7
                       11.0                                - 2.6.4.3 + 
ghc-9.0.2
                       11.9                        -- lib-2.1-rc2
--------------------------------------------------------

Here the time monotonously increases during several years from  7.5 sec 
to 11.9.
I suspect that the main impact is brought by upgrading from ghc-8.8.3 to 
higher GHC versions
(I wonder about Linux versions).
I do not think that this 3/2 is so important.
This is just an observation.

I expect that most people think that Agda is only for proofs.
But I naively expect of Agda that it also supports fast programs to 
perform computer algebra
methods. The idea is that the source code in Agda is more cultured 
mathematically,
it is possible a mathematically adequate style.


On 2024-07-11 22:59, mechvel at scico.botik.ru wrote:
> On 2024-07-11 06:30, Matthew Daggitt wrote:
>> Dear all,
>> 
>> The Agda Team is pleased to announce the second release candidate for
>> version 2.1 of the Agda standard library. The release candidate has
>> been tested using Agda 2.6.4.3 and can be downloaded here [1]. We
>> would be grateful for reports of any issues you may encounter with the
>> new version of the library on the Github issues page [2].
>> 
> 
> I have tested it on my large application on agda 2.6.4.3, MAlonzo;
> ghc-9.02, Debian Linux 10.
> It does not show any deviation from old tests.