[Agda] performance debugging?

[Robby Findler]

On Fri, Apr 26, 2024 at 4:05 AM Nils Anders Danielsson <nad at cse.gu.se>
wrote:

> I've recently optimised
> code with similar characteristics. Perhaps you can do something similar:
>
> * Prove suitable inversion lemmas for one of the two types.
>
> * Instead of matching on both arguments, match on one, and use inversion
>   lemmas for the other argument.
>
>
Wow! That made a huge difference, thank you! That technique took me from
7.5 minutes down to 12 seconds (plus another 2 seconds to check the file
with all the inversion lemmas)! That's more than a 35x speed up. Amazing!

Also it turns out, I didn't have 2 connected arguments, it was actually 3.
(One is an evaluation context and the other two are proofs of
decompositions, so the case split on the two decompositions was replaced by
the inversion lemmas.)  And now that I get the idea, I'm seeing
opportunities for this in more places, in this codebase too (not that
anything was that slow)!

Thanks again!

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