lean4 icon indicating copy to clipboard operation
lean4 copied to clipboard

Published 20 hours ago • verified publisher icon leanprover

panic in info handler on unterminated doc comment

Open digama0 opened this issue 3 years ago • 4 comments

The following lean file:

/--

causes this panic:

PANIC at Lean.Server.Snapshots.Snapshot.infoTree Lean.Server.Snapshots:68:2: assertion violation: s.cmdState.infoState.trees.size == 1
  
backtrace:
/home/mario/Documents/lean/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(lean_panic_fn+0x10f)[0x7fe4329d1e2f]
/home/mario/Documents/lean/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(l_Array_mapMUnsafe_map___at_Lean_Server_FileWorker_handleDocumentHighlight___spec__1+0x92)[0x7fe4326b5b12]
/home/mario/Documents/lean/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(l___private_Lean_Server_FileWorker_0__Lean_Server_FileWorker_publishIleanInfo+0x36)[0x7fe4326eeb06]
/home/mario/Documents/lean/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(l___private_Lean_Server_FileWorker_0__Lean_Server_FileWorker_nextCmdSnap___lambda__1+0x9a8)[0x7fe4326ef9a8]
/home/mario/Documents/lean/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(l___private_Lean_Server_FileWorker_0__Lean_Server_FileWorker_nextCmdSnap+0xa4b)[0x7fe4326f143b]
/home/mario/Documents/lean/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(lean_apply_2+0xa64)[0x7fe4329de7a4]
/home/mario/Documents/lean/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(l_IO_AsyncList_unfoldAsync_step___rarg+0x33)[0x7fe43272a343]
/home/mario/Documents/lean/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(lean_apply_1+0x9c4)[0x7fe4329dc8a4]
/home/mario/Documents/lean/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(l_EIO_toBaseIO___rarg+0x13)[0x7fe4300b3e23]
/home/mario/Documents/lean/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(lean_apply_1+0xa18)[0x7fe4329dc8f8]
/home/mario/Documents/lean/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(+0x30f1d45)[0x7fe4329f7d45]
/home/mario/Documents/lean/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(lean_apply_1+0xa18)[0x7fe4329dc8f8]
/home/mario/Documents/lean/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(+0x30d5314)[0x7fe4329db314]
/home/mario/Documents/lean/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(+0x30d59ff)[0x7fe4329db9ff]
/home/mario/Documents/lean/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(+0x30c95b3)[0x7fe4329cf5b3]
/lib/x86_64-linux-gnu/libc.so.6(+0x94b43)[0x7fe42f74cb43]
/lib/x86_64-linux-gnu/libc.so.6(+0x126a00)[0x7fe42f7dea00]
PANIC at Lean.Elab.InfoTree.visitM.go Lean.Server.InfoUtils:36:21: unexpected context-free info tree node
backtrace:
/home/mario/Documents/lean/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(lean_panic_fn+0x10f)[0x7fe4329d1e2f]
/home/mario/Documents/lean/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(l_panic___at_Lean_Server_findReferences___spec__4+0x17)[0x7fe43283c7d7]
/home/mario/Documents/lean/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(l_Lean_Elab_InfoTree_visitM_x27___at_Lean_Server_findReferences___spec__1+0x5d)[0x7fe43283d60d]
/home/mario/Documents/lean/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(l_Array_forInUnsafe_loop___at_Lean_Server_findReferences___spec__6+0xc9)[0x7fe43283de59]
/home/mario/Documents/lean/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(l_Lean_Server_findReferences+0x2c)[0x7fe43283dfbc]
/home/mario/Documents/lean/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(l_Lean_Server_findModuleRefs+0x1b)[0x7fe4328488bb]
/home/mario/Documents/lean/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(l___private_Lean_Server_FileWorker_0__Lean_Server_FileWorker_publishIleanInfo+0x5e)[0x7fe4326eeb2e]
/home/mario/Documents/lean/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(l___private_Lean_Server_FileWorker_0__Lean_Server_FileWorker_nextCmdSnap___lambda__1+0x9a8)[0x7fe4326ef9a8]
/home/mario/Documents/lean/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(l___private_Lean_Server_FileWorker_0__Lean_Server_FileWorker_nextCmdSnap+0xa4b)[0x7fe4326f143b]
/home/mario/Documents/lean/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(lean_apply_2+0xa64)[0x7fe4329de7a4]
/home/mario/Documents/lean/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(l_IO_AsyncList_unfoldAsync_step___rarg+0x33)[0x7fe43272a343]
/home/mario/Documents/lean/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(lean_apply_1+0x9c4)[0x7fe4329dc8a4]
/home/mario/Documents/lean/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(l_EIO_toBaseIO___rarg+0x13)[0x7fe4300b3e23]
/home/mario/Documents/lean/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(lean_apply_1+0xa18)[0x7fe4329dc8f8]
/home/mario/Documents/lean/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(+0x30f1d45)[0x7fe4329f7d45]
/home/mario/Documents/lean/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(lean_apply_1+0xa18)[0x7fe4329dc8f8]
/home/mario/Documents/lean/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(+0x30d5314)[0x7fe4329db314]
/home/mario/Documents/lean/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(+0x30d59ff)[0x7fe4329db9ff]
/home/mario/Documents/lean/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(+0x30c95b3)[0x7fe4329cf5b3]
/lib/x86_64-linux-gnu/libc.so.6(+0x94b43)[0x7fe42f74cb43]
/lib/x86_64-linux-gnu/libc.so.6(+0x126a00)[0x7fe42f7dea00]
PANIC at Lean.Elab.InfoTree.visitM.go Lean.Server.InfoUtils:36:21: unexpected context-free info tree node
backtrace:
/home/mario/Documents/lean/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(lean_panic_fn+0x10f)[0x7fe4329d1e2f]
/home/mario/Documents/lean/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(l_panic___at_Lean_Server_combineFvars_buildIdMap___spec__8+0x17)[0x7fe43283fe37]
/home/mario/Documents/lean/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(l_Lean_Elab_InfoTree_visitM_x27___at_Lean_Server_combineFvars_buildIdMap___spec__5+0x5d)[0x7fe432840c0d]
/home/mario/Documents/lean/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(l_Array_foldlMUnsafe_fold___at_Lean_Server_combineFvars_buildIdMap___spec__10+0x74)[0x7fe432840fb4]
/home/mario/Documents/lean/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(l_Lean_Server_combineFvars_buildIdMap+0xad)[0x7fe4328411ad]
/home/mario/Documents/lean/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(l_Lean_Server_combineFvars+0x4b)[0x7fe432842fab]
/home/mario/Documents/lean/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(l_Lean_Server_findModuleRefs+0x29)[0x7fe4328488c9]
/home/mario/Documents/lean/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(l___private_Lean_Server_FileWorker_0__Lean_Server_FileWorker_publishIleanInfo+0x5e)[0x7fe4326eeb2e]
/home/mario/Documents/lean/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(l___private_Lean_Server_FileWorker_0__Lean_Server_FileWorker_nextCmdSnap___lambda__1+0x9a8)[0x7fe4326ef9a8]
/home/mario/Documents/lean/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(l___private_Lean_Server_FileWorker_0__Lean_Server_FileWorker_nextCmdSnap+0xa4b)[0x7fe4326f143b]
/home/mario/Documents/lean/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(lean_apply_2+0xa64)[0x7fe4329de7a4]
/home/mario/Documents/lean/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(l_IO_AsyncList_unfoldAsync_step___rarg+0x33)[0x7fe43272a343]
/home/mario/Documents/lean/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(lean_apply_1+0x9c4)[0x7fe4329dc8a4]
/home/mario/Documents/lean/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(l_EIO_toBaseIO___rarg+0x13)[0x7fe4300b3e23]
/home/mario/Documents/lean/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(lean_apply_1+0xa18)[0x7fe4329dc8f8]
/home/mario/Documents/lean/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(+0x30f1d45)[0x7fe4329f7d45]
/home/mario/Documents/lean/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(lean_apply_1+0xa18)[0x7fe4329dc8f8]
/home/mario/Documents/lean/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(+0x30d5314)[0x7fe4329db314]
/home/mario/Documents/lean/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(+0x30d59ff)[0x7fe4329db9ff]
/home/mario/Documents/lean/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(+0x30c95b3)[0x7fe4329cf5b3]
/lib/x86_64-linux-gnu/libc.so.6(+0x94b43)[0x7fe42f74cb43]
/lib/x86_64-linux-gnu/libc.so.6(+0x126a00)[0x7fe42f7dea00]
PANIC at Lean.Server.Snapshots.Snapshot.infoTree Lean.Server.Snapshots:68:2: assertion violation: s.cmdState.infoState.trees.size == 1
  
