[Agda] Identifying inefficiency

[Guillaume Brunerie]

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.

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