issue-link js-issue-link" data-error-text="Failed to load title" data-id="2267230741" data-permission-text="Title is private" data-url="https://github.com/leanprover/lean4/issues/4006" data-hovercard-type="pull_request" data-hovercard-url="/leanprover/lean4/pull/4006/hovercard" href="https://github.com/leanprover/lean4/pull/4006">#4006. Here is the stacktrace produced by Kim: ``` * thread #1, queue = 'com.apple.main-thread', stop reason = EXC_BAD_ACCESS (code=1, address=0x100000000000a) * frame #0: 0x00000001066db21c libleanshared.dylib`lean::ir::interpreter::eval_body(lean::object_ref const&) + 2816 frame #1: 0x00000001066dd464 libleanshared.dylib`lean::ir::interpreter::call(lean::name const&, lean::array_ref<lean::object_ref> const&) + 1360 frame #2: 0x00000001066db394 libleanshared.dylib`lean::ir::interpreter::eval_body(lean::object_ref const&) + 3192 frame #3: 0x00000001066dd464 libleanshared.dylib`lean::ir::interpreter::call(lean::name const&, lean::array_ref<lean::object_ref> const&) + 1360 frame #4: 0x00000001066db394 libleanshared.dylib`lean::ir::interpreter::eval_body(lean::object_ref const&) + 3192 frame #5: 0x00000001066dd464 libleanshared.dylib`lean::ir::interpreter::call(lean::name const&, lean::array_ref<lean::object_ref> const&) + 1360 frame #6: 0x00000001066db394 libleanshared.dylib`lean::ir::interpreter::eval_body(lean::object_ref const&) + 3192 frame #7: 0x00000001066df288 libleanshared.dylib`lean::ir::interpreter::stub_m(lean_object**) + 556 frame #8: 0x00000001066d6ee0 libleanshared.dylib`lean_object* lean::ir::interpreter::with_interpreter<lean_object*>(lean::environment const&, lean::options const&, lean::name const&, std::__1::function<lean_object* (lean::ir::interpreter&)> const&) + 320 frame #9: 0x00000001066dee84 libleanshared.dylib`lean::ir::interpreter::stub_m_aux(lean_object**) + 92 frame #10: 0x00000001066deafc libleanshared.dylib`lean::ir::interpreter::stub_9_aux(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*) + 60 frame #11: 0x00000001066f52a0 libleanshared.dylib`lean_apply_6 + 1748 frame #12: 0x00000001055d1ac8 libleanshared.dylib`l_Array_forInUnsafe_loop___at___private_Lean_Elab_Term_0__Lean_Elab_Term_applyAttributesCore___spec__10___lambda__2 + 156 frame #13: 0x00000001055d47e8 libleanshared.dylib`l_Array_forInUnsafe_loop___at___private_Lean_Elab_Term_0__Lean_Elab_Term_applyAttributesCore___spec__10___lambda__2___boxed + 144 frame #14: 0x00000001066f5bcc libleanshared.dylib`lean_apply_7 + 1348 frame #15: 0x00000001055ccccc libleanshared.dylib`l_Lean_Elab_withInfoTreeContext___at___private_Lean_Elab_Term_0__Lean_Elab_Term_applyAttributesCore___spec__4 + 528 frame #16: 0x00000001066f5b6c libleanshared.dylib`lean_apply_7 + 1252 frame #17: 0x00000001055d1550 libleanshared.dylib`l_Lean_Elab_withLogging___at___private_Lean_Elab_Term_0__Lean_Elab_Term_applyAttributesCore___spec__6 + 240 frame #18: 0x00000001055d4cb4 libleanshared.dylib`l_Array_forInUnsafe_loop___at___private_Lean_Elab_Term_0__Lean_Elab_Term_applyAttributesCore___spec__10 + 940 frame #19: 0x00000001055d5394 libleanshared.dylib`l___private_Lean_Elab_Term_0__Lean_Elab_Term_applyAttributesCore___lambda__1 + 60 frame #20: 0x00000001055d5740 libleanshared.dylib`l___private_Lean_Elab_Term_0__Lean_Elab_Term_applyAttributesCore___lambda__1___boxed + 148 frame #21: 0x00000001066f11f4 libleanshared.dylib`lean_apply_1 + 840 frame #22: 0x0000000103bce27c libleanshared.dylib`l_Lean_profileitIOUnsafe___rarg___lambda__1 + 24 frame #23: 0x0000000103bce4ec libleanshared.dylib`l_Lean_profileitIOUnsafe___rarg___lambda__1___boxed + 20 frame #24: 0x00000001066f10bc libleanshared.dylib`lean_apply_1 + 528 frame #25: 0x0000000106644260 libleanshared.dylib`lean_profileit + 128 frame #26: 0x0000000103bce3e0 libleanshared.dylib`l_Lean_profileitIOUnsafe___rarg + 112 frame #27: 0x00000001055d564c libleanshared.dylib`l___private_Lean_Elab_Term_0__Lean_Elab_Term_applyAttributesCore + 268 frame #28: 0x00000001055d6264 libleanshared.dylib`l_Lean_Elab_Term_applyAttributes + 52 frame #29: 0x000000010597b840 libleanshared.dylib`l_Array_forInUnsafe_loop___at_Lean_Elab_Command_elabAttr___spec__6___lambda__1 + 740 frame #30: 0x000000010597daf4 libleanshared.dylib`l_Array_forInUnsafe_loop___at_Lean_Elab_Command_elabAttr___spec__6___lambda__1___boxed + 124 frame #31: 0x00000001066f65d8 libleanshared.dylib`lean_apply_8 + 1252 frame #32: 0x00000001066f5b6c libleanshared.dylib`lean_apply_7 + 1252 frame #33: 0x0000000104f587b0 libleanshared.dylib`l___private_Lean_Elab_InfoTree_Main_0__Lean_Elab_withSavedPartialInfoContext___at_Lean_Elab_Command_liftTermElabM___spec__2___rarg___lambda__1 + 344 frame #34: 0x0000000104f59ec4 libleanshared.dylib`l___private_Lean_Elab_InfoTree_Main_0__Lean_Elab_withSavedPartialInfoContext___at_Lean_Elab_Command_liftTermElabM___spec__2___rarg + 280 frame #35: 0x0000000104f5af20 libleanshared.dylib`l_Lean_Elab_Command_liftTermElabM___rarg___lambda__1 + 144 frame #36: 0x00000001066f5ab8 libleanshared.dylib`lean_apply_7 + 1072 frame #37: 0x0000000105636090 libleanshared.dylib`l_Lean_Elab_Term_TermElabM_run___rarg + 844 frame #38: 0x0000000104f5b8fc libleanshared.dylib`l_Lean_Elab_Command_liftTermElabM___rarg + 1696 frame #39: 0x000000010597d67c libleanshared.dylib`l_Array_forInUnsafe_loop___at_Lean_Elab_Command_elabAttr___spec__6 + 928 frame #40: 0x000000010597de60 libleanshared.dylib`l_Lean_Elab_Command_elabAttr + 772 frame #41: 0x000000010597e838 libleanshared.dylib`l_Lean_Elab_Command_elabAttr___boxed + 20 frame #42: 0x00000001066f2cd4 libleanshared.dylib`lean_apply_3 + 868 frame #43: 0x0000000104f385f8 libleanshared.dylib`l_Lean_Elab_withInfoTreeContext___at___private_Lean_Elab_Command_0__Lean_Elab_Command_elabCommandUsing___spec__2 + 396 frame #44: 0x0000000104f39e48 libleanshared.dylib`l___private_Lean_Elab_Command_0__Lean_Elab_Command_elabCommandUsing + 484 frame #45: 0x00000001066f2cf0 libleanshared.dylib`lean_apply_3 + 896 frame #46: 0x0000000104f341d4 libleanshared.dylib`l_Lean_withTraceNode___at_Lean_Elab_Command_runLinters___spec__11 + 788 frame #47: 0x00000001066f2d54 libleanshared.dylib`lean_apply_3 + 996 frame #48: 0x00000001066f2cf0 libleanshared.dylib`lean_apply_3 + 896 frame #49: 0x0000000104f40e30 libleanshared.dylib`l_Lean_Elab_withLogging___at_Lean_Elab_Command_elabCommand___spec__2 + 104 frame #50: 0x0000000104f4c51c libleanshared.dylib`l_Lean_Elab_Command_elabCommandTopLevel___lambda__1 + 432 frame #51: 0x00000001066f10e8 libleanshared.dylib`lean_apply_1 + 572 frame #52: 0x0000000103bce27c libleanshared.dylib`l_Lean_profileitIOUnsafe___rarg___lambda__1 + 24 frame #53: 0x0000000103bce4ec libleanshared.dylib`l_Lean_profileitIOUnsafe___rarg___lambda__1___boxed + 20 frame #54: 0x00000001066f10bc libleanshared.dylib`lean_apply_1 + 528 frame #55: 0x0000000106644260 libleanshared.dylib`lean_profileit + 128 frame #56: 0x0000000103bce3e0 libleanshared.dylib`l_Lean_profileitIOUnsafe___rarg + 112 frame #57: 0x0000000104f4fce0 libleanshared.dylib`l_Lean_Elab_Command_elabCommandTopLevel + 1284 frame #58: 0x00000001057d2f30 libleanshared.dylib`l_Lean_Elab_Frontend_elabCommandAtFrontend + 1384 frame #59: 0x00000001057d63b8 libleanshared.dylib`l_Lean_Elab_Frontend_processCommand + 1332 frame #60: 0x00000001057d6e48 libleanshared.dylib`l_Lean_Elab_Frontend_processCommands + 72 frame #61: 0x00000001057d7248 libleanshared.dylib`l_Lean_Elab_IO_processCommands + 212 frame #62: 0x00000001057d83d0 libleanshared.dylib`l_Lean_Elab_runFrontend___lambda__3 + 76 frame #63: 0x00000001057d96d0 libleanshared.dylib`lean_run_frontend + 2436 frame #64: 0x00000001065e72b4 libleanshared.dylib`lean::run_new_frontend(std::__1::basic_string<char, std::__1::char_traits<char>, std::__1::allocator<char>> const&, lean::options const&, std::__1::basic_string<char, std::__1::char_traits<char>, std::__1::allocator<char>> const&, lean::name const&, unsigned int, lean::optional<std::__1::basic_string<char, std::__1::char_traits<char>, std::__1::allocator<char>>> const&, unsigned char) + 244 frame #65: 0x00000001065e9c8c libleanshared.dylib`lean_main + 8348 frame #66: 0x0000000184f93f28 dyld`start + 2236 ``` cc @Kha

Commits

Commits on Apr 29, 2024

chore: disable #4006

chore: fix test