Basic tools for tracing/debugging tactics in Lean 3?

Stream: general

[Thomas Murrills]

Specifically, I'm looking for tools to help understand how existing tactic/meta def-type Lean 3 code works—even being able to stick a kind of "print" statement in the middle of a do block would be useful. (I'm just starting, really, so even extremely basic techniques are welcome!)

Pointing me to a resource that already talks about this would also be greatly appreciated; I couldn't find it in the Lean 3 manual :)

(Maybe this should be moved to #metaprogramming / tactics ? Not sure.)

[Alex J. Best]

docs#tactic.trace is the basic print command (and that's like 90% of debugging of course!)

[Alex J. Best]

One can also insert docs#trace_val even into non-meta defs and the VM will trace the value as it executes

[Alex J. Best]

There are other more advanced functions in the same file for tracing the stack etc