Skip to content

mathport sometimes panics #220

@rwbarton

Description

@rwbarton

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]

Metadata

Metadata

Assignees

No one assigned

    Labels

    No labels
    No labels

    Type

    No type

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions