segfault in mkParserOfConstantUnsafe

Stream: lean4

[Daniel Selsam]

I am probably doing something stupid, but I am trying to import modules dynamically (including one generated by binport) and hitting the following segfault:

Program received signal SIGSEGV, Segmentation fault.
0x00005555569783b5 in l_IO_ofExcept___at_Lean_Parser_mkParserOfConstantUnsafe___spec__2 ()
(gdb) bt
#0  0x00005555569783b5 in l_IO_ofExcept___at_Lean_Parser_mkParserOfConstantUnsafe___spec__2 ()
#1  0x0000555556979458 in l_Lean_Parser_mkParserOfConstantUnsafe___rarg ()
#2  0x000055555697f247 in l___private_Lean_Parser_Extension_0__Lean_Parser_ParserExtension_OLeanEntry_toEntry ()
#3  0x000055555846bc4b in lean_apply_4 ()
#4  0x0000555557699bed in l_Array_forInUnsafe_loop___at_Lean_ScopedEnvExtension_addImportedFn___spec__2___rarg ()
#5  0x000055555769acc8 in l_Array_forInUnsafe_loop___at_Lean_ScopedEnvExtension_addImportedFn___spec__3___rarg ()
#6  0x000055555769b777 in l_Lean_ScopedEnvExtension_addImportedFn___rarg ()
#7  0x000055555769bc51 in l_Lean_ScopedEnvExtension_addImportedFn___rarg___boxed ()
#8  0x000055555846a236 in lean_apply_3 ()
#9  0x000055555768933d in l___private_Lean_Environment_0__Lean_finalizePersistentExtensions_loop ()
#10 0x000055555768dc41 in l_Lean_importModules___lambda__3 ()
#11 0x0000555558468e30 in lean_apply_2 ()
#12 0x0000555558466cd7 in lean_apply_1 ()
#13 0x00005555576a862e in l_Lean_withImporting___rarg ()

A self-contained repro would take some work, so if anyone has any immediate hypotheses about what the issue might be, that would be helpful. Thanks.

[Daniel Selsam]

Clarification: it is easy to provide a recipe to reproduce that involves running mathport to generate an .olean.

[Daniel Selsam]

Update: I think I isolated the problem, working on a repro...

[Daniel Selsam]

It is sensitive to almost every weird detail in that directory. Also, the repro suggests a workaround for the issue, so I am not blocked on this anymore.