Find `get!` panic source

Stream: lean4

[Max Nowak]

I have (possibly foolishly) used a lot of Option.get! in my code, and now I get the error PANIC at Option.get! Init.Data.Option.BasicAux:16:14: value is none, which is very unhelpful since I don't know which of the many get!s actually caused it :/. Is there an easy way to find that information?

[Henrik Böving]

If you have an up to date-ish version of Lean and are running on Linux it should give you a full stack trace...if you're not on Linux there isnt really, I guess you could try to debug your binary but that is sort of painful due to the difference between the binary and the code you wrote (since it gets translated to C) so you're most likely better off putting debug prints

[Patrick Massot]

It would be nice to have more information in the panic message since this message is also very frequently encountered by the Lean server and displayed in VSCode.

[James Gallicchio]

maybe this is your incentive to get rid of those get!s :P

[James Gallicchio]

you could also do a macro-cheat to get locations to print:

macro "option_get!" o:term : term =>
  `(assert! (Option.isSome $o);
    ($o).get!)

#eval get_with_loc! (none : Option Nat)
#eval get_with_loc! (some 5)

and find-replace all your Option.get! with this. the meta-magicians might have a better solution than this though

[Sebastian Ullrich]

Henrik Böving said:

I guess you could try to debug your binary but that is sort of painful due to the difference between the binary and the code you wrote

You can still get a stack trace as good as on Linux that way (https://leanprover.github.io/lean4/doc/dev/debugging.html#debuggers)