Zulip Chat Archive

Stream: general

Topic: tactic debug

view this post on Zulip Patrick Massot (May 31 2018 at 20:44):

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?

view this post on Zulip Gabriel Ebner (Jun 01 2018 at 06:48):

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.

view this post on Zulip Patrick Massot (Jun 01 2018 at 06:54):


Last updated: May 13 2021 at 05:21 UTC