backtrace:
/home/mario/Documents/lean/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(lean_panic_fn+0x10f)[0x7fe4329d1e2f]
/home/mario/Documents/lean/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(l_Array_mapMUnsafe_map___at_Lean_Server_FileWorker_handleDocumentHighlight___spec__1+0x92)[0x7fe4326b5b12]
/home/mario/Documents/lean/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(l___private_Lean_Server_FileWorker_0__Lean_Server_FileWorker_publishIleanInfo+0x36)[0x7fe4326eeb06]
/home/mario/Documents/lean/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(l___private_Lean_Server_FileWorker_0__Lean_Server_FileWorker_nextCmdSnap___lambda__1+0x9a8)[0x7fe4326ef9a8]
/home/mario/Documents/lean/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(l___private_Lean_Server_FileWorker_0__Lean_Server_FileWorker_nextCmdSnap+0xa4b)[0x7fe4326f143b]
/home/mario/Documents/lean/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(lean_apply_2+0xa64)[0x7fe4329de7a4]
/home/mario/Documents/lean/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(l_IO_AsyncList_unfoldAsync_step___rarg+0x33)[0x7fe43272a343]
/home/mario/Documents/lean/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(lean_apply_1+0x9c4)[0x7fe4329dc8a4]
/home/mario/Documents/lean/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(l_EIO_toBaseIO___rarg+0x13)[0x7fe4300b3e23]
/home/mario/Documents/lean/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(lean_apply_1+0xa18)[0x7fe4329dc8f8]
/home/mario/Documents/lean/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(+0x30f1d45)[0x7fe4329f7d45]
/home/mario/Documents/lean/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(lean_apply_1+0xa18)[0x7fe4329dc8f8]
/home/mario/Documents/lean/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(+0x30d5314)[0x7fe4329db314]
/home/mario/Documents/lean/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(+0x30d59ff)[0x7fe4329db9ff]
/home/mario/Documents/lean/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(+0x30c95b3)[0x7fe4329cf5b3]
/lib/x86_64-linux-gnu/libc.so.6(+0x94b43)[0x7fe42f74cb43]
/lib/x86_64-linux-gnu/libc.so.6(+0x126a00)[0x7fe42f7dea00]
PANIC at Lean.Elab.InfoTree.visitM.go Lean.Server.InfoUtils:36:21: unexpected context-free info tree node
backtrace:
/home/mario/Documents/lean/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(lean_panic_fn+0x10f)[0x7fe4329d1e2f]
/home/mario/Documents/lean/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(l_panic___at_Lean_Server_findReferences___spec__4+0x17)[0x7fe43283c7d7]
/home/mario/Documents/lean/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(l_Lean_Elab_InfoTree_visitM_x27___at_Lean_Server_findReferences___spec__1+0x5d)[0x7fe43283d60d]
/home/mario/Documents/lean/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(l_Array_forInUnsafe_loop___at_Lean_Server_findReferences___spec__6+0xc9)[0x7fe43283de59]
/home/mario/Documents/lean/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(l_Lean_Server_findReferences+0x2c)[0x7fe43283dfbc]
/home/mario/Documents/lean/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(l_Lean_Server_findModuleRefs+0x1b)[0x7fe4328488bb]
/home/mario/Documents/lean/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(l___private_Lean_Server_FileWorker_0__Lean_Server_FileWorker_publishIleanInfo+0x5e)[0x7fe4326eeb2e]
/home/mario/Documents/lean/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(l___private_Lean_Server_FileWorker_0__Lean_Server_FileWorker_nextCmdSnap___lambda__1+0x9a8)[0x7fe4326ef9a8]
/home/mario/Documents/lean/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(l___private_Lean_Server_FileWorker_0__Lean_Server_FileWorker_nextCmdSnap+0xa4b)[0x7fe4326f143b]
/home/mario/Documents/lean/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(lean_apply_2+0xa64)[0x7fe4329de7a4]
/home/mario/Documents/lean/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(l_IO_AsyncList_unfoldAsync_step___rarg+0x33)[0x7fe43272a343]
/home/mario/Documents/lean/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(lean_apply_1+0x9c4)[0x7fe4329dc8a4]
/home/mario/Documents/lean/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(l_EIO_toBaseIO___rarg+0x13)[0x7fe4300b3e23]
/home/mario/Documents/lean/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(lean_apply_1+0xa18)[0x7fe4329dc8f8]
/home/mario/Documents/lean/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(+0x30f1d45)[0x7fe4329f7d45]
/home/mario/Documents/lean/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(lean_apply_1+0xa18)[0x7fe4329dc8f8]
/home/mario/Documents/lean/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(+0x30d5314)[0x7fe4329db314]
/home/mario/Documents/lean/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(+0x30d59ff)[0x7fe4329db9ff]
/home/mario/Documents/lean/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(+0x30c95b3)[0x7fe4329cf5b3]
/lib/x86_64-linux-gnu/libc.so.6(+0x94b43)[0x7fe42f74cb43]
/lib/x86_64-linux-gnu/libc.so.6(+0x126a00)[0x7fe42f7dea00]
PANIC at Lean.Elab.InfoTree.visitM.go Lean.Server.InfoUtils:36:21: unexpected context-free info tree node
backtrace:
/home/mario/Documents/lean/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(lean_panic_fn+0x10f)[0x7fe4329d1e2f]
/home/mario/Documents/lean/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(l_panic___at_Lean_Server_combineFvars_buildIdMap___spec__8+0x17)[0x7fe43283fe37]
/home/mario/Documents/lean/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(l_Lean_Elab_InfoTree_visitM_x27___at_Lean_Server_combineFvars_buildIdMap___spec__5+0x5d)[0x7fe432840c0d]
/home/mario/Documents/lean/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(l_Array_foldlMUnsafe_fold___at_Lean_Server_combineFvars_buildIdMap___spec__10+0x74)[0x7fe432840fb4]
/home/mario/Documents/lean/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(l_Lean_Server_combineFvars_buildIdMap+0xad)[0x7fe4328411ad]
/home/mario/Documents/lean/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(l_Lean_Server_combineFvars+0x4b)[0x7fe432842fab]
/home/mario/Documents/lean/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(l_Lean_Server_findModuleRefs+0x29)[0x7fe4328488c9]
/home/mario/Documents/lean/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(l___private_Lean_Server_FileWorker_0__Lean_Server_FileWorker_publishIleanInfo+0x5e)[0x7fe4326eeb2e]
/home/mario/Documents/lean/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(l___private_Lean_Server_FileWorker_0__Lean_Server_FileWorker_nextCmdSnap___lambda__1+0x9a8)[0x7fe4326ef9a8]
/home/mario/Documents/lean/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(l___private_Lean_Server_FileWorker_0__Lean_Server_FileWorker_nextCmdSnap+0xa4b)[0x7fe4326f143b]
/home/mario/Documents/lean/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(lean_apply_2+0xa64)[0x7fe4329de7a4]
/home/mario/Documents/lean/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(l_IO_AsyncList_unfoldAsync_step___rarg+0x33)[0x7fe43272a343]
/home/mario/Documents/lean/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(lean_apply_1+0x9c4)[0x7fe4329dc8a4]
/home/mario/Documents/lean/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(l_EIO_toBaseIO___rarg+0x13)[0x7fe4300b3e23]
/home/mario/Documents/lean/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(lean_apply_1+0xa18)[0x7fe4329dc8f8]
/home/mario/Documents/lean/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(+0x30f1d45)[0x7fe4329f7d45]
/home/mario/Documents/lean/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(lean_apply_1+0xa18)[0x7fe4329dc8f8]
/home/mario/Documents/lean/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(+0x30d5314)[0x7fe4329db314]
/home/mario/Documents/lean/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(+0x30d59ff)[0x7fe4329db9ff]
/home/mario/Documents/lean/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(+0x30c95b3)[0x7fe4329cf5b3]
/lib/x86_64-linux-gnu/libc.so.6(+0x94b43)[0x7fe42f74cb43]
/lib/x86_64-linux-gnu/libc.so.6(+0x126a00)[0x7fe42f7dea00]
PANIC at Lean.Server.Snapshots.Snapshot.infoTree Lean.Server.Snapshots:68:2: assertion violation: s.cmdState.infoState.trees.size == 1
  
