[Agda] performance debugging?

[Robby Findler]

Thanks everyone for the replies! I'm still digesting but a few follow-up
questions (to two different replies).

On Tue, Sep 26, 2023 at 3:35 AM James Wood <james.wood.100 at strath.ac.uk>
wrote:

> Hi Robby,
>
> An easy debugging step is to try setting `agda2-highlight-level` to
> `interactive`. This makes syntax highlighting happen in real time, which
> gives a visual impression of which the slow parts are.
>

This is great and has been very helpful to me already (I could see that a
function that didn't matter to what I was working on was slow so I just
commented it out and got a huge ux improvement while working in the file).

It looks like this highlighting will first highlight the entire function
and then later highlight each clause in the function -- is that right? Is
there an explanation of what it is doing in these different phases that
might help me understand how to do something differently?

On Tue, Sep 26, 2023 at 9:37 AM Nils Anders Danielsson <nad at cse.gu.se>
wrote:

> On 2023-09-25 16:21, Robby Findler wrote:
> > I'm still on 2.6.3, if that matters. I see that there is a performance
> > related change in 2.6.4: is there a way to get some hints about which
> > functions might benefit from that treatment?
>
> I assume that you refer to the new keyword "opaque".
>
>
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?

Thanks again!

Robby
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20230927/bff4ca1b/attachment.html>