[Agda] performance debugging?

[Nils Anders Danielsson]

On 2023-09-28 02:57, Robby Findler wrote:
> Ah, sorry. I was asking about this change:
> https://github.com/agda/agda/issues/6434 (filtering out absurd cases
> automatically).
> 
> Is there a way to measure (or just see perhaps via highlighting) how
> much time agda is spending doing that specific work in a particular
> function so I can tell that using this new option might be profitable?

If you use interactive highlighting and notice that there is a delay
between when Agda finishes checking the last clause and starts checking
the following definition, then this could be due to Agda working hard to
figure out that you have not omitted any clauses that should not be
omitted (but it could also be due to other things, like termination or
positivity checking).

If you turn on the new option and your code still type-checks, then
Agda's performance should be more or less unchanged. However, if your
code is rejected and you fix it (by adding absurd clauses), then you
might see a speedup.

-- 
/NAD