Debugging macro expansion

Stream: lean4

[Eric Wieser]

How can I see what a macro has expanded to at its use site? I have a macro with syntax that produces a type error, but I can't work out how to see the syntax. dbg_trace isn't very useful because it can't pretty-print the Syntax object (as the pretty printer can't be called from docs#MacroM)

[Shreyas Srinivas]

set_option pp.macroStack true?

[Eric Wieser]

That seems to expand much further than I was hoping; I want to expand only my current macro

[Eric Wieser]

(also lean4#2878 to fix the documentation for that option)

[Eric Wieser]

Ah, it's a call stack with the least expanded version at the bottom!

[Eric Wieser]

Unfortunately it prints as [Error pretty printing syntax: parenthesize: uncaught backtrack exception. Falling back to raw printer.], so it's still not very helpful; but that's a different problem

[Shreyas Srinivas]

One thing I recall is that if you mess with the syntax enough, Lean suggests a setting to view the fully expanded term.

[Shreyas Srinivas]

That gives you a huge term with a lot of TSyntax cat stuff

[Shreyas Srinivas]

Found it : set_option pp.rawOnError true

[Shreyas Srinivas]

But it also does exactly what your error message says.