Panic in Lean.MapDeclarationExtension.insert #10613
Description
Prerequisites
Please put an X between the brackets as you perform the following steps:
- Check that your issue is not already filed:
https://github.com/leanprover/lean4/issues - Reduce the issue to a minimal, self-contained, reproducible test case.
Avoid dependencies to Mathlib or Batteries. - Test your test case against the latest nightly release, for example on
https://live.lean-lang.org/#project=lean-nightly
(You can also use the settings there to switch to “Lean nightly”)
Description
The build of this commit fails in Init.Data.List.ofFn on a grind = annotation with the following error message:
PANIC at Lean.MapDeclarationExtension.insert Lean.EnvExtension:151:4: cannot insert `List.getLast.congr_simp` into `_private.Lean.AddDecl.0.Lean.privateConstKindsExt`, it is not defined in the current module but in `Init.Data.List.Lemmas`
backtrace:
/home/markus/code/lean4/build/release/stage0/lib/lean/libleanshared.so(+0x9708b22) [0x7f1b59908b22]
/home/markus/code/lean4/build/release/stage0/lib/lean/libleanshared.so(lean_panic_fn+0xf9) [0x7f1b59908de9]
/home/markus/code/lean4/build/release/stage0/lib/lean/libleanshared.so(l_Lean_addDecl___lam__1+0x154b) [0x7f1b517d4fcb]
/home/markus/code/lean4/build/release/stage0/lib/lean/libleanshared.so(l_Lean_addDecl+0xc3c) [0x7f1b517d6d6c]
/home/markus/code/lean4/build/release/stage0/lib/lean/libleanshared.so(l___private_Lean_Meta_CongrTheorems_0__Lean_Meta_initFn___lam__0____x40_Lean_Meta_CongrTheorems_4172217453____hygCtx___hyg_2_+0xba) [0x7f1b562a764a]
/home/markus/code/lean4/build/release/stage0/lib/lean/libleanshared.so(l___private_Lean_Meta_CongrTheorems_0__Lean_Meta_initFn___lam__0____x40_Lean_Meta_CongrTheorems_4172217453____hygCtx___hyg_2____boxed+0x1f) [0x7f1b562a8bbf]
/home/markus/code/lean4/build/release/stage0/lib/lean/libleanshared.so(lean_apply_5+0xa24) [0x7f1b59916524]
/home/markus/code/lean4/build/release/stage0/lib/lean/libleanshared.so(l___private_Lean_Meta_Basic_0__Lean_Meta_realizeConst_realizeAndReport___lam__0+0x92) [0x7f1b50f7d782]
/home/markus/code/lean4/build/release/stage0/lib/lean/libleanshared.so(lean_apply_5+0xa6c) [0x7f1b5991656c]
/home/markus/code/lean4/build/release/stage0/lib/lean/libleanshared.so(l_IO_withStderr___at___IO_FS_withIsolatedStreams___at_____private_Lean_Meta_Basic_0__Lean_Meta_realizeValue_realizeAndReport_spec__1_spec__4___redArg+0x81) [0x7f1b50f66e41]
/home/markus/code/lean4/build/release/stage0/lib/lean/libleanshared.so(lean_apply_5+0xa6c) [0x7f1b5991656c]
/home/markus/code/lean4/build/release/stage0/lib/lean/libleanshared.so(l_IO_withStdout___at___IO_FS_withIsolatedStreams___at_____private_Lean_Meta_Basic_0__Lean_Meta_realizeValue_realizeAndReport_spec__1_spec__1___redArg+0x81) [0x7f1b50f66291]
/home/markus/code/lean4/build/release/stage0/lib/lean/libleanshared.so(lean_apply_5+0xa6c) [0x7f1b5991656c]
/home/markus/code/lean4/build/release/stage0/lib/lean/libleanshared.so(l_IO_withStdin___at___IO_FS_withIsolatedStreams___at_____private_Lean_Meta_Basic_0__Lean_Meta_realizeValue_realizeAndReport_spec__1_spec__2___redArg+0x81) [0x7f1b50f66861]
/home/markus/code/lean4/build/release/stage0/lib/lean/libleanshared.so(l_IO_FS_withIsolatedStreams___at_____private_Lean_Meta_Basic_0__Lean_Meta_realizeValue_realizeAndReport_spec__1___redArg+0x1c9) [0x7f1b50f67469]
/home/markus/code/lean4/build/release/stage0/lib/lean/libleanshared.so(l___private_Lean_Meta_Basic_0__Lean_Meta_realizeConst_realizeAndReport+0x16d5) [0x7f1b50f7fd55]
/home/markus/code/lean4/build/release/stage0/lib/lean/libleanshared.so(lean_apply_3+0xc8c) [0x7f1b5991349c]
/home/markus/code/lean4/build/release/stage0/lib/lean/libleanshared.so(l_Lean_Environment_realizeConst___lam__0+0x5d) [0x7f1b518d011d]
/home/markus/code/lean4/build/release/stage0/lib/lean/libleanshared.so(lean_apply_3+0xc8c) [0x7f1b5991349c]
/home/markus/code/lean4/build/release/stage0/lib/lean/libleanshared.so(l_Lean_Environment_realizeValue___at___Lean_Environment_realizeConst_spec__2___lam__0+0x35e) [0x7f1b518d853e]
/home/markus/code/lean4/build/release/stage0/lib/lean/libleanshared.so(l_Lean_Environment_realizeValue___at___Lean_Environment_realizeConst_spec__2+0x790) [0x7f1b518d97e0]
/home/markus/code/lean4/build/release/stage0/lib/lean/libleanshared.so(l_Lean_Environment_realizeConst+0xb9) [0x7f1b518da4f9]
/home/markus/code/lean4/build/release/stage0/lib/lean/libleanshared.so(l_Lean_Meta_realizeConst___lam__3+0x8c9) [0x7f1b50f85079]
/home/markus/code/lean4/build/release/stage0/lib/lean/libleanshared.so(l_Lean_Meta_realizeConst___lam__3___boxed+0x40) [0x7f1b50f86f80]
/home/markus/code/lean4/build/release/stage0/lib/lean/libleanshared.so(lean_apply_5+0x98f) [0x7f1b5991648f]
/home/markus/code/lean4/build/release/stage0/lib/lean/libleanshared.so(l_Lean_Meta_realizeConst+0x377) [0x7f1b50f873d7]
/home/markus/code/lean4/build/release/stage0/lib/lean/libleanshared.so(l___private_Lean_Meta_CongrTheorems_0__Lean_Meta_initFn___lam__2____x40_Lean_Meta_CongrTheorems_4172217453____hygCtx___hyg_2_+0x281b) [0x7f1b562a4fab]
/home/markus/code/lean4/build/release/stage0/lib/lean/libleanshared.so(lean_apply_4+0x8d8) [0x7f1b59914bb8]
/home/markus/code/lean4/build/release/stage0/lib/lean/libleanshared.so(l___private_Init_Data_Array_Basic_0__Array_anyMUnsafe_any___at___Lean_executeReservedNameAction_spec__0+0x241) [0x7f1b51a285d1]
/home/markus/code/lean4/build/release/stage0/lib/lean/libleanshared.so(l_Lean_executeReservedNameAction___lam__1+0x246) [0x7f1b51a2e8f6]
/home/markus/code/lean4/build/release/stage0/lib/lean/libleanshared.so(l_Lean_executeReservedNameAction___lam__1___boxed+0xd) [0x7f1b51a2eb1d]
/home/markus/code/lean4/build/release/stage0/lib/lean/libleanshared.so(lean_apply_3+0xcb5) [0x7f1b599134c5]
/home/markus/code/lean4/build/release/stage0/lib/lean/libleanshared.so(l_Lean_executeReservedNameAction+0xdf) [0x7f1b51a2ec3f]
/home/markus/code/lean4/build/release/stage0/lib/lean/libleanshared.so(l_Lean_Meta_mkCongrSimpForConst_x3f+0x13d) [0x7f1b562ac3ad]
/home/markus/code/lean4/build/release/stage0/lib/lean/libleanshared.so(l___private_Lean_Meta_Tactic_Simp_Types_0__Lean_Meta_Simp_mkCongrSimp_x3f_go_x3f___redArg+0xe41) [0x7f1b5575e081]
/home/markus/code/lean4/build/release/stage0/lib/lean/libleanshared.so(l_Lean_Meta_Simp_mkCongrSimp_x3f___lam__0+0x500) [0x7f1b55761b90]
/home/markus/code/lean4/build/release/stage0/lib/lean/libleanshared.so(l_Lean_Meta_Simp_mkCongrSimp_x3f___lam__0___boxed+0x26) [0x7f1b55762c06]
/home/markus/code/lean4/build/release/stage0/lib/lean/libleanshared.so(lean_apply_9+0x8d3) [0x7f1b5991b3b3]
/home/markus/code/lean4/build/release/stage0/lib/lean/libleanshared.so(l_Lean_Meta_Simp_mkCongrSimp_x3f___lam__1___boxed+0x28) [0x7f1b55763198]
/home/markus/code/lean4/build/release/stage0/lib/lean/libleanshared.so(lean_apply_1+0xbda) [0x7f1b5990fa5a]
/home/markus/code/lean4/build/release/stage0/lib/lean/libleanshared.so(l_Lean_profileitIOUnsafe___redArg___lam__0+0xc) [0x7f1b5163079c]
/home/markus/code/lean4/build/release/stage0/lib/lean/libleanshared.so(lean_apply_1+0xd76) [0x7f1b5990fbf6]
/home/markus/code/lean4/build/release/stage0/lib/lean/libleanshared.so(l_unsafeBaseIO___redArg+0xe) [0x7f1b5052ba5e]
/home/markus/code/lean4/build/release/stage0/lib/lean/libleanshared.so(lean_apply_1+0xd76) [0x7f1b5990fbf6]
/home/markus/code/lean4/build/release/stage0/lib/lean/libleanshared.so(lean_profileit+0x83) [0x7f1b591dc0a3]
/home/markus/code/lean4/build/release/stage0/lib/lean/libleanshared.so(l_Lean_profileitIOUnsafe___redArg+0xac) [0x7f1b51631a0c]
/home/markus/code/lean4/build/release/stage0/lib/lean/libleanshared.so(l_Lean_Meta_Simp_mkCongrSimp_x3f+0x12b) [0x7f1b557632fb]
/home/markus/code/lean4/build/release/stage0/lib/lean/libleanshared.so(l_Lean_Meta_Simp_tryAutoCongrTheorem_x3f+0x12c) [0x7f1b557bc26c]
/home/markus/code/lean4/build/release/stage0/lib/lean/libleanshared.so(l_Lean_Meta_Simp_congrDefault+0x118) [0x7f1b556032d8]
/home/markus/code/lean4/build/release/stage0/lib/lean/libleanshared.so(l___private_Lean_Meta_Tactic_Simp_Main_0__Lean_Meta_Simp_simpLoop_visitPreContinue+0x7fd) [0x7f1b55607cfd]
/home/markus/code/lean4/build/release/stage0/lib/lean/libleanshared.so(l_Lean_Meta_Simp_simpLoop+0x1666) [0x7f1b5560a506]
/home/markus/code/lean4/build/release/stage0/lib/lean/libleanshared.so(lean_apply_8+0x940) [0x7f1b5991a2c0]
/home/markus/code/lean4/build/release/stage0/lib/lean/libleanshared.so(l_Lean_Meta_Simp_SimpM_run___redArg___lam__0+0x3fd) [0x7f1b557e496d]
/home/markus/code/lean4/build/release/stage0/lib/lean/libleanshared.so(lean_apply_5+0xa24) [0x7f1b59916524]
/home/markus/code/lean4/build/release/stage0/lib/lean/libleanshared.so(l_Lean_Meta_withTrackingZetaDeltaSet___at___Lean_Meta_Simp_SimpM_run_spec__2___redArg+0x2297) [0x7f1b557e2367]
/home/markus/code/lean4/build/release/stage0/lib/lean/libleanshared.so(lean_apply_1+0xc69) [0x7f1b5990fae9]
/home/markus/code/lean4/build/release/stage0/lib/lean/libleanshared.so(l_Lean_profileitIOUnsafe___redArg___lam__0+0xc) [0x7f1b5163079c]
/home/markus/code/lean4/build/release/stage0/lib/lean/libleanshared.so(lean_apply_1+0xd76) [0x7f1b5990fbf6]
/home/markus/code/lean4/build/release/stage0/lib/lean/libleanshared.so(l_unsafeBaseIO___redArg+0xe) [0x7f1b5052ba5e]
/home/markus/code/lean4/build/release/stage0/lib/lean/libleanshared.so(lean_apply_1+0xd76) [0x7f1b5990fbf6]
/home/markus/code/lean4/build/release/stage0/lib/lean/libleanshared.so(lean_profileit+0x83) [0x7f1b591dc0a3]
/home/markus/code/lean4/build/release/stage0/lib/lean/libleanshared.so(l_Lean_profileitIOUnsafe___redArg+0xac) [0x7f1b51631a0c]
/home/markus/code/lean4/build/release/stage0/lib/lean/libleanshared.so(l_Lean_Meta_simpCore+0xc8) [0x7f1b55616d08]
/home/markus/code/lean4/build/release/stage0/lib/lean/libleanshared.so(l_Lean_Meta_simp___lam__0+0x1e) [0x7f1b55616d8e]
/home/markus/code/lean4/build/release/stage0/lib/lean/libleanshared.so(lean_apply_1+0xc69) [0x7f1b5990fae9]
/home/markus/code/lean4/build/release/stage0/lib/lean/libleanshared.so(l_Lean_profileitIOUnsafe___redArg___lam__0+0xc) [0x7f1b5163079c]
/home/markus/code/lean4/build/release/stage0/lib/lean/libleanshared.so(lean_apply_1+0xd76) [0x7f1b5990fbf6]
/home/markus/code/lean4/build/release/stage0/lib/lean/libleanshared.so(l_unsafeBaseIO___redArg+0xe) [0x7f1b5052ba5e]
/home/markus/code/lean4/build/release/stage0/lib/lean/libleanshared.so(lean_apply_1+0xd76) [0x7f1b5990fbf6]
/home/markus/code/lean4/build/release/stage0/lib/lean/libleanshared.so(lean_profileit+0x83) [0x7f1b591dc0a3]
/home/markus/code/lean4/build/release/stage0/lib/lean/libleanshared.so(l_Lean_profileitIOUnsafe___redArg+0xac) [0x7f1b51631a0c]
/home/markus/code/lean4/build/release/stage0/lib/lean/libleanshared.so(l_Lean_Meta_simp+0x18c) [0x7f1b5561781c]
/home/markus/code/lean4/build/release/stage0/lib/lean/libleanshared.so(lean_grind_normalize+0x19b) [0x7f1b54eadf6b]
/home/markus/code/lean4/build/release/stage0/lib/lean/libleanshared.so(l_Lean_Meta_Grind_preprocessPattern+0x1b5) [0x7f1b54f32b95]
/home/markus/code/lean4/build/release/stage0/lib/lean/libleanshared.so(l_Lean_Meta_Grind_mkEMatchEqTheoremCore___lam__0+0x18e) [0x7f1b54f7f6be]
/home/markus/code/lean4/build/release/stage0/lib/lean/libleanshared.so(l_Lean_Meta_Grind_mkEMatchEqTheoremCore___lam__1___boxed+0x2a) [0x7f1b54f81a4a]
/home/markus/code/lean4/build/release/stage0/lib/lean/libleanshared.so(lean_apply_7+0x987) [0x7f1b59919077]
/home/markus/code/lean4/build/release/stage0/lib/lean/libleanshared.so(lean_apply_7+0x837) [0x7f1b59918f27]
/home/markus/code/lean4/build/release/stage0/lib/lean/libleanshared.so(lean_apply_5+0x94c) [0x7f1b5991644c]
/home/markus/code/lean4/build/release/stage0/lib/lean/libleanshared.so(l___private_Lean_Meta_Basic_0__Lean_Meta_forallTelescopeReducingAuxAux___redArg+0x51) [0x7f1b50efe111]
/home/markus/code/lean4/build/release/stage0/lib/lean/libleanshared.so(l___private_Lean_Meta_Basic_0__Lean_Meta_forallTelescopeReducingAux___redArg+0x622) [0x7f1b50efe752]
/home/markus/code/lean4/build/release/stage0/lib/lean/libleanshared.so(l___private_Lean_Meta_Basic_0__Lean_Meta_forallTelescopeReducingImp___redArg+0x29) [0x7f1b50f07789]
/home/markus/code/lean4/build/release/stage0/lib/lean/libleanshared.so(l_Lean_Meta_forallTelescopeReducing___at_____private_Lean_Meta_Tactic_Grind_EMatchTheorem_0__Lean_Meta_Grind_preprocessMatchCongrEqType_spec__5___redArg+0x81) [0x7f1b54f2acb1]
/home/markus/code/lean4/build/release/stage0/lib/lean/libleanshared.so(l_Lean_Meta_Grind_mkEMatchEqTheoremCore+0x234) [0x7f1b54f7d924]
/home/markus/code/lean4/build/release/stage0/lib/lean/libleanshared.so(l_Lean_Meta_Grind_mkEMatchEqTheorem+0x288) [0x7f1b54f7e558]
/home/markus/code/lean4/build/release/stage0/lib/lean/libleanshared.so(l___private_Lean_Meta_Tactic_Grind_EMatchTheorem_0__Lean_Meta_Grind_addGrindEqAttr+0xb08) [0x7f1b54fefff8]
/home/markus/code/lean4/build/release/stage0/lib/lean/libleanshared.so(l_Lean_Meta_Grind_addEMatchAttr+0x1c2) [0x7f1b54ff40d2]
/home/markus/code/lean4/build/release/stage0/lib/lean/libleanshared.so(l___private_Lean_Meta_Tactic_Grind_Attr_0__Lean_Meta_Grind_registerGrindAttr___lam__0+0x377d) [0x7f1b54efe43d]
/home/markus/code/lean4/build/release/stage0/lib/lean/libleanshared.so(lean_apply_6+0x71c) [0x7f1b5991791c]
/home/markus/code/lean4/build/release/stage0/lib/lean/libleanshared.so(l___private_Init_Data_Array_Basic_0__Array_forIn_x27Unsafe_loop___at_____private_Init_Data_Array_Basic_0__Array_forIn_x27Unsafe_loop___at_____private_Lean_Elab_Term_TermElabM_0__Lean_Elab_Term_applyAttributesCore_spec__12_spec__12___lam__2+0x61) [0x7f1b532d8761]
/home/markus/code/lean4/build/release/stage0/lib/lean/libleanshared.so(lean_apply_7+0x933) [0x7f1b59919023]
/home/markus/code/lean4/build/release/stage0/lib/lean/libleanshared.so(l_Lean_Elab_withInfoTreeContext___at___Lean_Elab_withMacroExpansionInfo___at___Lean_Elab_Term_withMacroExpansion_spec__0_spec__0___redArg+0x185) [0x7f1b532b17f5]
/home/markus/code/lean4/build/release/stage0/lib/lean/libleanshared.so(lean_apply_7+0x8dc) [0x7f1b59918fcc]
/home/markus/code/lean4/build/release/stage0/lib/lean/libleanshared.so(l_Lean_Elab_withLogging___at_____private_Lean_Elab_Term_TermElabM_0__Lean_Elab_Term_applyAttributesCore_spec__2+0xcb) [0x7f1b532d6d6b]
/home/markus/code/lean4/build/release/stage0/lib/lean/libleanshared.so(l___private_Init_Data_Array_Basic_0__Array_forIn_x27Unsafe_loop___at_____private_Init_Data_Array_Basic_0__Array_forIn_x27Unsafe_loop___at_____private_Lean_Elab_Term_TermElabM_0__Lean_Elab_Term_applyAttributesCore_spec__12_spec__12___lam__4___boxed+0x19) [0x7f1b532dc4c9]
/home/markus/code/lean4/build/release/stage0/lib/lean/libleanshared.so(lean_apply_7+0x987) [0x7f1b59919077]
/home/markus/code/lean4/build/release/stage0/lib/lean/libleanshared.so(l___private_Init_Data_Array_Basic_0__Array_forIn_x27Unsafe_loop___at_____private_Lean_Elab_Term_TermElabM_0__Lean_Elab_Term_applyAttributesCore_spec__12+0x3fa) [0x7f1b5331f58a]
/home/markus/code/lean4/build/release/stage0/lib/lean/libleanshared.so(l___private_Lean_Elab_Term_TermElabM_0__Lean_Elab_Term_applyAttributesCore___lam__0+0x2a) [0x7f1b5331faea]
/home/markus/code/lean4/build/release/stage0/lib/lean/libleanshared.so(l___private_Lean_Elab_Term_TermElabM_0__Lean_Elab_Term_applyAttributesCore___lam__0___boxed+0x70) [0x7f1b5331fc60]
/home/markus/code/lean4/build/release/stage0/lib/lean/libleanshared.so(lean_apply_7+0x8dc) [0x7f1b59918fcc]
PANIC at Lean.MapDeclarationExtension.insert Lean.EnvExtension:151:4: cannot insert `List.getLast.congr_simp` into `Lean.Meta.congrKindsExt`, it is not defined in the current module but in `Init.Data.List.Lemmas`
backtrace:
/home/markus/code/lean4/build/release/stage0/lib/lean/libleanshared.so(+0x9708b22) [0x7f1b59908b22]
/home/markus/code/lean4/build/release/stage0/lib/lean/libleanshared.so(lean_panic_fn+0xf9) [0x7f1b59908de9]
/home/markus/code/lean4/build/release/stage0/lib/lean/libleanshared.so(l___private_Lean_Meta_CongrTheorems_0__Lean_Meta_initFn___lam__0____x40_Lean_Meta_CongrTheorems_4172217453____hygCtx___hyg_2_+0x742) [0x7f1b562a7cd2]
/home/markus/code/lean4/build/release/stage0/lib/lean/libleanshared.so(l___private_Lean_Meta_CongrTheorems_0__Lean_Meta_initFn___lam__0____x40_Lean_Meta_CongrTheorems_4172217453____hygCtx___hyg_2____boxed+0x1f) [0x7f1b562a8bbf]
/home/markus/code/lean4/build/release/stage0/lib/lean/libleanshared.so(lean_apply_5+0xa24) [0x7f1b59916524]
/home/markus/code/lean4/build/release/stage0/lib/lean/libleanshared.so(l___private_Lean_Meta_Basic_0__Lean_Meta_realizeConst_realizeAndReport___lam__0+0x92) [0x7f1b50f7d782]
/home/markus/code/lean4/build/release/stage0/lib/lean/libleanshared.so(lean_apply_5+0xa6c) [0x7f1b5991656c]
/home/markus/code/lean4/build/release/stage0/lib/lean/libleanshared.so(l_IO_withStderr___at___IO_FS_withIsolatedStreams___at_____private_Lean_Meta_Basic_0__Lean_Meta_realizeValue_realizeAndReport_spec__1_spec__4___redArg+0x81) [0x7f1b50f66e41]
/home/markus/code/lean4/build/release/stage0/lib/lean/libleanshared.so(lean_apply_5+0xa6c) [0x7f1b5991656c]
/home/markus/code/lean4/build/release/stage0/lib/lean/libleanshared.so(l_IO_withStdout___at___IO_FS_withIsolatedStreams___at_____private_Lean_Meta_Basic_0__Lean_Meta_realizeValue_realizeAndReport_spec__1_spec__1___redArg+0x81) [0x7f1b50f66291]
/home/markus/code/lean4/build/release/stage0/lib/lean/libleanshared.so(lean_apply_5+0xa6c) [0x7f1b5991656c]
/home/markus/code/lean4/build/release/stage0/lib/lean/libleanshared.so(l_IO_withStdin___at___IO_FS_withIsolatedStreams___at_____private_Lean_Meta_Basic_0__Lean_Meta_realizeValue_realizeAndReport_spec__1_spec__2___redArg+0x81) [0x7f1b50f66861]
/home/markus/code/lean4/build/release/stage0/lib/lean/libleanshared.so(l_IO_FS_withIsolatedStreams___at_____private_Lean_Meta_Basic_0__Lean_Meta_realizeValue_realizeAndReport_spec__1___redArg+0x1c9) [0x7f1b50f67469]
/home/markus/code/lean4/build/release/stage0/lib/lean/libleanshared.so(l___private_Lean_Meta_Basic_0__Lean_Meta_realizeConst_realizeAndReport+0x16d5) [0x7f1b50f7fd55]
/home/markus/code/lean4/build/release/stage0/lib/lean/libleanshared.so(lean_apply_3+0xc8c) [0x7f1b5991349c]
/home/markus/code/lean4/build/release/stage0/lib/lean/libleanshared.so(l_Lean_Environment_realizeConst___lam__0+0x5d) [0x7f1b518d011d]
/home/markus/code/lean4/build/release/stage0/lib/lean/libleanshared.so(lean_apply_3+0xc8c) [0x7f1b5991349c]
/home/markus/code/lean4/build/release/stage0/lib/lean/libleanshared.so(l_Lean_Environment_realizeValue___at___Lean_Environment_realizeConst_spec__2___lam__0+0x35e) [0x7f1b518d853e]
/home/markus/code/lean4/build/release/stage0/lib/lean/libleanshared.so(l_Lean_Environment_realizeValue___at___Lean_Environment_realizeConst_spec__2+0x790) [0x7f1b518d97e0]
/home/markus/code/lean4/build/release/stage0/lib/lean/libleanshared.so(l_Lean_Environment_realizeConst+0xb9) [0x7f1b518da4f9]
/home/markus/code/lean4/build/release/stage0/lib/lean/libleanshared.so(l_Lean_Meta_realizeConst___lam__3+0x8c9) [0x7f1b50f85079]
/home/markus/code/lean4/build/release/stage0/lib/lean/libleanshared.so(l_Lean_Meta_realizeConst___lam__3___boxed+0x40) [0x7f1b50f86f80]
/home/markus/code/lean4/build/release/stage0/lib/lean/libleanshared.so(lean_apply_5+0x98f) [0x7f1b5991648f]
/home/markus/code/lean4/build/release/stage0/lib/lean/libleanshared.so(l_Lean_Meta_realizeConst+0x377) [0x7f1b50f873d7]
/home/markus/code/lean4/build/release/stage0/lib/lean/libleanshared.so(l___private_Lean_Meta_CongrTheorems_0__Lean_Meta_initFn___lam__2____x40_Lean_Meta_CongrTheorems_4172217453____hygCtx___hyg_2_+0x281b) [0x7f1b562a4fab]
/home/markus/code/lean4/build/release/stage0/lib/lean/libleanshared.so(lean_apply_4+0x8d8) [0x7f1b59914bb8]
/home/markus/code/lean4/build/release/stage0/lib/lean/libleanshared.so(l___private_Init_Data_Array_Basic_0__Array_anyMUnsafe_any___at___Lean_executeReservedNameAction_spec__0+0x241) [0x7f1b51a285d1]
/home/markus/code/lean4/build/release/stage0/lib/lean/libleanshared.so(l_Lean_executeReservedNameAction___lam__1+0x246) [0x7f1b51a2e8f6]
/home/markus/code/lean4/build/release/stage0/lib/lean/libleanshared.so(l_Lean_executeReservedNameAction___lam__1___boxed+0xd) [0x7f1b51a2eb1d]
/home/markus/code/lean4/build/release/stage0/lib/lean/libleanshared.so(lean_apply_3+0xcb5) [0x7f1b599134c5]
/home/markus/code/lean4/build/release/stage0/lib/lean/libleanshared.so(l_Lean_executeReservedNameAction+0xdf) [0x7f1b51a2ec3f]
/home/markus/code/lean4/build/release/stage0/lib/lean/libleanshared.so(l_Lean_Meta_mkCongrSimpForConst_x3f+0x13d) [0x7f1b562ac3ad]
/home/markus/code/lean4/build/release/stage0/lib/lean/libleanshared.so(l___private_Lean_Meta_Tactic_Simp_Types_0__Lean_Meta_Simp_mkCongrSimp_x3f_go_x3f___redArg+0xe41) [0x7f1b5575e081]
/home/markus/code/lean4/build/release/stage0/lib/lean/libleanshared.so(l_Lean_Meta_Simp_mkCongrSimp_x3f___lam__0+0x500) [0x7f1b55761b90]
/home/markus/code/lean4/build/release/stage0/lib/lean/libleanshared.so(l_Lean_Meta_Simp_mkCongrSimp_x3f___lam__0___boxed+0x26) [0x7f1b55762c06]
/home/markus/code/lean4/build/release/stage0/lib/lean/libleanshared.so(lean_apply_9+0x8d3) [0x7f1b5991b3b3]
/home/markus/code/lean4/build/release/stage0/lib/lean/libleanshared.so(l_Lean_Meta_Simp_mkCongrSimp_x3f___lam__1___boxed+0x28) [0x7f1b55763198]
/home/markus/code/lean4/build/release/stage0/lib/lean/libleanshared.so(lean_apply_1+0xbda) [0x7f1b5990fa5a]
/home/markus/code/lean4/build/release/stage0/lib/lean/libleanshared.so(l_Lean_profileitIOUnsafe___redArg___lam__0+0xc) [0x7f1b5163079c]
/home/markus/code/lean4/build/release/stage0/lib/lean/libleanshared.so(lean_apply_1+0xd76) [0x7f1b5990fbf6]
/home/markus/code/lean4/build/release/stage0/lib/lean/libleanshared.so(l_unsafeBaseIO___redArg+0xe) [0x7f1b5052ba5e]
/home/markus/code/lean4/build/release/stage0/lib/lean/libleanshared.so(lean_apply_1+0xd76) [0x7f1b5990fbf6]
/home/markus/code/lean4/build/release/stage0/lib/lean/libleanshared.so(lean_profileit+0x83) [0x7f1b591dc0a3]
/home/markus/code/lean4/build/release/stage0/lib/lean/libleanshared.so(l_Lean_profileitIOUnsafe___redArg+0xac) [0x7f1b51631a0c]
/home/markus/code/lean4/build/release/stage0/lib/lean/libleanshared.so(l_Lean_Meta_Simp_mkCongrSimp_x3f+0x12b) [0x7f1b557632fb]
/home/markus/code/lean4/build/release/stage0/lib/lean/libleanshared.so(l_Lean_Meta_Simp_tryAutoCongrTheorem_x3f+0x12c) [0x7f1b557bc26c]
/home/markus/code/lean4/build/release/stage0/lib/lean/libleanshared.so(l_Lean_Meta_Simp_congrDefault+0x118) [0x7f1b556032d8]
/home/markus/code/lean4/build/release/stage0/lib/lean/libleanshared.so(l___private_Lean_Meta_Tactic_Simp_Main_0__Lean_Meta_Simp_simpLoop_visitPreContinue+0x7fd) [0x7f1b55607cfd]
/home/markus/code/lean4/build/release/stage0/lib/lean/libleanshared.so(l_Lean_Meta_Simp_simpLoop+0x1666) [0x7f1b5560a506]
/home/markus/code/lean4/build/release/stage0/lib/lean/libleanshared.so(lean_apply_8+0x940) [0x7f1b5991a2c0]
/home/markus/code/lean4/build/release/stage0/lib/lean/libleanshared.so(l_Lean_Meta_Simp_SimpM_run___redArg___lam__0+0x3fd) [0x7f1b557e496d]
/home/markus/code/lean4/build/release/stage0/lib/lean/libleanshared.so(lean_apply_5+0xa24) [0x7f1b59916524]
/home/markus/code/lean4/build/release/stage0/lib/lean/libleanshared.so(l_Lean_Meta_withTrackingZetaDeltaSet___at___Lean_Meta_Simp_SimpM_run_spec__2___redArg+0x2297) [0x7f1b557e2367]
/home/markus/code/lean4/build/release/stage0/lib/lean/libleanshared.so(lean_apply_1+0xc69) [0x7f1b5990fae9]
/home/markus/code/lean4/build/release/stage0/lib/lean/libleanshared.so(l_Lean_profileitIOUnsafe___redArg___lam__0+0xc) [0x7f1b5163079c]
/home/markus/code/lean4/build/release/stage0/lib/lean/libleanshared.so(lean_apply_1+0xd76) [0x7f1b5990fbf6]
/home/markus/code/lean4/build/release/stage0/lib/lean/libleanshared.so(l_unsafeBaseIO___redArg+0xe) [0x7f1b5052ba5e]
/home/markus/code/lean4/build/release/stage0/lib/lean/libleanshared.so(lean_apply_1+0xd76) [0x7f1b5990fbf6]
/home/markus/code/lean4/build/release/stage0/lib/lean/libleanshared.so(lean_profileit+0x83) [0x7f1b591dc0a3]
/home/markus/code/lean4/build/release/stage0/lib/lean/libleanshared.so(l_Lean_profileitIOUnsafe___redArg+0xac) [0x7f1b51631a0c]
/home/markus/code/lean4/build/release/stage0/lib/lean/libleanshared.so(l_Lean_Meta_simpCore+0xc8) [0x7f1b55616d08]
/home/markus/code/lean4/build/release/stage0/lib/lean/libleanshared.so(l_Lean_Meta_simp___lam__0+0x1e) [0x7f1b55616d8e]
/home/markus/code/lean4/build/release/stage0/lib/lean/libleanshared.so(lean_apply_1+0xc69) [0x7f1b5990fae9]
/home/markus/code/lean4/build/release/stage0/lib/lean/libleanshared.so(l_Lean_profileitIOUnsafe___redArg___lam__0+0xc) [0x7f1b5163079c]
/home/markus/code/lean4/build/release/stage0/lib/lean/libleanshared.so(lean_apply_1+0xd76) [0x7f1b5990fbf6]
/home/markus/code/lean4/build/release/stage0/lib/lean/libleanshared.so(l_unsafeBaseIO___redArg+0xe) [0x7f1b5052ba5e]
/home/markus/code/lean4/build/release/stage0/lib/lean/libleanshared.so(lean_apply_1+0xd76) [0x7f1b5990fbf6]
/home/markus/code/lean4/build/release/stage0/lib/lean/libleanshared.so(lean_profileit+0x83) [0x7f1b591dc0a3]
/home/markus/code/lean4/build/release/stage0/lib/lean/libleanshared.so(l_Lean_profileitIOUnsafe___redArg+0xac) [0x7f1b51631a0c]
/home/markus/code/lean4/build/release/stage0/lib/lean/libleanshared.so(l_Lean_Meta_simp+0x18c) [0x7f1b5561781c]
/home/markus/code/lean4/build/release/stage0/lib/lean/libleanshared.so(lean_grind_normalize+0x19b) [0x7f1b54eadf6b]
/home/markus/code/lean4/build/release/stage0/lib/lean/libleanshared.so(l_Lean_Meta_Grind_preprocessPattern+0x1b5) [0x7f1b54f32b95]
/home/markus/code/lean4/build/release/stage0/lib/lean/libleanshared.so(l_Lean_Meta_Grind_mkEMatchEqTheoremCore___lam__0+0x18e) [0x7f1b54f7f6be]
/home/markus/code/lean4/build/release/stage0/lib/lean/libleanshared.so(l_Lean_Meta_Grind_mkEMatchEqTheoremCore___lam__1___boxed+0x2a) [0x7f1b54f81a4a]
/home/markus/code/lean4/build/release/stage0/lib/lean/libleanshared.so(lean_apply_7+0x987) [0x7f1b59919077]
/home/markus/code/lean4/build/release/stage0/lib/lean/libleanshared.so(lean_apply_7+0x837) [0x7f1b59918f27]
/home/markus/code/lean4/build/release/stage0/lib/lean/libleanshared.so(lean_apply_5+0x94c) [0x7f1b5991644c]
/home/markus/code/lean4/build/release/stage0/lib/lean/libleanshared.so(l___private_Lean_Meta_Basic_0__Lean_Meta_forallTelescopeReducingAuxAux___redArg+0x51) [0x7f1b50efe111]
/home/markus/code/lean4/build/release/stage0/lib/lean/libleanshared.so(l___private_Lean_Meta_Basic_0__Lean_Meta_forallTelescopeReducingAux___redArg+0x622) [0x7f1b50efe752]
/home/markus/code/lean4/build/release/stage0/lib/lean/libleanshared.so(l___private_Lean_Meta_Basic_0__Lean_Meta_forallTelescopeReducingImp___redArg+0x29) [0x7f1b50f07789]
/home/markus/code/lean4/build/release/stage0/lib/lean/libleanshared.so(l_Lean_Meta_forallTelescopeReducing___at_____private_Lean_Meta_Tactic_Grind_EMatchTheorem_0__Lean_Meta_Grind_preprocessMatchCongrEqType_spec__5___redArg+0x81) [0x7f1b54f2acb1]
/home/markus/code/lean4/build/release/stage0/lib/lean/libleanshared.so(l_Lean_Meta_Grind_mkEMatchEqTheoremCore+0x234) [0x7f1b54f7d924]
/home/markus/code/lean4/build/release/stage0/lib/lean/libleanshared.so(l_Lean_Meta_Grind_mkEMatchEqTheorem+0x288) [0x7f1b54f7e558]
/home/markus/code/lean4/build/release/stage0/lib/lean/libleanshared.so(l___private_Lean_Meta_Tactic_Grind_EMatchTheorem_0__Lean_Meta_Grind_addGrindEqAttr+0xb08) [0x7f1b54fefff8]
/home/markus/code/lean4/build/release/stage0/lib/lean/libleanshared.so(l_Lean_Meta_Grind_addEMatchAttr+0x1c2) [0x7f1b54ff40d2]
/home/markus/code/lean4/build/release/stage0/lib/lean/libleanshared.so(l___private_Lean_Meta_Tactic_Grind_Attr_0__Lean_Meta_Grind_registerGrindAttr___lam__0+0x377d) [0x7f1b54efe43d]
/home/markus/code/lean4/build/release/stage0/lib/lean/libleanshared.so(lean_apply_6+0x71c) [0x7f1b5991791c]
/home/markus/code/lean4/build/release/stage0/lib/lean/libleanshared.so(l___private_Init_Data_Array_Basic_0__Array_forIn_x27Unsafe_loop___at_____private_Init_Data_Array_Basic_0__Array_forIn_x27Unsafe_loop___at_____private_Lean_Elab_Term_TermElabM_0__Lean_Elab_Term_applyAttributesCore_spec__12_spec__12___lam__2+0x61) [0x7f1b532d8761]
/home/markus/code/lean4/build/release/stage0/lib/lean/libleanshared.so(lean_apply_7+0x933) [0x7f1b59919023]
/home/markus/code/lean4/build/release/stage0/lib/lean/libleanshared.so(l_Lean_Elab_withInfoTreeContext___at___Lean_Elab_withMacroExpansionInfo___at___Lean_Elab_Term_withMacroExpansion_spec__0_spec__0___redArg+0x185) [0x7f1b532b17f5]
/home/markus/code/lean4/build/release/stage0/lib/lean/libleanshared.so(lean_apply_7+0x8dc) [0x7f1b59918fcc]
/home/markus/code/lean4/build/release/stage0/lib/lean/libleanshared.so(l_Lean_Elab_withLogging___at_____private_Lean_Elab_Term_TermElabM_0__Lean_Elab_Term_applyAttributesCore_spec__2+0xcb) [0x7f1b532d6d6b]
/home/markus/code/lean4/build/release/stage0/lib/lean/libleanshared.so(l___private_Init_Data_Array_Basic_0__Array_forIn_x27Unsafe_loop___at_____private_Init_Data_Array_Basic_0__Array_forIn_x27Unsafe_loop___at_____private_Lean_Elab_Term_TermElabM_0__Lean_Elab_Term_applyAttributesCore_spec__12_spec__12___lam__4___boxed+0x19) [0x7f1b532dc4c9]
/home/markus/code/lean4/build/release/stage0/lib/lean/libleanshared.so(lean_apply_7+0x987) [0x7f1b59919077]
/home/markus/code/lean4/build/release/stage0/lib/lean/libleanshared.so(l___private_Init_Data_Array_Basic_0__Array_forIn_x27Unsafe_loop___at_____private_Lean_Elab_Term_TermElabM_0__Lean_Elab_Term_applyAttributesCore_spec__12+0x3fa) [0x7f1b5331f58a]
/home/markus/code/lean4/build/release/stage0/lib/lean/libleanshared.so(l___private_Lean_Elab_Term_TermElabM_0__Lean_Elab_Term_applyAttributesCore___lam__0+0x2a) [0x7f1b5331faea]
/home/markus/code/lean4/build/release/stage0/lib/lean/libleanshared.so(l___private_Lean_Elab_Term_TermElabM_0__Lean_Elab_Term_applyAttributesCore___lam__0___boxed+0x70) [0x7f1b5331fc60]
/home/markus/code/lean4/build/release/stage0/lib/lean/libleanshared.so(lean_apply_7+0x8dc) [0x7f1b59918fcc]
/home/markus/code/lean4/build/release/stage0/lib/lean/libleanshared.so(l_Lean_withDeclNameForAuxNaming___at___Lean_Elab_Term_withDeclName_spec__0___redArg+0x762) [0x7f1b532998b2]
/home/markus/code/lean4/build/release/stage0/lib/lean/libleanshared.so(lean_apply_7+0x987) [0x7f1b59919077]The error goes away when changing the import of Init.Data.List.Lemmas to a public import.
Steps to Reproduce
- Build the linked commit
Expected behavior: No error or helpful error message
Actual behavior: See above
Additional Information
[Additional information, configuration or data that might be necessary to reproduce the issue]
Impact
Add 👍 to issues you consider important. If others are impacted by this issue, please ask them to add 👍 to it.