[Agda] performance debugging?

Robby Findler robby at racket-lang.org
Mon Sep 25 16:21:20 CEST 2023


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
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20230925/abb3ec59/attachment.html>


More information about the Agda mailing list