Debugging `panic`?

Stream: new members

[Youngju Song]

I was abusing get! and ended up with several panics. It would be good to have a fancy debugger, but just knowing (1) where the panic happened, (2) call stack, and (3) the local environment (values) at the time panic has happened would be sufficient for me. Is there a way to get these informations?

For (1), #eval ((none: Option Nat).get!) currently prints the position of the "definition" of get! (i.e., Init.Data.Option.BasicAux:16:14), not the callsite. I have been using my own macro that behaves like get! but prints the callsite in case of none - but it feels like there should be better and more official way to do this.

[Henrik Böving]

Run your program with export LEAN_ABORT_ON_PANIC=1, then you'll get the option to dump a stacktrace etc

[Youngju Song]

@Henrik Böving Thank you! Can you elaborate on how to dump a stacktrace?
I have set LEAN_ABORT_ON_PANIC, built again with lake build, and ran binary in .lake/build/bin/, but the output seems unchanged.

[Henrik Böving]

It should just work

λ cat foo.lean
def main : IO Unit := do
  panic! "ahhh"
florence:~|
λ lean --run foo.lean
PANIC at main foo:2:2: ahhh
backtrace:
/home/nix/.elan/toolchains/leanprover--lean4---v4.12.0-rc1/bin/../lib/lean/libleanshared.so(lean_panic_fn+0x6d) [0x7ff0db9c9e6d]
/home/nix/.elan/toolchains/leanprover--lean4---v4.12.0-rc1/bin/../lib/lean/libleanshared.so(+0x4dbbd84) [0x7ff0db9bbd84]
/home/nix/.elan/toolchains/leanprover--lean4---v4.12.0-rc1/bin/../lib/lean/libleanshared.so(+0x4db9fe0) [0x7ff0db9b9fe0]
/home/nix/.elan/toolchains/leanprover--lean4---v4.12.0-rc1/bin/../lib/lean/libleanshared.so(+0x4dbc0c2) [0x7ff0db9bc0c2]
/home/nix/.elan/toolchains/leanprover--lean4---v4.12.0-rc1/bin/../lib/lean/libleanshared.so(+0x4db9fe0) [0x7ff0db9b9fe0]
/home/nix/.elan/toolchains/leanprover--lean4---v4.12.0-rc1/bin/../lib/lean/libleanshared.so(+0x4dbdc03) [0x7ff0db9bdc03]
/home/nix/.elan/toolchains/leanprover--lean4---v4.12.0-rc1/bin/../lib/lean/libleanshared.so(+0x4dbd887) [0x7ff0db9bd887]
/home/nix/.elan/toolchains/leanprover--lean4---v4.12.0-rc1/bin/../lib/lean/libleanshared.so(+0x4dbd42f) [0x7ff0db9bd42f]
/home/nix/.elan/toolchains/leanprover--lean4---v4.12.0-rc1/bin/../lib/lean/libleanshared.so(lean_apply_1+0x175) [0x7ff0db9d4eb5]
/home/nix/.elan/toolchains/leanprover--lean4---v4.12.0-rc1/bin/../lib/lean/libleanshared.so(+0x4db740a) [0x7ff0db9b740a]
/home/nix/.elan/toolchains/leanprover--lean4---v4.12.0-rc1/bin/../lib/lean/libleanshared.so(+0x4dbe0a9) [0x7ff0db9be0a9]
/home/nix/.elan/toolchains/leanprover--lean4---v4.12.0-rc1/bin/../lib/lean/libleanshared.so(+0x4db6b91) [0x7ff0db9b6b91]
/home/nix/.elan/toolchains/leanprover--lean4---v4.12.0-rc1/bin/../lib/lean/libleanshared.so(_ZN4lean2ir8run_mainERKNS_11environmentERKNS_7optionsEiPPc+0x87) [0x7ff0db9b5fc7]
/home/nix/.elan/toolchains/leanprover--lean4---v4.12.0-rc1/bin/../lib/lean/libleanshared.so(lean_main+0x274b) [0x7ff0d7a40d1b]
/lib64/libc.so.6(+0x3248) [0x7ff0d6906248]
/lib64/libc.so.6(__libc_start_main+0x8b) [0x7ff0d690630b]
/home/nix/.elan/toolchains/leanprover--lean4---v4.12.0-rc1/bin/lean(_start+0x25) [0x55da84e64785]
zsh: IOT instruction (core dumped)  lean --run foo.lean

[Sebastian Ullrich]

On Linux, that is. I don't think there's an issue for cross-platform support yet.

[Youngju Song]

@Henrik Böving Mine shows this:

~$ cat foo.lean
def main : IO Unit := do
  panic! "ahhh"
~$ export LEAN_ABORT_ON_PANIC=1
~$ echo $LEAN_ABORT_ON_PANIC
1
~$ lean --run foo.lean
PANIC at main foo:2:2: ahhh
[1]    40956 abort      lean --run foo.lean
~$ lean --version
Lean (version 4.16.0-nightly-2024-12-04, arm64-apple-darwin23.6.0, commit c5181569f959, Release)
~$ echo $0
-zsh
~$ sw_vers
ProductName:        macOS
ProductVersion:     14.7.1
BuildVersion:       23H222

[Youngju Song]

Tried the latest version (Lean (version 4.16.0-nightly-2025-01-03, arm64-apple-darwin23.6.0, commit 19078655bcfd, Release)) but the same result.
@Sebastian Ullrich (just to be clear) do you mean that Lean does not support this feature for operating systems other than Linux?

[Sebastian Ullrich]

It does not currently