Trace while compilation vs goal view

Stream: lean4

[Tomas Skrivan]

There seems to be difference in traces in goal view and while compiling.

If an instance is not found, in the goal view I get trace:

[Meta.Tactic.simp.discharge] differential_of_linear, failed to synthesize instance
  IsLin ?f

On the other hand, during compilation I get:

[Meta.Tactic.simp.discharge] differential_of_linear, failed to synthesize instance
  IsLin (swap (comp • swap comp) (HMul.hMul • NDVector.getOp x✝))

i.e. it tells me for which ?f it failed to find an instance. That is vastly more useful and I would like to have that in the goal view too.

[Gabriel Ebner]

Which editor are you in? Can you please post a #mwe?

[Tomas Skrivan]

I'm using Emacs and I will try to create mwe. Now, I realize that my lean-mode might not by in sync with lean version.

[Gabriel Ebner]

Ah, so no widgets yet.. This would have been my first guess.

[Tomas Skrivan]

Here is mwe:

class IsIdentity {α} (f : α → α) : Prop where
   (proof : f = id)

@[simp] def identity_reduce (f : α → α) (a : α) [IsIdentity f] : f a = a := by rw[@IsIdentity.proof _ f _]; simp; done

def simp_succ (foo : α → α) (a : α) [IsIdentity foo] : foo a = a := by simp; done

set_option trace.Meta.Tactic.simp.discharge true
def simp_fail (foo : α → α) (a : α) : foo a = a := by simp; done

*Lean Goal* in emacs shows:

Messages above (2)
9:60:
unsolved goals
α : Sort ?u.210
foo : α → α
a : α
⊢ foo a = a
9:54:
[Meta.Tactic.simp.discharge] identity_reduce, failed to synthesize instance
  IsIdentity ?f

From command line lean simp_trace.lean produces:

simp_trace.lean:9:60: error: unsolved goals
α : Sort ?u.210
foo : α → α
a : α
⊢ foo a = a
[Meta.Tactic.simp.discharge] identity_reduce, failed to synthesize instance
  IsIdentity foo

[Tomas Skrivan]

(deleted)

[Tomas Skrivan]

So it is IsIdentity ?f vs IsIdentity foo, the later way more useful.

[Tomas Skrivan]

And my lean and lean4-mode should be in sync now.

[Gabriel Ebner]

I get the same output with widgets. My guess is that there is just an instantiateMVars missing somewhere in the interactive trace formatting code. @Wojciech Nawrocki

[Wojciech Nawrocki]

Should be fixed in leanprover/lean4#730.