backtrace:
/home/mario/Documents/lean/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(lean_panic_fn+0x10f)[0x7fe4329d1e2f]
/home/mario/Documents/lean/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(l_Array_mapMUnsafe_map___at_Lean_Server_FileWorker_handleDocumentHighlight___spec__1+0x92)[0x7fe4326b5b12]
/home/mario/Documents/lean/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(l___private_Lean_Server_FileWorker_0__Lean_Server_FileWorker_publishIleanInfo+0x36)[0x7fe4326eeb06]
/home/mario/Documents/lean/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(l___private_Lean_Server_FileWorker_0__Lean_Server_FileWorker_nextCmdSnap+0x59f)[0x7fe4326f0f8f]
/home/mario/Documents/lean/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(lean_apply_2+0xa64)[0x7fe4329de7a4]
/home/mario/Documents/lean/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(l_IO_AsyncList_unfoldAsync_step___rarg+0x33)[0x7fe43272a343]
/home/mario/Documents/lean/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(lean_apply_1+0x9c4)[0x7fe4329dc8a4]
/home/mario/Documents/lean/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(l_EIO_toBaseIO___rarg+0x13)[0x7fe4300b3e23]
/home/mario/Documents/lean/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(lean_apply_1+0xa18)[0x7fe4329dc8f8]
/home/mario/Documents/lean/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(+0x30f1d45)[0x7fe4329f7d45]
/home/mario/Documents/lean/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(lean_apply_1+0xa18)[0x7fe4329dc8f8]
/home/mario/Documents/lean/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(+0x30d5314)[0x7fe4329db314]
/home/mario/Documents/lean/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(+0x30d59ff)[0x7fe4329db9ff]
/home/mario/Documents/lean/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(+0x30c95b3)[0x7fe4329cf5b3]
/lib/x86_64-linux-gnu/libc.so.6(+0x94b43)[0x7fe42f74cb43]
/lib/x86_64-linux-gnu/libc.so.6(+0x126a00)[0x7fe42f7dea00]
PANIC at Lean.Server.Snapshots.Snapshot.infoTree Lean.Server.Snapshots:68:2: assertion violation: s.cmdState.infoState.trees.size == 1
  
