@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
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)
Code at https://github.com/mit-plv/bedrock2/releases/tag/2022-08-CoqWorkshop-011-LtacProf, build with make bedrock2_noex; coqc -q -Q bedrock2/src/bedrock2 bedrock2 -Q bedrock2/src/bedrock2Examples bedrock2Examples -Q deps/coqutil/src/coqutil coqutil bedrock2/src/bedrock2Examples/chacha20.v
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).
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.
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.
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.)
(This came up when preparing my "10 Years of Superlinear Slowness in Coq" talk for the Coq Workshop)
Last updated: Sep 25 2023 at 12:01 UTC