Efficient dev flow for parser work

Stream: lean4 dev

[Dax Fohl]

I've been trying to explore issue https://github.com/leanprover/lean4/issues/7135, "Keep goal view active on unparsed input". I think I've kind of got a grasp on how the code is organized; I'm pretty sure the issue is somewhere in src/Lean/Parser, or maybe src/Lean/Language, or one of the core files in src/Lean/Elab. (When I started, I assumed all the core stuff like this would be in C++, so I've at least made that amount of progress).

The main thing I'm struggling with now is finding a decent dev cycle. Currently my dev cycle is something like "add a dbg_trace to src/Lean/Parser/Basic.lean, run make -C build/release -j$(nproc || sysctl -n hw.logicalcpu), wait a few minutes, go to my test project in vscode, click 'Restart File' in the info view, and look at the Output tab to see what got logged." That's compounded by the fact that many of the things I'd want to log, like cmdState.messages don't have a ToString, so figuring out how to log them either takes a long time, or I just give up.

I also tried logInfo, but that's even harder because it can only be used in certain places.

I also saw https://github.com/leanprover/lean4/blob/12536d2015eea27c7bad4dd47fdc6150c0f3ebb6/doc/dev/debugging.md talked about traces, but I haven't figured that out. If I set set_option trace.Elab.command true in src/Lean/Language/Lean.lean and rebuild, I see it emits a lot of info during build, but when I go to my test project in vscode and click Reload File, it doesn't seem to have an effect on the output tab. Also if I go back to src/Lean/Language/Lean.lean and try to add trace[Elab.command] "hello" somewhere, it tells me failed to synthesize Lean.MonadTrace Lean.Language.Lean.LeanProcessingM, so I'm generally stuck trying to figure out when and how to use the trace functionality.

Does anyone have guidance for what a productive dev flow should look like in lean parser etc code? I mean, ideally it'd be great if the debugging docs had a screen recording of what a proper dev flow would look like (should I file that as a github issue?), as I'm sure it would be useful for other new joiners. But I'll take whatever I can get.

[Dax Fohl]

(Tangent, on #7135 itself, I just saw there's also a src/Lean/Server folder for the LSP code. Is the problem in #7135 actually in the parser itself, or could it just be in the LSP?)

[Dax Fohl]

(Also I fixed some broken links in the markdown dev docs in https://github.com/leanprover/lean4/pull/8785, if anyone has time to look.)