LeanInk (or Lean?) bug

Stream: lean4

[Henrik Böving]

While writing integration for LeanInk with DocGen4 during my first test run I noticed that when processing a particular (very unsuspicious) file in Mathlib4 LeanInk will simply hang (maybe its just doing some infinitely long processing in the background, who knows. I does succeed in processing quite more complex files including tactic ones but this one seems to break it. I have an MWE here: https://github.com/hargoniX/lean-ink-bug you can compile it and run the binary in the root of a current Mathlib4 master checkout.

I suspect it might be a Lean bug or a bug in the way LeanInk tries to communicate with Lean since a gdb run shows that it is stuck quite deep in the elaboration stack.

[Henrik Böving]

I managed to reduce it to:

import Mathlib.Init.SetNotation

inductive rel : Option Unit → Option Unit → Prop
| ctor0 : rel none none

This file, botht he import and the rel inductive with this constructor (there used to be others that i deleted) are relevant, if either is deleted the above binary will run through. Furthermore if the relation is changed to just a predicate it does not hang, it will also not hang if one of the none is explicitly typed out as Option.none.

[Henrik Böving]

This is eh...confusing to me to say the least, does anyone have an idea? Maybe @Niklas Bülow or @Sebastian Ullrich ?

[Sebastian Ullrich]

Not immediately, I'd have to take a look myself

[Sebastian Ullrich]

Could you post the stack trace?

[Henrik Böving]

There is not exactly a stack trace i just interrupt the GDB whenever (since it seems to hang) and bt which looks like this:

#0  0x0000000000c1c35f in l_Std_HashMapImp_find_x3f___at_Lean_MetavarContext_instantiateExprMVars___spec__1 ()
#1  0x00000000015c19ca in l_Lean_MetavarContext_instantiateExprMVars___at_Lean_Meta_instantiateMVars___spec__1 ()
#2  0x00000000015c2153 in l_Lean_MetavarContext_instantiateExprMVars___at_Lean_Meta_instantiateMVars___spec__1 ()
#3  0x00000000015c4dca in l_Lean_Meta_instantiateMVars ()
#4  0x0000000001c0c64a in l_Lean_Meta_collectMVars ()
#5  0x0000000001c0cf42 in l_Lean_Meta_getMVars ()
#6  0x000000000134b9b0 in l_Lean_Elab_Term_collectUnassignedMVars_go ()
#7  0x000000000134c8ab in l_Lean_Elab_Term_collectUnassignedMVars ()
#8  0x00000000024aa0f8 in l_List_mapM___at___private_Lean_Elab_Inductive_0__Lean_Elab_Command_elabCtors___spec__2___lambda__4 ()
#9  0x0000000002e018cc in lean_apply_8 ()
#10 0x00000000024a6840 in l___private_Lean_Elab_Inductive_0__Lean_Elab_Command_elabCtors_elabCtorType___lambda__4 ()
#11 0x00000000024a7994 in l___private_Lean_Elab_Inductive_0__Lean_Elab_Command_elabCtors_elabCtorType ()
#12 0x00000000024ab064 in l_List_mapM___at___private_Lean_Elab_Inductive_0__Lean_Elab_Command_elabCtors___spec__2___lambda__5 ()
#13 0x0000000002e01c6e in lean_apply_8 ()
#14 0x0000000002e00bb7 in lean_apply_7 ()
#15 0x000000000136b572 in l_Lean_Elab_Term_universeConstraintsCheckpoint___rarg ()
#16 0x0000000001442f9c in l_Lean_Elab_Term_elabBinders___rarg ()
#17 0x0000000002e00e35 in lean_apply_7 ()
#18 0x0000000001349479 in l_Lean_Elab_Term_withAutoBoundImplicit_loop___rarg ()
#19 0x0000000001349184 in l_Lean_Elab_Term_withAutoBoundImplicit_loop___rarg___lambda__1 ()
#20 0x0000000002e0186b in lean_apply_8 ()
#21 0x0000000002dffefa in lean_apply_6 ()
#22 0x00000000015e3f46 in l___private_Lean_Meta_Basic_0__Lean_Meta_withNewFVar___rarg ()
#23 0x00000000015e4417 in l___private_Lean_Meta_Basic_0__Lean_Meta_withLocalDeclImp___rarg ()
#24 0x000000000132ef28 in l_Lean_Meta_withLocalDecl___at___private_Lean_Elab_Term_0__Lean_Elab_Term_elabImplicitLambda_loop___spec__1___rarg ()
#25 0x0000000001349a5a in l_Lean_Elab_Term_withAutoBoundImplicit_loop___rarg ()
#26 0x000000000134a498 in l_Lean_Elab_Term_withAutoBoundImplicit___rarg ()
#27 0x00000000024ab68a in l_List_mapM___at___private_Lean_Elab_Inductive_0__Lean_Elab_Command_elabCtors___spec__2 ()
#28 0x00000000024ad374 in l___private_Lean_Elab_Inductive_0__Lean_Elab_Command_elabCtors ()
#29 0x0000000002dff1bf in lean_apply_5 ()
#30 0x00000000024a2e6c in l_Lean_Meta_withNewBinderInfos___at___private_Lean_Elab_Inductive_0__Lean_Elab_Command_withExplicitToImplicit___spec__2___rarg ()
#31 0x00000000024a32d7 in l___private_Lean_Elab_Inductive_0__Lean_Elab_Command_withExplicitToImplicit___rarg ()
#32 0x00000000024f18d8 in l_Std_Range_forIn_loop___at___private_Lean_Elab_Inductive_0__Lean_Elab_Command_mkInductiveDecl___spec__1 ()
#33 0x00000000024fd5e9 in l___private_Lean_Elab_Inductive_0__Lean_Elab_Command_mkInductiveDecl___lambda__4 ()
#34 0x00000000024ff634 in l___private_Lean_Elab_Inductive_0__Lean_Elab_Command_mkInductiveDecl___lambda__5 ()
#35 0x0000000002e025d7 in lean_apply_9 ()
#36 0x000000000249c669 in l___private_Lean_Elab_Inductive_0__Lean_Elab_Command_withInductiveLocalDecls_loop___rarg ()
#37 0x000000000249c444 in l___private_Lean_Elab_Inductive_0__Lean_Elab_Command_withInductiveLocalDecls_loop___rarg___lambda__1 ()
#38 0x0000000002e01948 in lean_apply_8 ()
#39 0x0000000002dffefa in lean_apply_6 ()
#40 0x00000000015e3f46 in l___private_Lean_Meta_Basic_0__Lean_Meta_withNewFVar___rarg ()
#41 0x00000000015e4417 in l___private_Lean_Meta_Basic_0__Lean_Meta_withLocalDeclImp___rarg ()
#42 0x000000000132ef28 in l_Lean_Meta_withLocalDecl___at___private_Lean_Elab_Term_0__Lean_Elab_Term_elabImplicitLambda_loop___spec__1___rarg ()
#43 0x000000000249c5f3 in l___private_Lean_Elab_Inductive_0__Lean_Elab_Command_withInductiveLocalDecls_loop___rarg ()
#44 0x000000000249d2ef in l___private_Lean_Elab_Inductive_0__Lean_Elab_Command_withInductiveLocalDecls___rarg___lambda__1 ()
#45 0x000000000249dccc in l___private_Lean_Elab_Inductive_0__Lean_Elab_Command_withInductiveLocalDecls___rarg___lambda__1___boxed ()
#46 0x0000000002dff1bf in lean_apply_5 ()
#47 0x000000000145f09f in l_Lean_Meta_withLCtx___at___private_Lean_Elab_Binders_0__Lean_Elab_Term_FunBinders_elabFunBinderViews___spec__3___rarg ()
#48 0x000000000249d90f in l___private_Lean_Elab_Inductive_0__Lean_Elab_Command_withInductiveLocalDecls___rarg ()
#49 0x00000000024ffe4b in l___private_Lean_Elab_Inductive_0__Lean_Elab_Command_mkInductiveDecl___lambda__7 ()
#50 0x0000000002e00c08 in lean_apply_7 ()
#51 0x00000000012eab39 in l_Lean_Elab_Term_withLevelNames___rarg ()
#52 0x0000000002500cdc in l___private_Lean_Elab_Inductive_0__Lean_Elab_Command_mkInductiveDecl___lambda__8 ()
#53 0x0000000002e00bb7 in lean_apply_7 ()
#54 0x0000000002501296 in l___private_Lean_Elab_Inductive_0__Lean_Elab_Command_mkInductiveDecl ()
#55 0x0000000002504e75 in l_Lean_Elab_Command_elabInductiveViews___lambda__1 ()
#56 0x0000000002506e0e in l_Lean_Elab_Command_elabInductiveViews___lambda__1___boxed ()
#57 0x0000000002e00c08 in lean_apply_7 ()
#58 0x000000000134a723 in l_Lean_Elab_Term_withoutAutoBoundImplicit___rarg ()
#59 0x0000000002507d30 in l_Lean_Elab_Command_elabInductiveViews___lambda__2___boxed ()
#60 0x0000000002e02563 in lean_apply_9 ()
#61 0x000000000134ec4c in l_Lean_Elab_Term_addAutoBoundImplicits_x27___rarg ()
#62 0x0000000002507691 in l_Lean_Elab_Command_elabInductiveViews___lambda__3 ()
#63 0x000000000250a09c in l_Lean_Elab_Command_elabInductiveViews___lambda__3___boxed ()
#64 0x0000000002e01b62 in lean_apply_8 ()
#65 0x0000000002e00bb7 in lean_apply_7 ()
#66 0x000000000136b572 in l_Lean_Elab_Term_universeConstraintsCheckpoint___rarg ()
#67 0x0000000001442f9c in l_Lean_Elab_Term_elabBinders___rarg ()
#68 0x0000000002e00e35 in lean_apply_7 ()
#69 0x0000000001349479 in l_Lean_Elab_Term_withAutoBoundImplicit_loop___rarg ()
#70 0x000000000134a498 in l_Lean_Elab_Term_withAutoBoundImplicit___rarg ()
#71 0x0000000002e00b6f in lean_apply_7 ()
#72 0x00000000013e37d3 in l_Lean_Elab_withSaveInfoContext___at_Lean_Elab_Command_liftTermElabM___spec__1___rarg ()
#73 0x00000000013e5219 in l_Lean_Elab_Command_liftTermElabM___rarg___lambda__1 ()
#74 0x0000000002e00b6f in lean_apply_7 ()
#75 0x000000000135b04e in l_Lean_Elab_Term_TermElabM_run___rarg ()
#76 0x00000000013e57ed in l_Lean_Elab_Command_liftTermElabM___rarg ()
#77 0x0000000002509925 in l_Lean_Elab_Command_elabInductiveViews ()
#78 0x0000000002dfd5ca in lean_apply_3 ()
#79 0x00000000013c8ac2 in l_Lean_Elab_withInfoTreeContext___at___private_Lean_Elab_Command_0__Lean_Elab_Command_elabCommandUsing___spec__2 ()
#80 0x00000000013ca703 in l___private_Lean_Elab_Command_0__Lean_Elab_Command_elabCommandUsing ()
#81 0x0000000002dfd602 in lean_apply_3 ()
#82 0x0000000002dfd5e4 in lean_apply_3 ()
#83 0x00000000013cc496 in l_Lean_Elab_Command_withLogging ()
#84 0x00000000013dc8eb in l_Lean_Elab_Command_elabCommandTopLevel ()
#85 0x00000000012c5938 in l_Lean_Elab_Frontend_elabCommandAtFrontend ()
#86 0x00000000012c6190 in l_Lean_Elab_Frontend_elabCommandAtFrontend___boxed ()
#87 0x0000000002dfb632 in lean_apply_1 ()
#88 0x0000000001e7fa8e in l_Lean_profileitIOUnsafe___rarg___lambda__1 ()
#89 0x0000000001e7fc9c in l_Lean_profileitIOUnsafe___rarg___lambda__1___boxed ()
#90 0x0000000002dfb606 in lean_apply_1 ()
#91 0x0000000000b4c6e3 in lean_profileit ()
#92 0x0000000001e7fbb4 in l_Lean_profileitIOUnsafe___rarg ()
#93 0x00000000012c8b2e in l_Lean_Elab_Frontend_processCommand ()
#94 0x00000000012c96dc in l_Lean_Elab_Frontend_processCommands ()
#95 0x00000000012c9b02 in l_Lean_Elab_IO_processCommands ()
#96 0x0000000000ad3fc3 in l_LeanInk_Analysis_analyzeInput ()
#97 0x0000000000a86d93 in _lean_main ()
#98 0x0000000000a87145 in main ()

[Henrik Böving]

Hmmm, if I provide LeanInk with the lakefile.lean of the project it handles this file well, then however I start getting the same errors @Xubai Wang was observing in his PR like:

libc++abi: terminating with uncaught exception of type lean::exception: cannot evaluate `[init]` declaration 'Mathlib.Tactic.Ext.extExtension' in the same module

where the module that is being processed right now is Mathlib.Logic.Function.Basic