Debugging tactic errors

Stream: metaprogramming / tactics

[Eric Wieser]

In the build for #8211, finish is giving me the error unknown local constant: 0._fresh.59.36963.

Is there some way to get lean to tell me where this error is originating from, and show some kind of stack trace?

[Eric Wieser]

Inserting trace statements is pretty annoying as then I have to wait for all the other files using the tactic to rebuild

[Gabriel Ebner]

You can add the --old command-line option to the server, then you don't need to wait for the rebuild.

[Eric Wieser]

I take it then that sprinkling trace calls is the best approach available to me?

[Gabriel Ebner]

You can also sprinkle show_term calls. :smile:

[Eric Wieser]

In the meta code?

[Eric Wieser]

Ok, it looks like the error originates from docs#smt_state.mk, which lives in C++ land

[Eric Wieser]

Which I guess is here:
https://github.com/leanprover-community/lean/blob/65ad4ffdb3abac75be748554e3cbe990fb1c6500/src/library/tactic/smt/smt_state.cpp#L500-L504