[Agda] performance debugging?

[mechvel at scico.botik.ru]

On 2023-09-25 17:21, Robby Findler wrote:
> 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?
> [..]


My experience is as follows.

1) For example:
skipping a type expression may lead to expensive type check.
If the type checker hungs long at the same module of your program, then 
do type
checking in the dialogue under the emacs editor, and see in colors the 
place where it
hungs. Set explicitly the type of each item around this place.
Sometimes it helps. Then, find the value which type declaration is 
crucial for
type-cheching of this module.

2) Sometimes replacing the construct of `with' with the function 
case_of_ saves the type checking expense greatly.

3) Even pseudo-generalization may reduce the type check cost.
For example, the lemma
x*yz+uz≈f*z : ∀ x y z u yz uz f → yz ≈ y * z → uz ≈ u * z → f ≈ x * y + 
u →
               x * yz + uz ≈ f * z

is proved in a simple way in a module M.
And it is applied only once in the program, so that its proof is set 
strictly in-place.

Then, I discovered that people call “generalization” the tricks like 
moving the code part like of the above x*yz+uz≈f*z to a separate 
function, may be even in a separate module.

Strangely, after I moved this implementation making it a separate lemma 
in another module,
type checking of M became many times faster.

--
SM