Debugging errors in generated syntax

Stream: lean4

[Alex Keizer]

I am writing an elaborator that generates a bunch of syntax and feeds it to elabCommand.
I do trace all generated syntax. Nonetheless, whenever I inevitably mess something up, it is very hard to relate the error in my infoview to which piece of syntax actually causes that error.

I tried to wrap elabCommand in a try ... catch, but it seems the errors aren't actually bubbled up; they're just logged. Does anybody have some tips for how to debug metaprograms? I saw some mention of hooking up gdb to lean. Is there an easy way to do that inside vscode, allowing me to set breakpoints in my Lean code, or am I doomed to finally learn to work with gdb's CLI?

[Mario Carneiro]

The better approach is to either use %$tk on tokens of your syntax to copy the positions to generated tokens (for a macro-like command) or to use withRef tk when calling elaborator functions (for an elab-like command) so that error messages that are reported end up on the correct spans.

[Mario Carneiro]

Although, the second paragraph seems to be going in a completely different direction here, it sounds like you don't just want to relate the error messages to syntax but to actually debug the program in GDB or something

[Alex Keizer]

Sure, that works if there is an issue with the input syntax (and I do do that). My elaborator is quite complex, though, I meant when I make mistakes in my metaprogram and the syntax I generate is wrong.

[Mario Carneiro]

Most of the time when I want to debug metaprograms I use println! or trace[Meta.debug], depending on the context

[Alex Keizer]

My problem is that there are actually a few different places in my code (the elaborator is more than 500 SLOC), so it is difficult to figure out exactly which one is wrong.

[Mario Carneiro]

I would use targeted trace messages for that

[Mario Carneiro]

just put different print lines before each of the lines that could possibly go wrong and see what the last thing that is printed is

[Alex Keizer]

Right, except that elabCommand just logs error, ignores them and chugs right through to the rest (that's presumably also why try ... catching doesn't work). So all syntax is traced, and I'm left with an info log that says unknown identifier 'α'. It would be nice to immediately see which invocation of elabCommand caused that error

[Alex Keizer]

Aha, but if I run the build on the command line, then I can see in-between which traces the error is logged! It's only when running from inside vscode when this information is lost (because errors are shown separately from traces). Thanks for pointing me in the right direction!

[Mario Carneiro]

Alex Keizer said:

Right, except that elabCommand just logs error, ignores them and chugs right through to the rest (that's presumably also why try ... catching doesn't work). So all syntax is traced, and I'm left with an info log that says unknown identifier 'α'. It would be nice to immediately see which invocation of elabCommand caused that error

The trace messages will be preserved even if the elabCommand causes an error

[Alex Keizer]

Exactly, there doesn't seem to be a difference in the trace messages when elabCommand causes an error and when it doesn't.