Debugging an Option.get! panic

Stream: lean4

[Michael Rothgang]

On [e2e468c](https://github.com/leanprover-community/mathlib4/pull/30658/commits/e2e468ce936152145e3765ed4461c0b2b1754d5a) (extending the commandStart linter, in-progress), there is a linter panic in many files, which look very similar to the following:

I understand this is due to calling Option.get! on a none value --- but how would I debug which call is causing this? The backtrace appears very unhelpful.

[Michael Rothgang]

Here is the error message: PastedText.txt

[Michael Rothgang]

(The error is almost sure a linter bug: but being unable to debug it without magic skills is not ideal :-))

[Aaron Liu]

it's debuggin time

[Henrik Böving]

I would set export LEAN_ABORT_ON_PANIC=1 and then run whatever file is causing the issue with lake lean path/to/file.lean. You should then get a backtrace that looks something like this:

/home/nix/.elan/toolchains/leanprover--lean4---v4.18.0-rc1/lib/lean/libleanshared.so(+0x738ab82) [0x7f781dd8ab82]
/home/nix/.elan/toolchains/leanprover--lean4---v4.18.0-rc1/lib/lean/libleanshared.so(lean_panic+0x4e) [0x7f781dd8a9ee]
/home/nix/.elan/toolchains/leanprover--lean4---v4.18.0-rc1/lib/lean/libleanshared.so(lean_panic_fn+0x15) [0x7f781dd8ac15]
...

which hopefully points closer to the caller. Note however that because mathlib is not using native compilation for it's system (for good reasons) you might end up receiving essentially a lot of stack frames that only talk about the interpreter which will likely not help you. If that happens I would probably start adding debug traces along the program and try to bisect my way to the failure by observing which ones print before the abort and which ones do not.

It's a bit unfortunate that we currently do not have nice debugging tools for the interpreter and likely also will not in the near term future :/

[Aaron Liu]

none of the top 22 lines of the trace have any function names, except for lean_panic_fn

[Aaron Liu]

and below that is just the docs#Lean.Elab.Command.runLinters

[Aaron Liu]

I picked one instance of the panic to debug (here) and the panic is in _private.Mathlib.Tactic.Linter.CommandStart.0.Mathlib.Linter.generateCorrespondence

[Aaron Liu]

it's because it's trying to get the trailing whitespace of synthetic syntax

[Aaron Liu]

which doesn't exist so it panics