Janno (Nov 19 2020 at 11:40): Janno (Nov 19 2020 at 11:40):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.
Théo Zimmermann (Nov 19 2020 at 16:22):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.
Janno (Nov 20 2020 at 09:53):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.
Théo Zimmermann (Nov 20 2020 at 09:56):If we believe your bisect, it is more a consequence of a change in the stdlib.
Janno (Nov 20 2020 at 09:58):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.
Théo Zimmermann (Nov 20 2020 at 10:00):OK, so maybe there are several changes and your bisect didn't point you to the most relevant one because of your minimized example...
Janno (Nov 20 2020 at 10:02):Exactly!
Gaëtan Gilbert (Nov 20 2020 at 11:00):There are no evars so we shortcut out of unification to the kernel and there are no traces
Janno (Nov 20 2020 at 11:05):But I do get (unicoq) traces on 8.11.
Gaëtan Gilbert (Nov 20 2020 at 11:05):In fact you can take 8.11, see that it's fast, change just eqb to Definition in BinIntDef, see that it's slow
Gaëtan Gilbert (Nov 20 2020 at 11:06):Maybe unicoq doesn't go to the kernel or traces differently, I don't know
Janno (Nov 20 2020 at 11:17):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