Editor panic

Stream: lean4

[Patrick Massot]

When I see in VSCode's problem list errors starting with:

Lean (version 4.0.0-nightly-2022-09-23, commit eed569153b53, Release)
elan 1.4.2 (4a1b1b918 2022-09-13)
Lean (version 4.0.0-nightly-2022-09-23, commit eed569153b53, Release)
PANIC at getElem! Init.Util:77:36: index out of bounds

Is there anything to do to get a better bug report? Should I copy all the other lines? Where should this be reported?

[Mario Carneiro]

The other lines are important

[Mario Carneiro]

It's very obfuscated (we really need a demangler), but you can kind of see the call stack in the report

[Mario Carneiro]

Where it should be reported depends on who's calling getElem!

[Mario Carneiro]

of course getElem! is not buggy here, it's doing what it is supposed to

[Patrick Massot]

I think the following is one full trace:

backtrace:
/home/pmassot/.elan/toolchains/leanprover--lean4---nightly-2022-09-23/bin/../lib/lean/libleanshared.so(lean_panic_fn+0x9e)[0x7fb35c66752e]
/home/pmassot/.elan/toolchains/leanprover--lean4---nightly-2022-09-23/bin/../lib/lean/libleanshared.so(+0x317e523)[0x7fb35c660523]
/home/pmassot/.elan/toolchains/leanprover--lean4---nightly-2022-09-23/bin/../lib/lean/libleanshared.so(+0x317c7e7)[0x7fb35c65e7e7]
/home/pmassot/.elan/toolchains/leanprover--lean4---nightly-2022-09-23/bin/../lib/lean/libleanshared.so(+0x317e893)[0x7fb35c660893]
/home/pmassot/.elan/toolchains/leanprover--lean4---nightly-2022-09-23/bin/../lib/lean/libleanshared.so(+0x317c7e7)[0x7fb35c65e7e7]
/home/pmassot/.elan/toolchains/leanprover--lean4---nightly-2022-09-23/bin/../lib/lean/libleanshared.so(+0x317e893)[0x7fb35c660893]
/home/pmassot/.elan/toolchains/leanprover--lean4---nightly-2022-09-23/bin/../lib/lean/libleanshared.so(+0x317c7e7)[0x7fb35c65e7e7]
/home/pmassot/.elan/toolchains/leanprover--lean4---nightly-2022-09-23/bin/../lib/lean/libleanshared.so(+0x31804d9)[0x7fb35c6624d9]
/home/pmassot/.elan/toolchains/leanprover--lean4---nightly-2022-09-23/bin/../lib/lean/libleanshared.so(+0x3178f43)[0x7fb35c65af43]
/home/pmassot/.elan/toolchains/leanprover--lean4---nightly-2022-09-23/bin/../lib/lean/libleanshared.so(+0x3180107)[0x7fb35c662107]
/home/pmassot/.elan/toolchains/leanprover--lean4---nightly-2022-09-23/bin/../lib/lean/libleanshared.so(+0x317fd53)[0x7fb35c661d53]
/home/pmassot/.elan/toolchains/leanprover--lean4---nightly-2022-09-23/bin/../lib/lean/libleanshared.so(lean_apply_3+0x402)[0x7fb35c673e62]
/home/pmassot/.elan/toolchains/leanprover--lean4---nightly-2022-09-23/bin/../lib/lean/libleanshared.so(l_Lean_Elab_withInfoTreeContext___at___private_Lean_Elab_Command_0__Lean_Elab_Command_elabCommandUsing___spec__2+0x162)[0x7fb35c4fe232]
/home/pmassot/.elan/toolchains/leanprover--lean4---nightly-2022-09-23/bin/../lib/lean/libleanshared.so(l___private_Lean_Elab_Command_0__Lean_Elab_Command_elabCommandUsing+0x1e3)[0x7fb35c4ffe73]
/home/pmassot/.elan/toolchains/leanprover--lean4---nightly-2022-09-23/bin/../lib/lean/libleanshared.so(lean_apply_3+0x3c2)[0x7fb35c673e22]
/home/pmassot/.elan/toolchains/leanprover--lean4---nightly-2022-09-23/bin/../lib/lean/libleanshared.so(lean_apply_3+0x3a4)[0x7fb35c673e04]
/home/pmassot/.elan/toolchains/leanprover--lean4---nightly-2022-09-23/bin/../lib/lean/libleanshared.so(l_Lean_Elab_withLogging___at_Lean_Elab_Command_elabCommand___spec__2+0x54)[0x7fb35c508814]
/home/pmassot/.elan/toolchains/leanprover--lean4---nightly-2022-09-23/bin/../lib/lean/libleanshared.so(l_Lean_Elab_Command_elabCommandTopLevel___lambda__2+0x1b0)[0x7fb35c518000]
/home/pmassot/.elan/toolchains/leanprover--lean4---nightly-2022-09-23/bin/../lib/lean/libleanshared.so(lean_apply_3+0x38a)[0x7fb35c673dea]
/home/pmassot/.elan/toolchains/leanprover--lean4---nightly-2022-09-23/bin/../lib/lean/libleanshared.so(l_Lean_Elab_withLogging___at_Lean_Elab_Command_elabCommand___spec__2+0x54)[0x7fb35c508814]
/home/pmassot/.elan/toolchains/leanprover--lean4---nightly-2022-09-23/bin/../lib/lean/libleanshared.so(l_Lean_Server_Snapshots_compileNextCmd___lambda__2+0xa)[0x7fb35b4f096a]
/home/pmassot/.elan/toolchains/leanprover--lean4---nightly-2022-09-23/bin/../lib/lean/libleanshared.so(lean_apply_1+0x182)[0x7fb35c671e52]
/home/pmassot/.elan/toolchains/leanprover--lean4---nightly-2022-09-23/bin/../lib/lean/libleanshared.so(l_IO_withStderr___at_Lean_Server_Snapshots_compileNextCmd___spec__4+0x6e)[0x7fb35b4efd3e]
/home/pmassot/.elan/toolchains/leanprover--lean4---nightly-2022-09-23/bin/../lib/lean/libleanshared.so(lean_apply_1+0x16a)[0x7fb35c671e3a]
/home/pmassot/.elan/toolchains/leanprover--lean4---nightly-2022-09-23/bin/../lib/lean/libleanshared.so(l_IO_withStdout___at_Lean_Server_Snapshots_compileNextCmd___spec__2+0x6e)[0x7fb35b4ef63e]
/home/pmassot/.elan/toolchains/leanprover--lean4---nightly-2022-09-23/bin/../lib/lean/libleanshared.so(lean_apply_1+0x16a)[0x7fb35c671e3a]
/home/pmassot/.elan/toolchains/leanprover--lean4---nightly-2022-09-23/bin/../lib/lean/libleanshared.so(l_IO_withStdin___at_Lean_Server_Snapshots_compileNextCmd___spec__3+0x6e)[0x7fb35b4ef9be]
/home/pmassot/.elan/toolchains/leanprover--lean4---nightly-2022-09-23/bin/../lib/lean/libleanshared.so(l_IO_FS_withIsolatedStreams___at_Lean_Server_Snapshots_compileNextCmd___spec__1+0x192)[0x7fb35b4f01e2]
/home/pmassot/.elan/toolchains/leanprover--lean4---nightly-2022-09-23/bin/../lib/lean/libleanshared.so(l_Lean_Server_Snapshots_compileNextCmd+0x11b9)[0x7fb35b4f1f79]
/home/pmassot/.elan/toolchains/leanprover--lean4---nightly-2022-09-23/bin/../lib/lean/libleanshared.so(l___private_Lean_Server_FileWorker_0__Lean_Server_FileWorker_nextCmdSnap___lambda__1+0x20e)[0x7fb35b4c29de]
/home/pmassot/.elan/toolchains/leanprover--lean4---nightly-2022-09-23/bin/../lib/lean/libleanshared.so(l___private_Lean_Server_FileWorker_0__Lean_Server_FileWorker_nextCmdSnap+0x596)[0x7fb35b4c3b56]
/home/pmassot/.elan/toolchains/leanprover--lean4---nightly-2022-09-23/bin/../lib/lean/libleanshared.so(lean_apply_2+0x69c)[0x7fb35c672fac]
/home/pmassot/.elan/toolchains/leanprover--lean4---nightly-2022-09-23/bin/../lib/lean/libleanshared.so(l_IO_AsyncList_unfoldAsync_step___rarg+0x39)[0x7fb35b48bd89]
/home/pmassot/.elan/toolchains/leanprover--lean4---nightly-2022-09-23/bin/../lib/lean/libleanshared.so(lean_apply_1+0x462)[0x7fb35c672132]
/home/pmassot/.elan/toolchains/leanprover--lean4---nightly-2022-09-23/bin/../lib/lean/libleanshared.so(l_EIO_toBaseIO___rarg+0xd)[0x7fb35a0294dd]
/home/pmassot/.elan/toolchains/leanprover--lean4---nightly-2022-09-23/bin/../lib/lean/libleanshared.so(lean_apply_1+0x42d)[0x7fb35c6720fd]
/home/pmassot/.elan/toolchains/leanprover--lean4---nightly-2022-09-23/bin/../lib/lean/libleanshared.so(+0x31a33be)[0x7fb35c6853be]
/home/pmassot/.elan/toolchains/leanprover--lean4---nightly-2022-09-23/bin/../lib/lean/libleanshared.so(lean_apply_1+0x42d)[0x7fb35c6720fd]
/home/pmassot/.elan/toolchains/leanprover--lean4---nightly-2022-09-23/bin/../lib/lean/libleanshared.so(+0x318e662)[0x7fb35c670662]
/home/pmassot/.elan/toolchains/leanprover--lean4---nightly-2022-09-23/bin/../lib/lean/libleanshared.so(+0x318f992)[0x7fb35c671992]
/home/pmassot/.elan/toolchains/leanprover--lean4---nightly-2022-09-23/bin/../lib/lean/libleanshared.so(+0x31837f1)[0x7fb35c6657f1]
/lib/x86_64-linux-gnu/libc.so.6(+0x94b43)[0x7fb359324b43]
/lib/x86_64-linux-gnu/libc.so.6(+0x126a00)[0x7fb3593b6a00]

