Skip to content

fix: make new codegen async realization-compatible#7316

Merged
Kha merged 1 commit intoleanprover:masterfrom
Kha:push-pyvwsznlknru
Apr 1, 2025
Merged

fix: make new codegen async realization-compatible#7316
Kha merged 1 commit intoleanprover:masterfrom
Kha:push-pyvwsznlknru

Conversation

@Kha
Copy link
Copy Markdown
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
@ghost
Copy link
Copy Markdown

ghost commented Mar 4, 2025 •
edited by ghost
Loading

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)
  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 911ea07a73733650eefa5240652404856bdcceb7 --onto 2edfe2e9cffd55e3c79291628ae091b942291ec9. You can force Mathlib CI using the force-mathlib-ci label. (2025-04-01 08:10:38)
  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 9c6c54107f19cf36f539408178faa5137ae7d25d --onto 2edfe2e9cffd55e3c79291628ae091b942291ec9. You can force Mathlib CI using the force-mathlib-ci label. (2025-04-01 16:00:31)

@zwarich
Copy link
Copy Markdown
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
Copy Markdown
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.

zwarich
zwarich approved these changes Apr 1, 2025
View reviewed changes
Copy link
Copy Markdown
Contributor

@zwarich zwarich left a comment

Choose a reason for hiding this comment

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

With this (and using a stage0 update commit instead of going stage1 -> stage2 like I was used to), I'm able to rebase up to a few days ago, right before the Lake changes in 2d28331. There are some new test failures, but I don't think they're due to this.

@zwarich zwarich enabled auto-merge April 1, 2025 00:15
@Kha Kha force-pushed the push-pyvwsznlknru branch from 5c5857b to 3e748e7 Compare April 1, 2025 07:44
@zwarich zwarich added this pull request to the merge queue Apr 1, 2025
auto-merge was automatically disabled April 1, 2025 08:14

Pull Request is not mergeable

@github-merge-queue github-merge-queue bot removed this pull request from the merge queue due to failed status checks Apr 1, 2025
@Kha Kha force-pushed the push-pyvwsznlknru branch from 3e748e7 to d4dcf0b Compare April 1, 2025 15:39
@Kha Kha enabled auto-merge April 1, 2025 15:39
@Kha Kha added this pull request to the merge queue Apr 1, 2025
Merged via the queue into leanprover:master with commit 8b1caa3 Apr 1, 2025
15 checks passed
@Kha Kha deleted the push-pyvwsznlknru branch April 2, 2025 08:27
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@leodemoura leodemoura Awaiting requested review from leodemoura leodemoura is a code owner

1 more reviewer

@zwarich zwarich zwarich approved these changes

Reviewers whose approvals may not affect merge requirements

Assignees

No one assigned

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

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

2 participants

@Kha @zwarich