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

fix: make new codegen async realization-compatible #7316

Open
wants to merge 1 commit into
base: master
Choose a base branch
from

Conversation

Kha
Copy link
Member

@Kha Kha commented Mar 4, 2025

Follow-up to #7247

@Kha Kha added the changelog-no Do not include this PR in the release changelog label Mar 4, 2025
@Kha Kha requested a review from zwarich March 4, 2025 08:59
@Kha Kha requested a review from leodemoura as a code owner March 4, 2025 08:59
@github-actions github-actions bot added the toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN label Mar 4, 2025
@leanprover-community-bot
Copy link
Collaborator

Mathlib CI status (docs):

  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase f8f1b2212ace2db4153e4b06db550931b4f093e3 --onto e3c6909ad593e5a966a449df5e92abb1f0dbc317. (2025-03-04 09:24:12)

@zwarich
Copy link
Contributor

zwarich commented Mar 4, 2025

Putting this commit on top of master and then my new codegen branch causes a segfault during the stage2 build that is not obviously related to this change, but also nothing that I've seen before. I'll check that things still work as expected before the realizeConst changes and then try narrowing things down a bit more.

@zwarich
Copy link
Contributor

zwarich commented Mar 4, 2025

Yeah, putting this on top of 0a55f4bf (which is before new calls to realizeConst, I think) leads to a segfault during the stage2 build with this backtrace:

* thread #3, stop reason = EXC_BAD_ACCESS (code=1, address=0x200081313c66)
  * frame #0: 0x00000001063d9810 libleanshared.dylib`l_Array_uget___boxed + 56
    frame #1: 0x000000010b63f6e4 libleanshared.dylib`lean::ir::interpreter::call(lean::name const&, lean::array_ref<lean::object_ref> const&) + 540
    frame #2: 0x000000010b63d834 libleanshared.dylib`lean::ir::interpreter::eval_body(lean::object_ref const&) + 3040
    frame #3: 0x000000010b63f9ec libleanshared.dylib`lean::ir::interpreter::call(lean::name const&, lean::array_ref<lean::object_ref> const&) + 1316
    frame #4: 0x000000010b63d834 libleanshared.dylib`lean::ir::interpreter::eval_body(lean::object_ref const&) + 3040
    frame #5: 0x000000010b641a90 libleanshared.dylib`lean::ir::interpreter::stub_m(lean_object**) + 636
    frame #6: 0x000000010b6391bc libleanshared.dylib`lean_object* lean::ir::interpreter::with_interpreter<lean_object*>(lean::elab_environment const&, lean::options const&, lean::name const&, std::__1::function<lean_object* (lean::ir::interpreter&)> const&) + 320
    frame #7: 0x000000010b641624 libleanshared.dylib`lean::ir::interpreter::stub_m_aux(lean_object**) + 92
    frame #8: 0x000000010b641180 libleanshared.dylib`lean::ir::interpreter::stub_6_aux(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*) + 48
    frame #9: 0x000000010b656b48 libleanshared.dylib`lean_apply_2 + 896
    frame #10: 0x0000000109081cf8 libleanshared.dylib`l_Lean_Elab_liftMacroM___at_Lean_Elab_Tactic_evalTactic_expandEval___spec__1 + 1044

It seems that this is causing bad IR to be generated, written to an olean, and then executed later as part of a tactic.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
changelog-no Do not include this PR in the release changelog toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
Projects
None yet
Development

Successfully merging this pull request may close these issues.

3 participants