[Mario Carneiro]

oh wow that's a really unhelpful backtrace

[Patrick Massot]

It certainly didn't help me...

[Mario Carneiro]

Normally those function names would give a hint but there is a big stack of functions missing debug info and the first thing you can see with a name, elabCommandUsing, is just the top level "elaborate a command" function

[Patrick Massot]

A new case of editor integration panic:

Lean (version 4.0.0-nightly-2022-10-12, commit aa845dee98e3, Release)
PANIC at List.tail! Init.Data.List.BasicAux:46:13: empty list
backtrace:
/home/pmassot/.elan/toolchains/leanprover--lean4---nightly-2022-10-12/bin/../lib/lean/libleanshared.so(lean_panic_fn+0x9e)[0x7ff82cd570ce]
/home/pmassot/.elan/toolchains/leanprover--lean4---nightly-2022-10-12/bin/../lib/lean/libleanshared.so(+0x336a0c3)[0x7ff82cd500c3]
/home/pmassot/.elan/toolchains/leanprover--lean4---nightly-2022-10-12/bin/../lib/lean/libleanshared.so(+0x3368387)[0x7ff82cd4e387]
/home/pmassot/.elan/toolchains/leanprover--lean4---nightly-2022-10-12/bin/../lib/lean/libleanshared.so(+0x336a433)[0x7ff82cd50433]
/home/pmassot/.elan/toolchains/leanprover--lean4---nightly-2022-10-12/bin/../lib/lean/libleanshared.so(+0x3368387)[0x7ff82cd4e387]
/home/pmassot/.elan/toolchains/leanprover--lean4---nightly-2022-10-12/bin/../lib/lean/libleanshared.so(+0x336c079)[0x7ff82cd52079]
/home/pmassot/.elan/toolchains/leanprover--lean4---nightly-2022-10-12/bin/../lib/lean/libleanshared.so(+0x3364ae3)[0x7ff82cd4aae3]
/home/pmassot/.elan/toolchains/leanprover--lean4---nightly-2022-10-12/bin/../lib/lean/libleanshared.so(+0x336bca7)[0x7ff82cd51ca7]
/home/pmassot/.elan/toolchains/leanprover--lean4---nightly-2022-10-12/bin/../lib/lean/libleanshared.so(+0x336b97d)[0x7ff82cd5197d]
/home/pmassot/.elan/toolchains/leanprover--lean4---nightly-2022-10-12/bin/../lib/lean/libleanshared.so(lean_apply_3+0x453)[0x7ff82cd63a53]
/home/pmassot/.elan/toolchains/leanprover--lean4---nightly-2022-10-12/bin/../lib/lean/libleanshared.so(+0x336a0c3)[0x7ff82cd500c3]
/home/pmassot/.elan/toolchains/leanprover--lean4---nightly-2022-10-12/bin/../lib/lean/libleanshared.so(+0x3368387)[0x7ff82cd4e387]
/home/pmassot/.elan/toolchains/leanprover--lean4---nightly-2022-10-12/bin/../lib/lean/libleanshared.so(+0x336c079)[0x7ff82cd52079]
/home/pmassot/.elan/toolchains/leanprover--lean4---nightly-2022-10-12/bin/../lib/lean/libleanshared.so(+0x3364ae3)[0x7ff82cd4aae3]
/home/pmassot/.elan/toolchains/leanprover--lean4---nightly-2022-10-12/bin/../lib/lean/libleanshared.so(+0x336bca7)[0x7ff82cd51ca7]
/home/pmassot/.elan/toolchains/leanprover--lean4---nightly-2022-10-12/bin/../lib/lean/libleanshared.so(+0x336b97d)[0x7ff82cd5197d]
/home/pmassot/.elan/toolchains/leanprover--lean4---nightly-2022-10-12/bin/../lib/lean/libleanshared.so(lean_apply_5+0x822)[0x7ff82cd65892]
/home/pmassot/.elan/toolchains/leanprover--lean4---nightly-2022-10-12/bin/../lib/lean/libleanshared.so(l_Lean_Meta_MetaM_run_x27___rarg+0x107)[0x7ff82c97dc97]
/home/pmassot/.elan/toolchains/leanprover--lean4---nightly-2022-10-12/bin/../lib/lean/libleanshared.so(lean_apply_3+0x6b1)[0x7ff82cd63cb1]
/home/pmassot/.elan/toolchains/leanprover--lean4---nightly-2022-10-12/bin/../lib/lean/libleanshared.so(l_Lean_Core_CoreM_run_x27___rarg+0x92)[0x7ff82c1fe9d2]
/home/pmassot/.elan/toolchains/leanprover--lean4---nightly-2022-10-12/bin/../lib/lean/libleanshared.so(lean_apply_1+0x4a4)[0x7ff82cd61d14]
/home/pmassot/.elan/toolchains/leanprover--lean4---nightly-2022-10-12/bin/../lib/lean/libleanshared.so(l_EIO_toBaseIO___rarg+0xd)[0x7ff82a5bfa3d]
/home/pmassot/.elan/toolchains/leanprover--lean4---nightly-2022-10-12/bin/../lib/lean/libleanshared.so(lean_apply_1+0x42d)[0x7ff82cd61c9d]
/home/pmassot/.elan/toolchains/leanprover--lean4---nightly-2022-10-12/bin/../lib/lean/libleanshared.so(l_EStateM_bind___rarg+0x13)[0x7ff82a5ad203]
/home/pmassot/.elan/toolchains/leanprover--lean4---nightly-2022-10-12/bin/../lib/lean/libleanshared.so(lean_apply_1+0x462)[0x7ff82cd61cd2]
/home/pmassot/.elan/toolchains/leanprover--lean4---nightly-2022-10-12/bin/../lib/lean/libleanshared.so(+0x338ef5e)[0x7ff82cd74f5e]
/home/pmassot/.elan/toolchains/leanprover--lean4---nightly-2022-10-12/bin/../lib/lean/libleanshared.so(lean_apply_1+0x42d)[0x7ff82cd61c9d]
/home/pmassot/.elan/toolchains/leanprover--lean4---nightly-2022-10-12/bin/../lib/lean/libleanshared.so(+0x337a202)[0x7ff82cd60202]
/home/pmassot/.elan/toolchains/leanprover--lean4---nightly-2022-10-12/bin/../lib/lean/libleanshared.so(+0x337b532)[0x7ff82cd61532]
/home/pmassot/.elan/toolchains/leanprover--lean4---nightly-2022-10-12/bin/../lib/lean/libleanshared.so(+0x336f391)[0x7ff82cd55391]
/lib/x86_64-linux-gnu/libc.so.6(+0x94b43)[0x7ff829828b43]
/lib/x86_64-linux-gnu/libc.so.6(+0x126a00)[0x7ff8298baa00]

[Gabriel Ebner]

Do you have maybe have a repro? Or at least the file this happened with?

[Patrick Massot]

Unfortunately no, those are completely random errors that pop up when editing files. I think this happens only when some line isn't finished

[Gabriel Ebner]

Just pasting the unfinished line here could already be helpful.

[Kevin Buzzard]

Oh this reminds me of the "unreachable code has been reached" error which used to pop up in Lean 3 when you were in the middle of defining an instance of a structure. Super-hard to reproduce because you were busy typing and then you realised that Lean had stopped running. Fixed by Gabriel removing the check :-)

[Patrick Massot]

Yes, I always notice the popup too late to reproduce.