tracing unification?

Stream: lean4

[Jason Gross]

Is there a tracing option for debugging the unifier?

[Leonardo de Moura]

set_option trace.Meta.isDefEq true -- for expressions
set_option trace.Meta.isLevelDefEq true -- for universe levels

It is currently a "tsunami" of trace messages.
Recall that we can now use set_option in subterms and tactics, and it helps to filter the number of messages.
Example:

def f (a : Nat) : a + 2 = a.succ.succ ∧ a + 3 = a.succ.succ.succ :=
  ⟨rfl, set_option trace.Meta.isDefEq true in rfl⟩

We are planning to provide a simple API for filtering/query the trace messages. @Jason Gross I am curious if you have suggestions.

[Jason Gross]

Hmm, I don't have any suggestions yet, I think I need more experience first. I guess the thing I actually want is some sort of point-and-click or debugger-like experience, where I can click on some part of an error message. For example, in https://github.com/leanprover/lean4/issues/352 , the experience I would have liked to have had is that, on getting "failed to synthesize instance", I could click somewhere on it and get the instance trace (perhaps folded, or something, for easier navigation), and then when I see

      [Meta.synthInstance.tryResolve] CoeSort.{max (u1 + 2) (u2 + 2), u + 2} Cat1.{u1, u2}
        ?m.492 =?= CoeSort.{max (?u.494 + 2) (?u.495 + 2), ?u.494 + 2} Cat1.{?u.494, ?u.495} (Type ?u.494)
      [Meta.synthInstance.tryResolve] failure

I could click on the =?= problem and get a unification trace for this problem/failure.

Alas, this is not a "simple API" :-P

(Tangentially, I think a view I'm coming to hold is that if something in lean fails only due to universes not matching, that's a cause for concern. I kind-of want a version of error-message-reporting where universe issues are propagated more.)