backtrace:
/home/mario/Documents/lean/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(lean_panic_fn+0x10f)[0x7fe4329d1e2f]
/home/mario/Documents/lean/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(l_Array_mapMUnsafe_map___at_Lean_Server_FileWorker_handleDocumentHighlight___spec__1+0x92)[0x7fe4326b5b12]
/home/mario/Documents/lean/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(l___private_Lean_Server_FileWorker_0__Lean_Server_FileWorker_publishIleanInfo+0x36)[0x7fe4326eeb06]
/home/mario/Documents/lean/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(l___private_Lean_Server_FileWorker_0__Lean_Server_FileWorker_nextCmdSnap+0x59f)[0x7fe4326f0f8f]
/home/mario/Documents/lean/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(lean_apply_2+0xa64)[0x7fe4329de7a4]
/home/mario/Documents/lean/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(l_IO_AsyncList_unfoldAsync_step___rarg+0x33)[0x7fe43272a343]
/home/mario/Documents/lean/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(lean_apply_1+0x9c4)[0x7fe4329dc8a4]
/home/mario/Documents/lean/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(l_EIO_toBaseIO___rarg+0x13)[0x7fe4300b3e23]
/home/mario/Documents/lean/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(lean_apply_1+0xa18)[0x7fe4329dc8f8]
/home/mario/Documents/lean/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(+0x30f1d45)[0x7fe4329f7d45]
/home/mario/Documents/lean/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(lean_apply_1+0xa18)[0x7fe4329dc8f8]
/home/mario/Documents/lean/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(+0x30d5314)[0x7fe4329db314]
/home/mario/Documents/lean/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(+0x30d59ff)[0x7fe4329db9ff]
/home/mario/Documents/lean/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(+0x30c95b3)[0x7fe4329cf5b3]
/lib/x86_64-linux-gnu/libc.so.6(+0x94b43)[0x7fe42f74cb43]
/lib/x86_64-linux-gnu/libc.so.6(+0x126a00)[0x7fe42f7dea00]
PANIC at Lean.Elab.InfoTree.visitM.go Lean.Server.InfoUtils:36:21: unexpected context-free info tree node
backtrace:
/home/mario/Documents/lean/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(lean_panic_fn+0x10f)[0x7fe4329d1e2f]
/home/mario/Documents/lean/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(l_panic___at_Lean_Server_findReferences___spec__4+0x17)[0x7fe43283c7d7]
/home/mario/Documents/lean/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(l_Lean_Elab_InfoTree_visitM_x27___at_Lean_Server_findReferences___spec__1+0x5d)[0x7fe43283d60d]
/home/mario/Documents/lean/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(l_Array_forInUnsafe_loop___at_Lean_Server_findReferences___spec__6+0xc9)[0x7fe43283de59]
/home/mario/Documents/lean/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(l_Lean_Server_findReferences+0x2c)[0x7fe43283dfbc]
/home/mario/Documents/lean/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(l_Lean_Server_findModuleRefs+0x1b)[0x7fe4328488bb]
/home/mario/Documents/lean/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(l___private_Lean_Server_FileWorker_0__Lean_Server_FileWorker_publishIleanInfo+0x5e)[0x7fe4326eeb2e]
/home/mario/Documents/lean/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(l___private_Lean_Server_FileWorker_0__Lean_Server_FileWorker_nextCmdSnap+0x59f)[0x7fe4326f0f8f]
/home/mario/Documents/lean/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(lean_apply_2+0xa64)[0x7fe4329de7a4]
/home/mario/Documents/lean/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(l_IO_AsyncList_unfoldAsync_step___rarg+0x33)[0x7fe43272a343]
/home/mario/Documents/lean/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(lean_apply_1+0x9c4)[0x7fe4329dc8a4]
/home/mario/Documents/lean/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(l_EIO_toBaseIO___rarg+0x13)[0x7fe4300b3e23]
/home/mario/Documents/lean/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(lean_apply_1+0xa18)[0x7fe4329dc8f8]
/home/mario/Documents/lean/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(+0x30f1d45)[0x7fe4329f7d45]
/home/mario/Documents/lean/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(lean_apply_1+0xa18)[0x7fe4329dc8f8]
/home/mario/Documents/lean/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(+0x30d5314)[0x7fe4329db314]
/home/mario/Documents/lean/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(+0x30d59ff)[0x7fe4329db9ff]
/home/mario/Documents/lean/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(+0x30c95b3)[0x7fe4329cf5b3]
/lib/x86_64-linux-gnu/libc.so.6(+0x94b43)[0x7fe42f74cb43]
/lib/x86_64-linux-gnu/libc.so.6(+0x126a00)[0x7fe42f7dea00]
PANIC at Lean.Elab.InfoTree.visitM.go Lean.Server.InfoUtils:36:21: unexpected context-free info tree node
backtrace:
/home/mario/Documents/lean/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(lean_panic_fn+0x10f)[0x7fe4329d1e2f]
/home/mario/Documents/lean/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(l_panic___at_Lean_Server_findReferences___spec__4+0x17)[0x7fe43283c7d7]
/home/mario/Documents/lean/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(l_Lean_Elab_InfoTree_visitM_x27___at_Lean_Server_findReferences___spec__1+0x5d)[0x7fe43283d60d]
/home/mario/Documents/lean/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(l_Array_forInUnsafe_loop___at_Lean_Server_findReferences___spec__6+0xc9)[0x7fe43283de59]
/home/mario/Documents/lean/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(l_Lean_Server_findReferences+0x2c)[0x7fe43283dfbc]
/home/mario/Documents/lean/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(l_Lean_Server_findModuleRefs+0x1b)[0x7fe4328488bb]
/home/mario/Documents/lean/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(l___private_Lean_Server_FileWorker_0__Lean_Server_FileWorker_publishIleanInfo+0x5e)[0x7fe4326eeb2e]
/home/mario/Documents/lean/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(l___private_Lean_Server_FileWorker_0__Lean_Server_FileWorker_nextCmdSnap+0x59f)[0x7fe4326f0f8f]
/home/mario/Documents/lean/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(lean_apply_2+0xa64)[0x7fe4329de7a4]
/home/mario/Documents/lean/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(l_IO_AsyncList_unfoldAsync_step___rarg+0x33)[0x7fe43272a343]
/home/mario/Documents/lean/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(lean_apply_1+0x9c4)[0x7fe4329dc8a4]
/home/mario/Documents/lean/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(l_EIO_toBaseIO___rarg+0x13)[0x7fe4300b3e23]
/home/mario/Documents/lean/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(lean_apply_1+0xa18)[0x7fe4329dc8f8]
/home/mario/Documents/lean/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(+0x30f1d45)[0x7fe4329f7d45]
/home/mario/Documents/lean/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(lean_apply_1+0xa18)[0x7fe4329dc8f8]
/home/mario/Documents/lean/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(+0x30d5314)[0x7fe4329db314]
/home/mario/Documents/lean/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(+0x30d59ff)[0x7fe4329db9ff]
/home/mario/Documents/lean/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(+0x30c95b3)[0x7fe4329cf5b3]
/lib/x86_64-linux-gnu/libc.so.6(+0x94b43)[0x7fe42f74cb43]
/lib/x86_64-linux-gnu/libc.so.6(+0x126a00)[0x7fe42f7dea00]
PANIC at Lean.Elab.InfoTree.visitM.go Lean.Server.InfoUtils:36:21: unexpected context-free info tree node
backtrace:
/home/mario/Documents/lean/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(lean_panic_fn+0x10f)[0x7fe4329d1e2f]
/home/mario/Documents/lean/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(l_panic___at_Lean_Server_combineFvars_buildIdMap___spec__8+0x17)[0x7fe43283fe37]
/home/mario/Documents/lean/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(l_Lean_Elab_InfoTree_visitM_x27___at_Lean_Server_combineFvars_buildIdMap___spec__5+0x5d)[0x7fe432840c0d]
/home/mario/Documents/lean/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(l_Array_foldlMUnsafe_fold___at_Lean_Server_combineFvars_buildIdMap___spec__10+0x74)[0x7fe432840fb4]
/home/mario/Documents/lean/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(l_Lean_Server_combineFvars_buildIdMap+0xad)[0x7fe4328411ad]
/home/mario/Documents/lean/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(l_Lean_Server_combineFvars+0x4b)[0x7fe432842fab]
/home/mario/Documents/lean/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(l_Lean_Server_findModuleRefs+0x29)[0x7fe4328488c9]
/home/mario/Documents/lean/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(l___private_Lean_Server_FileWorker_0__Lean_Server_FileWorker_publishIleanInfo+0x5e)[0x7fe4326eeb2e]
/home/mario/Documents/lean/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(l___private_Lean_Server_FileWorker_0__Lean_Server_FileWorker_nextCmdSnap+0x59f)[0x7fe4326f0f8f]
/home/mario/Documents/lean/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(lean_apply_2+0xa64)[0x7fe4329de7a4]
/home/mario/Documents/lean/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(l_IO_AsyncList_unfoldAsync_step___rarg+0x33)[0x7fe43272a343]
/home/mario/Documents/lean/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(lean_apply_1+0x9c4)[0x7fe4329dc8a4]
/home/mario/Documents/lean/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(l_EIO_toBaseIO___rarg+0x13)[0x7fe4300b3e23]
/home/mario/Documents/lean/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(lean_apply_1+0xa18)[0x7fe4329dc8f8]
/home/mario/Documents/lean/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(+0x30f1d45)[0x7fe4329f7d45]
/home/mario/Documents/lean/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(lean_apply_1+0xa18)[0x7fe4329dc8f8]
/home/mario/Documents/lean/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(+0x30d5314)[0x7fe4329db314]
/home/mario/Documents/lean/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(+0x30d59ff)[0x7fe4329db9ff]
/home/mario/Documents/lean/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(+0x30c95b3)[0x7fe4329cf5b3]
/lib/x86_64-linux-gnu/libc.so.6(+0x94b43)[0x7fe42f74cb43]
/lib/x86_64-linux-gnu/libc.so.6(+0x126a00)[0x7fe42f7dea00]
PANIC at Lean.Elab.InfoTree.visitM.go Lean.Server.InfoUtils:36:21: unexpected context-free info tree node
backtrace:
/home/mario/Documents/lean/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(lean_panic_fn+0x10f)[0x7fe4329d1e2f]
/home/mario/Documents/lean/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(l_panic___at_Lean_Server_combineFvars_buildIdMap___spec__8+0x17)[0x7fe43283fe37]
/home/mario/Documents/lean/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(l_Lean_Elab_InfoTree_visitM_x27___at_Lean_Server_combineFvars_buildIdMap___spec__5+0x5d)[0x7fe432840c0d]
/home/mario/Documents/lean/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(l_Array_foldlMUnsafe_fold___at_Lean_Server_combineFvars_buildIdMap___spec__10+0x74)[0x7fe432840fb4]
/home/mario/Documents/lean/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(l_Lean_Server_combineFvars_buildIdMap+0xad)[0x7fe4328411ad]
/home/mario/Documents/lean/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(l_Lean_Server_combineFvars+0x4b)[0x7fe432842fab]
/home/mario/Documents/lean/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(l_Lean_Server_findModuleRefs+0x29)[0x7fe4328488c9]
/home/mario/Documents/lean/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(l___private_Lean_Server_FileWorker_0__Lean_Server_FileWorker_publishIleanInfo+0x5e)[0x7fe4326eeb2e]
/home/mario/Documents/lean/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(l___private_Lean_Server_FileWorker_0__Lean_Server_FileWorker_nextCmdSnap+0x59f)[0x7fe4326f0f8f]
/home/mario/Documents/lean/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(lean_apply_2+0xa64)[0x7fe4329de7a4]
/home/mario/Documents/lean/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(l_IO_AsyncList_unfoldAsync_step___rarg+0x33)[0x7fe43272a343]
/home/mario/Documents/lean/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(lean_apply_1+0x9c4)[0x7fe4329dc8a4]
/home/mario/Documents/lean/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(l_EIO_toBaseIO___rarg+0x13)[0x7fe4300b3e23]
/home/mario/Documents/lean/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(lean_apply_1+0xa18)[0x7fe4329dc8f8]
/home/mario/Documents/lean/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(+0x30f1d45)[0x7fe4329f7d45]
/home/mario/Documents/lean/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(lean_apply_1+0xa18)[0x7fe4329dc8f8]
/home/mario/Documents/lean/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(+0x30d5314)[0x7fe4329db314]
/home/mario/Documents/lean/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(+0x30d59ff)[0x7fe4329db9ff]
/home/mario/Documents/lean/lean4/build/release/stage1/bin/../lib/lean/libleanshared.so(+0x30c95b3)[0x7fe4329cf5b3]
/lib/x86_64-linux-gnu/libc.so.6(+0x94b43)[0x7fe42f74cb43]
/lib/x86_64-linux-gnu/libc.so.6(+0x126a00)[0x7fe42f7dea00]

