Skip to content

Conversation

@hargoniX
Copy link
Contributor

@hargoniX hargoniX commented Oct 28, 2025

This PR fixes a memleak caused by the Lean based IO.waitAny implementation by reverting it.

This the faulty Lean implementation:

def IO.waitAny (tasks : @& List (Task α)) (h : tasks.length > 0 := by exact Nat.zero_lt_succ _) :
    BaseIO α := do
  have : Nonempty α := ⟨tasks[0].get⟩
  let promise : IO.Promise α ← IO.Promise.new
  tasks.forM <| fun t => BaseIO.chainTask (sync := true) t promise.resolve
  return promise.result!.get

In a situation where we call this function repeatedly in a loop with a pair of tasks [t1, t2]
where t2 is a long lived task that we pass every time and t1 is fresh a short lived task, t2 will
accumlate more and more children from BaseIO.chainTask that fill memory over time. The old C++
implementation did not have this issue so we are reverting.

@hargoniX hargoniX requested a review from mhuisi as a code owner October 28, 2025 20:38
@hargoniX hargoniX added the changelog-compiler Compiler, runtime, and FFI label Oct 28, 2025
@hargoniX hargoniX requested a review from Kha October 28, 2025 20:58
@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 Oct 28, 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 19533ab1d4312903f98ff0429a5962db24ce402b --onto 3a42ee0c3060e2a8365927d205ead5990366053d. You can force Mathlib CI using the force-mathlib-ci label. (2025-10-28 21:59:02)

@leanprover-bot
Copy link
Collaborator

Reference manual CI status:

  • ❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase 19533ab1d4312903f98ff0429a5962db24ce402b --onto d3dda9f6d4428a906c096067ecb75e432afc4615. You can force reference manual CI using the force-manual-ci label. (2025-10-28 21:59:04)

@hargoniX hargoniX added this pull request to the merge queue Oct 29, 2025
Merged via the queue into master with commit 2cfd980 Oct 29, 2025
16 checks passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

changelog-compiler Compiler, runtime, and FFI 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.

4 participants