The Coq mailing list

[mechvel AT scico.botik.ru]

Continuing a sub-discussion about the  type check performance,

I add that I have tried now the current Development Agda version (March 
5, 2020).

I compare it to the last official version of 2.6.0.1
at a certain BFLib project (Binary Integer + General Fraction 
arithmetcic).
This library is may be 5 times smaller than DoCon-A, but it is large in 
comparison to
usual Agda application practice.

It is applied
      > time agda $agdaLibOpt BRationalTest.agda  +RTS -M<size> -RTS

(on  ghc-8.8.3, Ubuntu Linux 18.04, 3 GHz personal computer)

which type-checks everything in the given memory space.
Development Agda type-checks it in the minimum of  1400 Mb memory,
it is about 1.5 times less space eager and 20% faster.

This gives a certain hope, assuming that 2.6.0.1 probably wins something 
relatively to
the versions of 2017.
This needs testing and effort in upgrading DoCon-A.

Regards,

------
Sergei



On 2020-03-04 20:07, 
mechvel AT scico.botik.ru
 wrote:
> On 2020-03-04 14:22, 
> mechvel AT scico.botik.ru
>  wrote:
> > On 2020-03-04 02:04, Jason Gross wrote:
> > > I'm confused by this.  Are you saying that in Agda typechecking is
> > > exponential in the number of files?  Or exponential in the number of
> > > nested abstractions?  Or something else?  Do you have a toy example
> > > demonstrating this behavior?
> >
> > No toy example, so far, but I think such can be provided.
> >
> > I have a real-world example of the DoCon-A library for algebra:
> >
> >   http://www.botik.ru/pub/local/Mechveliani/docon-A/2.02/
> >
> > This is a small part of the intended general purpose library for 
> > algebra
> > (for algebra methods, it is very small, but comparing to the Agda
> > practice, it is large).
> >
> > It is written in  install.txt
> > "for the  -M15G  key  (15 Gb heap) installation takes about 50 minutes 
> > on a
> >  3 GHz personal computer.
> > "
>
>
> I am sorry.
>
> I need to add the following.
> This as about the Agda versions of about  2017.
>
> It may occur that the current Agda version improves something there.
> This needs testing, needs more effort in porting the library.
> I use the last Agda versions, but on certain smaller projects.