[Agda] performance debugging?

[James Wood]

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.

Regards,
James

On 25/09/2023 15:21, Robby Findler wrote:
> CAUTION: This email originated outside the University. Check before 
> clicking links or attachments.
> Hi all-- I'm having some performance trouble with an agda development 
> I'm working on. I made a change to some low-level data structure and am 
> now working my way through the rest of the code doing the required 
> updates. Some of the updates require me to add a new argument alongside 
> an existing one and as I'm working through the cases in a lemma, doing 
> that, I'm at the point in a 200 line file where it takes about 12 
> minutes for agda to check it. There seemed to be a large jump after I 
> repaired one of the cases (from a bit less than a minute to about 5 
> minutes; this was when I was in the stage of getting errors instead of 
> having holes to fill in).
> 
> Anyway, all that is context to ask if there is any advice on things I 
> might do to try to get back to more interactive speeds. I tried filling 
> (nearly) all of the implicit parameters in the case that had the large 
> jump, but that didn't seem to help (although filling in implicit 
> arguments explicitly has seemed to help in other situations). Are there 
> other things one might try?
> 
> 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?
> 
> Thanks in advance!
> 
> Best,
> Robby
> 
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda