Skip to content

Commit

Permalink
chore: disable leanprover#4006 (leanprover#4021)
Browse files Browse the repository at this point in the history 
Mathlib is crashing with leanprover#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 leanprover#31: 0x00000001066f65d8 libleanshared.dylib`lean_apply_8 + 1252
    frame leanprover#32: 0x00000001066f5b6c libleanshared.dylib`lean_apply_7 + 1252
    frame leanprover#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 leanprover#34: 0x0000000104f59ec4 libleanshared.dylib`l___private_Lean_Elab_InfoTree_Main_0__Lean_Elab_withSavedPartialInfoContext___at_Lean_Elab_Command_liftTermElabM___spec__2___rarg + 280
    frame leanprover#35: 0x0000000104f5af20 libleanshared.dylib`l_Lean_Elab_Command_liftTermElabM___rarg___lambda__1 + 144
    frame leanprover#36: 0x00000001066f5ab8 libleanshared.dylib`lean_apply_7 + 1072
    frame leanprover#37: 0x0000000105636090 libleanshared.dylib`l_Lean_Elab_Term_TermElabM_run___rarg + 844
    frame leanprover#38: 0x0000000104f5b8fc libleanshared.dylib`l_Lean_Elab_Command_liftTermElabM___rarg + 1696
    frame leanprover#39: 0x000000010597d67c libleanshared.dylib`l_Array_forInUnsafe_loop___at_Lean_Elab_Command_elabAttr___spec__6 + 928
    frame leanprover#40: 0x000000010597de60 libleanshared.dylib`l_Lean_Elab_Command_elabAttr + 772
    frame leanprover#41: 0x000000010597e838 libleanshared.dylib`l_Lean_Elab_Command_elabAttr___boxed + 20
    frame leanprover#42: 0x00000001066f2cd4 libleanshared.dylib`lean_apply_3 + 868
    frame leanprover#43: 0x0000000104f385f8 libleanshared.dylib`l_Lean_Elab_withInfoTreeContext___at___private_Lean_Elab_Command_0__Lean_Elab_Command_elabCommandUsing___spec__2 + 396
    frame leanprover#44: 0x0000000104f39e48 libleanshared.dylib`l___private_Lean_Elab_Command_0__Lean_Elab_Command_elabCommandUsing + 484
    frame leanprover#45: 0x00000001066f2cf0 libleanshared.dylib`lean_apply_3 + 896
    frame leanprover#46: 0x0000000104f341d4 libleanshared.dylib`l_Lean_withTraceNode___at_Lean_Elab_Command_runLinters___spec__11 + 788
    frame leanprover#47: 0x00000001066f2d54 libleanshared.dylib`lean_apply_3 + 996
    frame leanprover#48: 0x00000001066f2cf0 libleanshared.dylib`lean_apply_3 + 896
    frame leanprover#49: 0x0000000104f40e30 libleanshared.dylib`l_Lean_Elab_withLogging___at_Lean_Elab_Command_elabCommand___spec__2 + 104
    frame leanprover#50: 0x0000000104f4c51c libleanshared.dylib`l_Lean_Elab_Command_elabCommandTopLevel___lambda__1 + 432
    frame leanprover#51: 0x00000001066f10e8 libleanshared.dylib`lean_apply_1 + 572
    frame leanprover#52: 0x0000000103bce27c libleanshared.dylib`l_Lean_profileitIOUnsafe___rarg___lambda__1 + 24
    frame leanprover#53: 0x0000000103bce4ec libleanshared.dylib`l_Lean_profileitIOUnsafe___rarg___lambda__1___boxed + 20
    frame leanprover#54: 0x00000001066f10bc libleanshared.dylib`lean_apply_1 + 528
    frame leanprover#55: 0x0000000106644260 libleanshared.dylib`lean_profileit + 128
    frame leanprover#56: 0x0000000103bce3e0 libleanshared.dylib`l_Lean_profileitIOUnsafe___rarg + 112
    frame leanprover#57: 0x0000000104f4fce0 libleanshared.dylib`l_Lean_Elab_Command_elabCommandTopLevel + 1284
    frame leanprover#58: 0x00000001057d2f30 libleanshared.dylib`l_Lean_Elab_Frontend_elabCommandAtFrontend + 1384
    frame leanprover#59: 0x00000001057d63b8 libleanshared.dylib`l_Lean_Elab_Frontend_processCommand + 1332
    frame leanprover#60: 0x00000001057d6e48 libleanshared.dylib`l_Lean_Elab_Frontend_processCommands + 72
    frame leanprover#61: 0x00000001057d7248 libleanshared.dylib`l_Lean_Elab_IO_processCommands + 212
    frame leanprover#62: 0x00000001057d83d0 libleanshared.dylib`l_Lean_Elab_runFrontend___lambda__3 + 76
    frame leanprover#63: 0x00000001057d96d0 libleanshared.dylib`lean_run_frontend + 2436
    frame leanprover#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 leanprover#65: 0x00000001065e9c8c libleanshared.dylib`lean_main + 8348
    frame leanprover#66: 0x0000000184f93f28 dyld`start + 2236
```

cc @Kha
  • Loading branch information
@leodemoura
leodemoura authored Apr 29, 2024
1 parent 15cfe60 commit 4b88965
Show file tree
Hide file tree
Showing 2 changed files with 6 additions and 2 deletions.
5 changes: 4 additions & 1 deletion src/library/constructions/projection.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -99,7 +99,10 @@ environment mk_projections(environment const & env, name const & n, buffer<name>
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
Expand Down
3 changes: 2 additions & 1 deletion tests/lean/run/2575.lean
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down

0 comments on commit 4b88965

Please sign in to comment.