<div dir="ltr"><div dir="ltr">Thanks everyone for the replies! I'm still digesting but a few follow-up questions (to two different replies).<br></div><div><br><div class="gmail_quote"><div dir="ltr" class="gmail_attr">On Tue, Sep 26, 2023 at 3:35 AM James Wood <<a href="mailto:james.wood.100@strath.ac.uk">james.wood.100@strath.ac.uk</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">Hi Robby,<br>
<br>
An easy debugging step is to try setting `agda2-highlight-level` to <br>
`interactive`. This makes syntax highlighting happen in real time, which <br>
gives a visual impression of which the slow parts are.<br>
</blockquote><div><br></div><div>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). <br></div><div><br></div><div>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?<br></div></div></div><div><br></div><div class="gmail_quote"><div dir="ltr" class="gmail_attr">On Tue, Sep 26, 2023 at 9:37 AM Nils Anders Danielsson <<a href="mailto:nad@cse.gu.se">nad@cse.gu.se</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">On 2023-09-25 16:21, Robby Findler wrote:<br>
> I'm still on 2.6.3, if that matters. I see that there is a performance<br>
> related change in 2.6.4: is there a way to get some hints about which<br>
> functions might benefit from that treatment?<br>
<br>
I assume that you refer to the new keyword "opaque".<br>
<br></blockquote><div><br></div><div>Ah, sorry. I was asking about this change: <a href="https://github.com/agda/agda/issues/6434">https://github.com/agda/agda/issues/6434</a> (filtering out absurd cases automatically).<br></div><div><br></div><div>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?</div><div><br></div><div>Thanks again!<br></div><div><br></div><div>Robby</div><div><br></div></div></div>