search

leanprover-community / mathport

Mathport is a tool for porting Lean3 projects to Lean4
Apache License 2.0
40 stars 15 forks source link

mathport sometimes panics #220

Open rwbarton opened 1 year ago

rwbarton commented 1 year ago

When I run make port-mathbin locally, there are 5 panics. It's not clear to me what files are being processed at the time. The failure is not propagated to the main mathport process. So likely this has been going on for some time. Really there are two issues:

PANIC at Lean.Name.getString! Lean.Data.Name:22:15: unreachable code has been reached
backtrace:
/home/rb1083/math/lean/mathport/build/bin/mathport(lean_panic_fn+0x9e)[0x55d572e1900e]
/home/rb1083/math/lean/mathport/build/bin/mathport(l_Mathport_Rename_renameField_x3f+0x1ac)[0x55d56ea4ae2c]
/home/rb1083/math/lean/mathport/build/bin/mathport(l_Mathport_Translate_renameField+0x78)[0x55d56fcb9878]
/home/rb1083/math/lean/mathport/build/bin/mathport(l_Mathport_Translate_mkIdentF+0x14)[0x55d56fcba4d4]
/home/rb1083/math/lean/mathport/build/bin/mathport(l_Mathport_Translate_trExpr_x27+0x2c86)[0x55d56fd21196]
/home/rb1083/math/lean/mathport/build/bin/mathport(lean_apply_4+0x6e8)[0x55d572e26088]
/home/rb1083/math/lean/mathport/build/bin/mathport(l_Mathport_Translate_trExprUnspanned___boxed+0x5a)[0x55d56fcb860a]
/home/rb1083/math/lean/mathport/build/bin/mathport(lean_apply_5+0x363)[0x55d572e26ac3]
/home/rb1083/math/lean/mathport/build/bin/mathport(l_Mathport_Translate_withSpanS___rarg+0x1c)[0x55d56fcb7f8c]
/home/rb1083/math/lean/mathport/build/bin/mathport(l_Mathport_Translate_spanningS___rarg+0x93)[0x55d56fcb8413]
/home/rb1083/math/lean/mathport/build/bin/mathport(l_Mathport_Translate_trAppArgs___rarg+0x286)[0x55d56fce4866]
/home/rb1083/math/lean/mathport/build/bin/mathport(l_Mathport_Translate_trAppArgs___rarg+0x153)[0x55d56fce4733]
/home/rb1083/math/lean/mathport/build/bin/mathport(l_Mathport_Translate_trAppArgs___rarg+0x153)[0x55d56fce4733]
/home/rb1083/math/lean/mathport/build/bin/mathport(l_Mathport_Translate_trAppArgs___rarg+0x153)[0x55d56fce4733]
/home/rb1083/math/lean/mathport/build/bin/mathport(l_Mathport_Translate_trAppArgs___rarg+0x153)[0x55d56fce4733]
/home/rb1083/math/lean/mathport/build/bin/mathport(l_Mathport_Translate_trAppArgs___rarg+0x153)[0x55d56fce4733]
/home/rb1083/math/lean/mathport/build/bin/mathport(l_Mathport_Translate_trAppArgs___rarg+0x153)[0x55d56fce4733]
/home/rb1083/math/lean/mathport/build/bin/mathport(l_Mathport_Translate_trExpr_x27+0xd4f)[0x55d56fd1f25f]
/home/rb1083/math/lean/mathport/build/bin/mathport(lean_apply_4+0x6e8)[0x55d572e26088]
/home/rb1083/math/lean/mathport/build/bin/mathport(l_Mathport_Translate_trDecl+0x221b)[0x55d56fe2f2bb]
/home/rb1083/math/lean/mathport/build/bin/mathport(l_Mathport_Translate_trCommand_x27+0xc05)[0x55d56fe733a5]
/home/rb1083/math/lean/mathport/build/bin/mathport(lean_apply_4+0x6e8)[0x55d572e26088]
/home/rb1083/math/lean/mathport/build/bin/mathport(l_Mathport_Translate_trCommandUnspanned___boxed+0x5a)[0x55d56fcb88ea]
/home/rb1083/math/lean/mathport/build/bin/mathport(lean_apply_5+0x363)[0x55d572e26ac3]
/home/rb1083/math/lean/mathport/build/bin/mathport(l_Mathport_Translate_spanning___rarg+0x93)[0x55d56fcb82d3]
/home/rb1083/math/lean/mathport/build/bin/mathport(l_Array_foldlMUnsafe_fold___at_Mathport_Translate_AST3toData4___spec__2+0x1e2)[0x55d5700fc422]
/home/rb1083/math/lean/mathport/build/bin/mathport(l_Mathport_Translate_AST3toData4+0xeab)[0x55d57010399b]
/home/rb1083/math/lean/mathport/build/bin/mathport(l_Mathport_Translate_AST3toData4___boxed+0x18)[0x55d570104aa8]
/home/rb1083/math/lean/mathport/build/bin/mathport(lean_apply_5+0x3a0)[0x55d572e26b00]
/home/rb1083/math/lean/mathport/build/bin/mathport(lean_apply_6+0x3a5)[0x55d572e27785]
/home/rb1083/math/lean/mathport/build/bin/mathport(l_ReaderT_bind___at_Mathport_Translate_trTactic_x27___spec__3___rarg+0x213)[0x55d5700c5c73]
/home/rb1083/math/lean/mathport/build/bin/mathport(lean_apply_5+0x3a0)[0x55d572e26b00]
/home/rb1083/math/lean/mathport/build/bin/mathport(l_Mathport_AST3toData4+0x160)[0x55d570104c40]
/home/rb1083/math/lean/mathport/build/bin/mathport(l_Mathport_synport1+0x2b9)[0x55d5701076d9]
/home/rb1083/math/lean/mathport/build/bin/mathport(l_Mathport_mathport1___lambda__1+0x1e2)[0x55d570471562]
/home/rb1083/math/lean/mathport/build/bin/mathport(lean_apply_3+0x393)[0x55d572e25023]
/home/rb1083/math/lean/mathport/build/bin/mathport(l_Lean_Elab_Command_CommandElabM_toIO___rarg+0x92)[0x55d56ea3c1b2]
/home/rb1083/math/lean/mathport/build/bin/mathport(l_Mathport_mathport1___lambda__2+0x15e)[0x55d570471e3e]
/home/rb1083/math/lean/mathport/build/bin/mathport(l_Mathport_mathport1___lambda__2___boxed+0x29)[0x55d5704725d9]
/home/rb1083/math/lean/mathport/build/bin/mathport(lean_apply_2+0x3a2)[0x55d572e23f42]
/home/rb1083/math/lean/mathport/build/bin/mathport(l_Lean_withImportModules___rarg+0x141)[0x55d571b1d8d1]
/home/rb1083/math/lean/mathport/build/bin/mathport(l_Mathport_mathport1___lambda__3+0x12e)[0x55d5704720ee]
/home/rb1083/math/lean/mathport/build/bin/mathport(l_Mathport_mathport1+0x6ef)[0x55d570472cff]
/home/rb1083/math/lean/mathport/build/bin/mathport(+0x1275853)[0x55d56ea28853]
/lib/x86_64-linux-gnu/libc.so.6(__libc_start_main+0xf3)[0x7fea0d0aa083]
/home/rb1083/math/lean/mathport/build/bin/mathport(_start+0x2e)[0x55d56ea21fae]