[Agda] performance debugging?

[Robby Findler]

Hi all-- This morning I was working on a lemma that really seems like it is
taking longer than it should. I tried all the approaches that various folks
sent me in this thread (lossy-unification, no-infer-absurd-clauses, opaque
declarations -- thank you!) but, alas, was not able to get any
improvements. (I'm not sure that I made the right definitions opaque,
tho!).

The lemma takes in two related arguments and, instead of being O(n^2) cases
in the constructors, it is O(n) because of the relationship. Each time I
load this lemma, it takes 7.5 minutes (using "time agda file.agda" on a
file containing only this lemma whose imports are all already checked).
After the initial case split, it was taking maybe 2-3 minutes to load the
file (with each rhs just being a hole), in case that seems important. A
different lemma that I was working on yesterday takes similar arguments
except there is only one (not two) of these one arguments and I can work on
that one at basically interactive speeds (just some seconds to load that
lemma). According to the Emacs mode, the thing that takes most of the time
is when the entire function is highlighted (not the individual cases,
although those aren't speedy either).

Assuming this description doesn't spark any ideas that others might have
that I could try, I was wondering if anyone more versed in agda performance
might be willing to have a look? I've trimmed down the development to just
the file that has the overly slow lemma and its dependencies (it also
depends on the iowa agda library, not the standard lib that comes with agda
which I've not yet learned...). It is still pretty big, I'm sorry to say,
at nearly 1800 lines (not counting what it uses in ial), but the file with
the bad lemma is 118 lines. I don't think I'm doing anything particularly
sophisticated in this code. (I'm no agda guru! :).

tia, Robby
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20240425/8e183a41/attachment.html>