Panic backtraces with line numbers?

Stream: general

[Jason Reed]

When running lean code (on linux, if that matters) with a panic, with buildType := BuildType.debug in my lakefile.lean (which I speculatively added without being certain that was necessary) I notice that a panic produces an error message with a nicely formatted lean symbol and a line number, e.g.

PANIC at Verso.Genre.Manual.instGenreTeXReaderTExtensionImplsIO VersoManual.Basic:1205:8: Inline Verso.Genre.Manual.Inline.margin doesn't support TeX

but the remainder of the backtrace is internally-generated symbols presumably at the C++ level, e.g.

/lean-code/verso/.lake/build/bin/demotextbook(l_Array_mapMUnsafe_map___at___Verso_Doc_Inline_toTeX___at___Verso_Doc_Block_toTeX___at___Verso_Genre_Manual_emitTeX_spec__0_spec__0_spec__0+0xc9) [0x56fbf43e5bc9]
/lean-code/verso/.lake/build/bin/demotextbook(l_Verso_Doc_Block_toTeX___at___Verso_Genre_Manual_emitTeX_spec__0+0x774) [0x56fbf43e8e24]
/lean-code/verso/.lake/build/bin/demotextbook(l_Array_mapMUnsafe_map___at___Verso_Doc_Part_toTeX___at___Verso_Genre_Manual_emitTeX_spec__9_spec__12+0x107) [0x56fbf43ed207]
/lean-code/verso/.lake/build/bin/demotextbook(l_Verso_Doc_Part_toTeX___at___Verso_Genr

My question is: does there exist a way to get the symbols unmangled back to Lean line numbers? If not, no problem, I'll be content to know that I can stop looking for how to get it :slight_smile:

[Jason Reed]

(In this case the mangled symbols are still a nontrivial help in understanding the trace)

[Henrik Böving]

No that is currently not possible

[Jason Reed]

Thanks, good to know!