mathport icon indicating copy to clipboard operation
mathport copied to clipboard

mathport sometimes panics

Open rwbarton opened this issue 3 years ago • 0 comments

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:

  • Panics in porting individual files are not caught/reported and it's hard to find out what files are panicking.
  • There seems to be some actual bug in Mathport.Rename.renameField?.
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]

rwbarton avatar Jan 19 '23 14:01 rwbarton