Were there any changes to unification order in 8.12? We are trying to upgrade from 8.11.2 to 8.12.1 and I am seeing changes to the order of unification in basically any tactic (apply
, refine
, apply:
, typeclasses eauto
, ..) that leads to practically diverging unification attempts on problems in the form of f x1 x2 =?= f y1 y2
where x1
and y1
are obviously not unifiable. 8.11.2 tried to unify them first and thus failed quickly. 8.12.1 however attempts to unify x2
and y2
which in some of our goals contain numeric functions that take forever (at least an hour, probably much more) to reduce.
No such change is documented in the changelog (and it clearly should have been) so you did well to open https://github.com/coq/coq/issues/13419.
I still don't actually know if anything changed about the order of unification/conversion. I think I need to patch Coq to get a trace of everything being unified.
If we believe your bisect, it is more a consequence of a change in the stdlib.
But that's basically separate from what I though the problem to be initially. As far as I can tell from unicoq traces (which may or may not have any bearing on what happens in evarconv) I can tell that on 8.11 I don't even get to the point of trying to unify the terms whose fixpoint status has changed.
OK, so maybe there are several changes and your bisect didn't point you to the most relevant one because of your minimized example...
Exactly!
There are no evars so we shortcut out of unification to the kernel and there are no traces
But I do get (unicoq) traces on 8.11.
In fact you can take 8.11, see that it's fast, change just eqb
to Definition in BinIntDef, see that it's slow
Maybe unicoq doesn't go to the kernel or traces differently, I don't know
perf
profile shows it's going through Reduction.cmp_rec
and various other other functions that smell like convertibility. And the fact that unicoq on 8.12 also hangs seems a pretty good indicator that it ends up in the same code path as everaconv.
Last updated: Dec 01 2023 at 07:01 UTC