Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Azure Pipelines CI + Windows fixes #16

Merged
merged 7 commits into from
Jul 5, 2019
Merged

Azure Pipelines CI + Windows fixes #16

merged 7 commits into from
Jul 5, 2019

Conversation

Kha
Copy link
Member

@Kha Kha commented Jun 30, 2019

No description provided.

@Kha Kha merged commit 16f3e48 into leanprover:master Jul 5, 2019
size_t mpz::get_size_t() const {
static_assert(sizeof(size_t) <= sizeof(mp_limb_t), "GMP word size should be not greater than system word size");
return static_cast<size_t>(mpz_getlimbn(m_val, 0));
}
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I am assuming is_size_t() must hold here. Then, we have

is_nonneg() && mpz_size(m_val) * sizeof(mp_limb_t) <= sizeof(size_t);

So, the code above seems incorrect if, for example, we have

is_nonneg() == true
mpz_size(m_val) == 2
sizeof(mp_limb_t) == 4
sizeof(size_t) == 8

Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

It seems the code above is only correct when sizeof(mp_limb_t) == sizeof(size_t)

Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Your example does not seem to fulfill the static_assert. However, I see that I did screw up the ordering in the message.

Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

My point is that the conditions I listed satisfy is_size_t.
It is not acceptable for get_size_t to fail if is_size_t is satisfied.

Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

But the function cannot fail in this case - the code would refuse to compile in the first place because of the static_assert. Yes, it would be nicer to have higher-level code that works on all imaginable platforms, but GMP only gives us unsigned long accessors. So either we add a messy ifdef for sizeof(unsigned long) < sizeof(size_t) platforms with some shifts generating suboptimal code, or we use this one direct access that CI tells us is safe on all platforms we're interested in. It is possible that the definition of mp_limb_t will change in the future, but I would argue the chance of this being incredibly low - and even then we will immediately know and can fix that line.

Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

But the function cannot fail in this case - the code would refuse to compile in the first place because of the static_assert

Fail to compile is bad in this case since the current static_assert does not make sense. One would get the failure and then would find a mismatch between is_size_t and get_size_t. This must be fixed.

Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Yes, it would be nicer to have higher-level code that works on all imaginable platforms, but GMP only gives us unsigned long accessors. So either we add a messy ifdef for sizeof(unsigned long) < sizeof(size_t) platforms with some shifts generating suboptimal code

I am confused now. I thought you started to make these changes because on Windows sizeof(unsigned long) < sizeof(size_t). So, as far as I can tell, this is already an issue. Or, is sizeof(mp_limb_t) == sizeof(size_t) on Windows?

Copy link
Member Author

@Kha Kha Jul 5, 2019

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I'm not sure if you were referring to this, but I now see one potential in is_size_t on a hypothetical platform: if sizeof(size_t) < sizeof(mp_limb_t), it would always return false for any positive value. So, here are the solutions I can see right now:

  • I assume sizeof(mp_limb_t) == sizeof(size_t) in both functions and simplify is_size_t to is_nonneg() && mpz_size(m_val) <= 1.
  • I completely avoid mp_limb_t and reimplement both functions with generic but ugly and suboptimal code.

Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

My problem is that the implementation of is_size_t does not match the static_assert at get_size_t.

I assume sizeof(mp_limb_t) == sizeof(size_t) in both functions and simplify is_size_t to is_nonneg() && mpz_size(m_val) <= 1.

Yes, this is a reasonable solution, and we add a static_assert to both functions.

BTW, does static_cast<size_t>(mpz_getlimbn(m_val, 0)) behave correctly when mpz_size(m_val) == 0?

else
return mk_nat_obj_core(m);
}

inline obj_res mk_nat_obj(usize n) {
inline obj_res unsigned_to_nat(usize n) {
if (n <= LEAN_MAX_SMALL_NAT) {
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Why didn't you name it usize_to_nat?

@@ -1237,7 +1232,7 @@ inline obj_res byte_array_set(obj_arg a, b_obj_arg i, uint8 b) {
// uint8
uint8 uint8_of_big_nat(b_obj_arg a);
inline uint8 uint8_of_nat(b_obj_arg a) { return is_scalar(a) ? static_cast<uint8>(unbox(a)) : uint8_of_big_nat(a); }
inline obj_res uint8_to_nat(uint8 a) { return mk_nat_obj(static_cast<usize>(a)); }
inline obj_res uint8_to_nat(uint8 a) { return unsigned_to_nat(static_cast<usize>(a)); }
inline uint8 uint8_add(uint8 a1, uint8 a2) { return a1+a2; }
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

The new and old code seems to be suboptimal here. unsigned_to_nat will perform an unnecessary test. Well, perhaps the compiler will be smart enough to remove it after inlining.

Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

If both are inlined into the same function, the branch will definitely be optimized away. Well, we could get unlucky and have LLVM inline only the outer function, but in that case the overall overhead from that is probably relatively large in general.

ChrisHughes24 pushed a commit to ChrisHughes24/lean4 that referenced this pull request Dec 2, 2022
leodemoura added a commit that referenced this pull request Apr 29, 2024
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<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
github-merge-queue bot pushed a commit that referenced this pull request Apr 29, 2024
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<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
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

2 participants