Performance Puzzles · Coq devs & plugin devs

@Pierre-Marie Pédrot I have a new performance puzzle for you. (The question is roughly: "what performance-relevant side-effects of tactics are reset by Undo but not by backtracking in the tactic monad?") https://github.com/coq/coq/issues/12299

Jason Gross (Aug 06 2022 at 05:10):

In a goal of the form x = v :> T, where x is an evar and v is evar-free (though it may reference context variables whose bodies contain evars), can someone (@Pierre-Marie Pédrot ?) explain why the following performance profile to me?

Time to run tactic 10 times: tactic
4.434 secs : instantiate (1:=v); reflexivity
5.054 secs : instantiate (1:=v); refine eq_refl
4.337 secs : instantiate (1:=v); refine (@eq_refl T v)
17.516 secs : unify x v; reflexivity
29.855 secs : unify x v; refine eq_refl
17.032 secs : unify x v; refine (@eq_refl T v)
17.112 secs : unify v x; reflexivity
30.830 secs : unify v x; refine eq_refl
19.057 secs : unify v x; refine (@eq_refl T v)

In particular, why is instantiate so much faster than unify, and why does unify result in so much more overhead from the implicits of eq_refl in refine? (Possibly important to note: the size of the context is around 300 variables, some of which are assigned to evars which themselves may contain (recursively?) large instances)

Pierre-Marie Pédrot (Aug 06 2022 at 09:33):

I didn't profile the code, but an educated guess is that unify uses the old unification algorithm, which does very weird things with evars (read: is unsound) and in particular has an half-baked evar substitution process that is known to be a source of slowness (the informal subst_defined_metas_evars function).

Pierre-Marie Pédrot (Aug 06 2022 at 10:20):

Actually, no. Profiling shows that time is spent in evarconv, not in unification. The exact unification algorithm probably produces a slightly different term that makes evarconv take another path.

Pierre-Marie Pédrot (Aug 06 2022 at 10:21):

That said, we're hitting here the usual aliasing hotspot of evarconv. I think somebody should have been done about this algorithmic borehole a long time ago but I don't even understand what this is doing.

Jason Gross (Aug 06 2022 at 17:10):

I think the thing that's going on here is that when you have x := z in the context of your unification problem, if x is valid in the context of your evar then you should use x, but if x is not in the context of your evar but z is, then you should use z wherever x shows up rather than failing. (I guess if z is itself an evar with a large substitution you will want to cache the judgment of whether or not z is valid in the context of the evar / what its replacement should be.)

Jason Gross (Aug 06 2022 at 17:14):

(This came up when preparing my "10 Years of Superlinear Slowness in Coq" talk for the Coq Workshop)

Stream: Coq devs & plugin devs