Janno (Mar 02 2021 at 15:54): Janno (Mar 02 2021 at 15:54):I am looking for debugging help on a unification issue that pops up 40 minutes into a non-open source proof. Luckily, the problem is pretty easy to explain: I have a goal of the form bi_entails P ?Q and solve it using refine (bi_entails_refl P). Those are iris definitions but you can substitute with eq P ?Q and eq_refl P. After that call to refine, the contents of ?Q are almost P except that a few terms have been changed. In my specific example, P is a huge term that contains the subterm (0 < nb)%N under a few binders (one of which is nb). In ?Q that subterm has been changed to (?GoalX < nb)%N where ?GoalX (X is some number) is a new evar. I am extremely confused by this. The reason I think that this is a unification bug is that Requiring unicoq and using Set Use Unicoq fixes the problem (i.e. ?Q is instantiated exactly with P). My suspicion is that the value 0 in 0 < nb was originally an evar that got instantiated with 0 and somehow that evar got messed up during unification. Does anyone have any ideas about this? I'd love to report this as a bug with a reproducible example.
Michael Soegtrop (Mar 02 2021 at 18:55):This is way obvious but did you try adding prints at a few key points of the unifier and inspect the output? Since you know which terms get messed up, it should be possible to search this in the logs. Also you might be ok to share at least parts of this log. I don't see much of an alternative for debugging code that runs 40 minutes until it gets to the spot.
Is the issue that you don't know what to print where?
Janno (Mar 02 2021 at 21:29):I have debug output before and after refine. I know the exact value of P and I know the exact value(s) of ?Q. I can see the output of Set Debug Unification (which print the correct unification problem for P ~ ?Q). I think I have all the data.. I just don't know why this particular call to refine produces new evars and puts them into the ?Q. I am slowly reproducing the exact circumstances in which refine gets called so that I can find out what parts of the goal are necessary for the bug to trigger.
Janno (Mar 02 2021 at 22:00):I managed to rephrase things in terms of eq. Here's the proof script..
ltac2:(lazy_match! goal with
| [ |- ?p = ?q ] =>
let prf := constr:(@eq_refl _ $p) in
Message.print (Message.of_string "DIFF");
Message.print (Message.of_constr q);
Message.print (Message.of_constr p);
refine prf;
Message.print (Message.of_constr q);
()
end).
.. and the output: (my ?Q, or ?q in the ltac2 code above, is called ?F)
DIFF
?F@{x45:=0%N; p'1:=nullptr}
(my_term 0)
(my_term ?Goal3@{x45:=0; p'1:=nullptr})
And here with Set Printing All to avoid any scope confusion around numeric literals:
DIFF
?F@{x45:=N0; p'1:=nullptr}
(my_term N0)
(my_term ?Goal3@{x45:=N0; p'1:=nullptr})
Okay, this is enough nightmare material for me. I'll go to bed...
Gaëtan Gilbert (Mar 02 2021 at 22:33):there's probably a delayed constraint ?Goal3@{x45:=N0; p'1:=nullptr} == N0 (which can be solved by both Goal3 = N0 and Goal3 = x45)
maybe solve_constraints after the refine helps
Janno (Mar 03 2021 at 11:22):Thanks a lot! solve_contraints does indeed help! Judging by the documentation of Solve Unification Constraints it seems like one of our custom tactic isn't maintaining the no-remaining-constraints invariant. I wonder if makes sense to invest time into figuring out exactly which tactic leaves unsolved constraints or if I should just stick solve_constraints at the end of all our tactics.
Janno (Mar 03 2021 at 11:29):Hm, maybe it is not so clear cut after all. The only place where progress solve_constraints works is right after the call to refine. Is this a bug in refine itself?
Janno (Mar 03 2021 at 11:36):Oh.. this only comes up in Ltac2's refine. So it's not really a unification problem. I suspect Unicoq simply doesn't delay the constraint. But evarconv does delay it and Ltac2 does not honor Solve Unification Constraints. @Pierre-Marie Pédrot is this on purpose?
Gaëtan Gilbert (Mar 03 2021 at 11:43):ltac2 should respect the option, it goes through the same Proof.solve as ltac1 which is where that's handled
Janno (Mar 03 2021 at 11:44):Maybe it's the ltac1/ltac2 boundary that enforces it in this case. I'll write the whole snippet in ltac1 to find out which one out of exact/refine/exact: does the right thing.
Gaëtan Gilbert (Mar 03 2021 at 11:45):note that Solve Unification Constraints basically replaces tac. by tac;solve_constraint. ie it's sentence based
Gaëtan Gilbert (Mar 03 2021 at 11:46):it has nothing to do with atoms like refine/exact/etc
Janno (Mar 03 2021 at 11:46):Ah!
Gaëtan Gilbert (Mar 03 2021 at 11:46):looking at the doc that's not very clear
Janno (Mar 03 2021 at 11:47):But.. hm. That makes the whole thing even more puzzling. I can definitely get these unresolved evars to show up after a sentence.
Janno (Mar 03 2021 at 11:47):(Not in my tiny reproduction of the problem but in the original example.)
Janno (Mar 03 2021 at 11:48):I might have reproduced the wrong thing..
Janno (Mar 03 2021 at 11:59):Or can I? I need to try this again.
Janno (Mar 03 2021 at 12:09):I cannot. I only observed the unresolved constraints by printing after refine. Well, I guess none of this was actually a problem then.
Janno (Mar 03 2021 at 12:47):I just got one step closer to figuring out at a problem that's actually real: Using Ltac2's refine (like in my minimal proof script) I get new a subgoal that corresponds to the already-defined evar. I can solve that subgoal with any value of N I like. For example, refine prf > [refine '99%N] works just fine and it seems 99%N disappears into a black hole. I cannot find any trace of it in any term afterwards. Ltac1's refine doesn't leave such a subgoal. Also, the subgoal disappears at the end of the sentence (probably because the contraints are being solved).
Gaëtan Gilbert (Mar 03 2021 at 12:49):if you unset the option does it still disappear?
Janno (Mar 03 2021 at 12:50):Just tried that and the goal is returned, i.e. it no longer disappears
Janno (Mar 03 2021 at 12:50):And I can get the corresponding(does it correspond?) evar to show up in the other goal.. that's pretty much to be expected, I guess.
Janno (Mar 03 2021 at 12:51):Ha, what's even better is that this apparently loses the constraint and I can now solve the goal with 99%N and the value shows up in the other goal.
Janno (Mar 03 2021 at 12:52):(I imagine that in the other scenario where I solve the goal with 99%N before the end of the sentence the value is ignored because it violates the constraint?)
Janno (Mar 03 2021 at 12:55):I wish I could push this all the way to Qed to see what explodes but I don't have 20+40 minutes for getting there and returning to the current position in the proof :(
Jason Gross (Mar 03 2021 at 13:40):Goal True.
let g := open_constr:((fun x => _) 0 = 0) in
assert g.
Unset Solve Unification Constraints.
refine eq_refl.
exact 1.
constructor.
Qed. (* Error: The term "eq_refl" has type "1 = 1" while it is expected to have type "1 = 0". *)
Is this a bug? What's the spec of unsetting the unification constraints solver?
Jason Gross (Mar 03 2021 at 13:46):I believe it's a bug; I'll report it
Jason Gross (Mar 03 2021 at 13:50):https://github.com/coq/coq/issues/13893
Jason Gross (Mar 03 2021 at 13:51):Note that reflexivity correctly leaves the constraint behind, while refine does not
Janno (Mar 03 2021 at 13:53):Hm, reflexivity uses tactic unification..
Janno (Mar 03 2021 at 13:53):So maybe this is an evarconv bug after all? I don't know what to think anymore :D
Last updated: Oct 13 2024 at 01:02 UTC