Zulip Chat Archive

Stream: general

Topic: tactic debug


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?

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.

Patrick Massot (Jun 01 2018 at 06:54):

Thanks!


Last updated: Dec 20 2023 at 11:08 UTC