[Agda] testing Agda-2.6.1 on a large project

[mechvel at scico.botik.ru]

Dear all,

I have tested Agda 2.6.1 + lib-4.1 on a certain large project of 
computer algebra.

This is kind of a report about the _cost of type checking and 
compilation_.

Earlier it was DoCon-A-2.02 under Agda-2.5.4.2,
and it took the minimum of
                            13 Gb memory  to type-check,

and for  15 Gb  the type check took  2700 sec.  (on a 3 GHz machine).

Now it is rewritten into a certain  DoCon-A-3.0
under Agda-2.6.1 + lib-1.4, ghc-8.8.3, MAlonzo.

and it takes the minimum of
                          3 Gb memory  to type-check,

and for 3 Gb the type check takes  234 sec,
then, compilation takes ~ 300 sec.

So the type check cost has reduced about 4 times for memory and about 12 
times
for time.
This gives us a real hope for that a large part of computer algebra
(somewhat 10-20 times larger than this DoCon-A-3.0) can be type-checked 
and compiled in Agda at a reasonable cost.

The functionality of DoCon-A-3.0 is about 10% larger, it includes 
certified multivariate polynomial arithmetic.
But the design has changed.
* It is much more close to Standard library,
* parametrized modules are used more widely,
* generally, the design style is as it is traditional in Agda.

So that I cannot say that this is the very same library ported to 
Agda-2.6.1.

Regards,

------
Sergei