[Agda] Identifying inefficiency

[Martin Escardo]

On 26/03/2019 15:01, guillaume.brunerie at gmail.com wrote:
> You can turn on interactive highlighting (setting the variable
> "agda2-highlight-level" to "interactive"), and then when loading a
> file in emacs you can see where the highlighting gets "stuck".
> 
> Another option is to run agda from the command line with the options "
> -v profile:7 ", and you will get a breakdown of which part of Agda
> took a long time (e.g. LHS checking, positivity, termination checking,
> and so on), which might help to identify different sources of
> inefficiency.

Thanks. I already knew it is a single definition (or more precisely a 
pair of definitions in a where clause of that definition). Now I know 
that all the time is spent as

Typing.CheckRHS              30,715ms

With the RHS's replace by "?", typechecking is instant.

(I tried supplying all the implicit arguments to the RHS's, but the 30s 
time remains the same.  At the holes, the types of the subterms of the 
terms that I want to fill the holes with is known, so I am not sure what 
is going on. But I guess this is a different question from the one in 
this thread.)

Martin




> 
> Best,
> Guillaume
> 
> Den tis 26 mars 2019 kl 15:11 skrev Martin Escardo <m.escardo at cs.bham.ac.uk>:
>>
>> I have a file with 339 lines only that takes 31s to type check.
>>
>> (Then on the same computer a development of 25k lines without comments
>> takes 3m 20s to type check.)
>>
>> I can find the place where the inefficiency takes place by manual bisection.
>>
>> Is there a better way?
>>
>> M.
>> _______________________________________________
>> Agda mailing list
>> Agda at lists.chalmers.se
>> https://lists.chalmers.se/mailman/listinfo/agda

-- 
Martin Escardo
http://www.cs.bham.ac.uk/~mhe