From 4b8896536388864527c640801318f0cc51172a12 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 29 Apr 2024 12:58:11 +0200 Subject: [PATCH] chore: disable #4006 (#4021) Mathlib is crashing with #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 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 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 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::environment const&, lean::options const&, lean::name const&, std::__1::function 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, std::__1::allocator> const&, lean::options const&, std::__1::basic_string, std::__1::allocator> const&, lean::name const&, unsigned int, lean::optional, std::__1::allocator>> const&, unsigned char) + 244 frame #65: 0x00000001065e9c8c libleanshared.dylib`lean_main + 8348 frame #66: 0x0000000184f93f28 dyld`start + 2236 ``` cc @Kha --- src/library/constructions/projection.cpp | 5 ++++- tests/lean/run/2575.lean | 3 ++- 2 files changed, 6 insertions(+), 2 deletions(-) diff --git a/src/library/constructions/projection.cpp b/src/library/constructions/projection.cpp index b9b964474463..4ba99d67bcbe 100644 --- a/src/library/constructions/projection.cpp +++ b/src/library/constructions/projection.cpp @@ -99,7 +99,10 @@ environment mk_projections(environment const & env, name const & n, buffer expr proj_val = mk_proj(n, i, c); proj_val = lctx.mk_lambda(proj_args, proj_val); declaration new_d; - if (is_prop) { + // TODO: replace `if (false) {` with `if (is_prop) {`. + // Mathlib is crashing when prop fields are theorems. + // The crash is in the ir_interpreter. Kyle suspects this is an use-after-free bug in the interpreter. + if (false) { // if (is_prop) { bool unsafe = use_unsafe(env, proj_type) || use_unsafe(env, proj_val); if (unsafe) { // theorems cannot be unsafe diff --git a/tests/lean/run/2575.lean b/tests/lean/run/2575.lean index c6d6f947c629..0ab4e8b299cb 100644 --- a/tests/lean/run/2575.lean +++ b/tests/lean/run/2575.lean @@ -4,8 +4,9 @@ structure AtLeastThirtySeven where theorem AtLeastThirtySeven.lt (x : AtLeastThirtySeven) : 36 < x.val := x.le +-- TODO: fix /-- -info: theorem AtLeastThirtySeven.le : ∀ (self : AtLeastThirtySeven), 37 ≤ self.val := +info: def AtLeastThirtySeven.le : ∀ (self : AtLeastThirtySeven), 37 ≤ self.val := fun self => self.2 -/ #guard_msgs in