[Agda] [lean-user] Re: [Coq-Club] Why dependent type theory?

[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.
>