Debuggin Evaluation

Stream: lean4

[Yicheng Qian]

How can I debug evaluation in Lean4? To be specific, after I defined a function f, I executed #eval (f arg) and the result res is incorrect. To find out what's wrong, I wanted to follow the evaluation of f arg step-by-step. How to do that?

I tried this: First, I declared a theorem f arg = res and entered tactic mode

theorem foo : f arg = res := by

Then, I used the tactic rw to reduce f arg step-by-step. However, the reduction often stucks, for example at expressions like <typeclass-object>.<field-notation>. What can I do?

[Henrik Böving]

The simple answer right now is: You do not do that. You do not follow execution step by step, what you can do though is add little fragments of dbg_trace s!"Fooo {myvar}" into even pure code to see what is going on.

[Yicheng Qian]

Can you further explain how to use the "dbg_trace" command? I'm new to lean and don't know how to use it.

[Yicheng Qian]

Is there any documentation which explains it?

[Henrik Böving]

def foo (x : Nat) :=
  dbg_trace s!"{x}"
  Nat.add x 12

[Henrik Böving]

Yicheng Qian said:

Is there any documentation which explains it?

Not to my knowledge

[Sebastian Ullrich]

https://leanprover.github.io/lean4/doc/dev/debugging.html, additions are welcome

[Yicheng Qian]

Thanks. This is very helpful.