tactic debug

Stream: general

[Patrick Massot]

Is there anything like a Lean debugger which would allow me to execute tactics line by line and inspect the values of variables? Or should I add trace commands after every lines in Simon's tactics to hope to understand how they work?

[Gabriel Ebner]

There is a debugger, but I don't think anybody here uses it (or even knows how to use it). You need to run it from the command-line. Example: https://github.com/leanprover/presentations/blob/master/20170116_POPL/debug/has_to_string_break.lean I'd stick to trace messages.

[Patrick Massot]

Thanks!