panics in runtime

Stream: lean4

[Arthur Paulino]

Is there a way to make the panic messages show up when LEAN_ABORT_ON_PANIC=1?

[Arthur Paulino]

Hi, since nobody answered the question above, I'm gonna assume the answer is "no" so I can ask the following:
Are there plans to make the (reasonable) behavior below possible?

fn main() {
    panic!("Panic!");
}

λ cargo run
thread 'main' panicked at src/main.rs:2:5:
Panic!

That is, it shows the panic source location and the panic message

[Henrik Böving]

That's at least technically possible yes.

[Jz Pan]

Matt Diamond said:

but rather they want a partial notation on any function which may potentially panic at runtime

But that's impossible since every function may potentially panic due to out of memory or stack overflow

[Notification Bot]

Arthur Paulino has marked this topic as unresolved.

[Arthur Paulino]

Henrik Böving said:

That's at least technically possible yes.

What's possible? To show the panic message with the current Lean release? Or to implement the behavior Rust offers?

[Arthur Paulino]

Let me be specific about my current pain point: debugging is hard. My only options, as far as I understand, are to let panics return default instances or to make the program abort abruptly, without telling me where or why it aborted.

[Henrik Böving]

Arthur Paulino said:

Henrik Böving said:

That's at least technically possible yes.

What's possible? To show the panic message with the current Lean release? Or to implement the behavior Rust offers?

Implementing the behavior.

Arthur Paulino said:

Let me be specific about my current pain point: debugging is hard. My only options, as far as I understand, are to let panics return default instances or to make the program abort abruptly, without telling me where or why it aborted.

If you crash on a panic you should get a stacktrace and a coredump (at least on linux) that you can load into GDB and debug to your heart's content

[Arthur Paulino]

Would it make sense to set abortOnPanic := true in the lakefile configuration for the executable?

[Kyle Miller]

Arthur Paulino said:

or to make the program abort abruptly, without telling me where or why it aborted.

I'm a little confused about this — I have had the experience of aborts and seeing the exact source position of the error, though I haven't tested this recently.

Reading the source code, if you do panic! then you should see an error message and source position if lean_set_panic_messages(true) (which should be true except during module initialization) and also if LEAN_ABORT_ON_PANIC=1.

[Arthur Paulino]

panic! indeed does that. But mean panics like #[0].get! 1