backtrace for panic!

Stream: lean4

[Henrik Böving]

I've noticed during my development on doc-gen4 that when I commit some logic error in my handling of e.g. HashMapand try to access a key that is not there nailing even the location of the error down (especially when the HashMap is not in the spot I just edited but somewhere else and this error is a side effect of the change I made) is kind of hard due to the fact that panic! only knows about the location it was called it but not actually the entire backtrace. With my current knowledge of Lean I can also see that it's very convenient to have panic work this way because you can just determine this location easily at compile time but I was wondering whether it would be feasible to actually print a full backtrace? This would make my life soooo much easier when I eventually mess up again.

[Gabriel Ebner]

You can always run the program in a debugger and set a breakpoint on lean_panic_fn.

[Gabriel Ebner]

You could also try setting the environment variable LEAN_ABORT_ON_PANIC (on the official nightlies). I believe libc++ produces backtraces for uncaught exceptions.

[Mario Carneiro]

I don't think lean has any support for language level backtraces. It would definitely be nice

[Mario Carneiro]

it's pretty painful to get a backtrace in haskell, it's opt in with a magic typeclass. Not sure if lean would suffer similar issues

[Mario Carneiro]

Probably a better strategy is just to use the C stack and demangle the names

[Gabriel Ebner]

I think the big issue in Haskell is laziness, the actual stack trace at the time of execution has little relation to nested calls in the source. In Lean we could indeed look at the C stack (and the interpreter!).

[Mario Carneiro]

In the interpreter, I guess it's possible to directly produce the backtrace

[Gabriel Ebner]

Typically the interpreter is interleaved with native functions, so ideally you'd want both.

[Henrik Böving]

Yeah I kind of expected it's non trivial to acutally do it in lean :/ the Rust backtrace/unwind machinery (its the only other I know) is also kinda complex.

[Mario Carneiro]

I think rust is just wrapping libunwind

[Henrik Böving]

But the debugger is a good idea, I'll try that in the future!

[Mario Carneiro]

which I guess we could do too

[Henrik Böving]

Yeah they do but there is also some degrees of platform specific logic, for example under OpenBSD libunwind does work but for the longest time it would just print "unknown function" n times (for stack depth n) until I fixed it in the unwind wrapper so there is apparently some non trivial piece of platform specific code involved at least in Rust.

[Henrik Böving]

maybe Lean doesnt suffer from this since we are just C code

[Gabriel Ebner]

I wonder if it is possible to integrate the VM stack with libunwind.

[Gabriel Ebner]

Apparently the state of the art is to capture both the native stack as well as the interpreter stack(s) and then merge them. https://www.benfrederickson.com/profiling-native-python-extensions-with-py-spy/

[Locria Cyber]

Henrik Böving said:

But the debugger is a good idea, I'll try that in the future!

Use libunwind and add debug information (DWARF) when compiling. This can be done with #line macro in C.

[Locria Cyber]

Make sure to emit row+column