digama0 avatar Aug 27 '22 04:08 digama0

Hmm, I can't reproduce that. We already have the test https://github.com/leanprover/lean4/blob/master/tests/lean/interactive/unterminatedDocComment.lean.

Kha avatar Aug 27 '22 08:08 Kha

@digama0 Is it reproducible 100% of the time?

leodemoura avatar Aug 28 '22 03:08 leodemoura

I think I might have minimized too much. Here's another example:

1525.lean:

structure Foo where
  /--/-/

1525.lean.produced.out:

PANIC at Lean.Server.Snapshots.Snapshot.infoTree Lean.Server.Snapshots:68:2: assertion violation: s.cmdState.infoState.trees.size == 1
  
PANIC at Lean.Elab.InfoTree.visitM.go Lean.Server.InfoUtils:36:21: unexpected context-free info tree node
PANIC at Lean.Elab.InfoTree.visitM.go Lean.Server.InfoUtils:36:21: unexpected context-free info tree node
PANIC at Lean.Server.Snapshots.Snapshot.infoTree Lean.Server.Snapshots:68:2: assertion violation: s.cmdState.infoState.trees.size == 1
  
PANIC at Lean.Elab.InfoTree.visitM.go Lean.Server.InfoUtils:36:21: unexpected context-free info tree node
PANIC at Lean.Elab.InfoTree.visitM.go Lean.Server.InfoUtils:36:21: unexpected context-free info tree node
PANIC at Lean.Server.Snapshots.Snapshot.infoTree Lean.Server.Snapshots:68:2: assertion violation: s.cmdState.infoState.trees.size == 1
  
PANIC at Lean.Server.Snapshots.Snapshot.infoTree Lean.Server.Snapshots:68:2: assertion violation: s.cmdState.infoState.trees.size == 1
  
PANIC at Lean.Elab.InfoTree.visitM.go Lean.Server.InfoUtils:36:21: unexpected context-free info tree node
PANIC at Lean.Elab.InfoTree.visitM.go Lean.Server.InfoUtils:36:21: unexpected context-free info tree node
PANIC at Lean.Elab.InfoTree.visitM.go Lean.Server.InfoUtils:36:21: unexpected context-free info tree node
PANIC at Lean.Elab.InfoTree.visitM.go Lean.Server.InfoUtils:36:21: unexpected context-free info tree node

digama0 avatar Aug 28 '22 03:08 digama0

I can reproduce this one.

leodemoura avatar Aug 29 '22 07:08 leodemoura