Zulip Chat Archive

Stream: general

Topic: Basic tools for tracing/debugging tactics in Lean 3?

Thomas Murrills (Oct 18 2022 at 19:39):

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 (Oct 18 2022 at 20:11):

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

Alex J. Best (Oct 18 2022 at 20:12):

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 (Oct 18 2022 at 20:13):

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

Last updated: Dec 20 2023 at 11:08 UTC