Skip to content

feat: finalize libuv thread#14037

Draft
algebraic-dev wants to merge 3 commits into
masterfrom
sofia/finalize-libuv-thread
Draft

feat: finalize libuv thread#14037
algebraic-dev wants to merge 3 commits into
masterfrom
sofia/finalize-libuv-thread

Conversation

@algebraic-dev

@algebraic-dev algebraic-dev commented Jun 12, 2026

Copy link
Copy Markdown
Member

his PR finalizes all the handles, destroys all objects, and destroys the lthread that runs event_loop before task_manager is null. It also adds safeguards so we can check if the libuv thread died when a Task accesses libuv during the interval in which it is finalizing.

As a future PR, as the code gets more and more complicated, I want to make a PR adding a libuv_loop class and RAII safety guards to lock and unlock libuv.

Kha and others added 2 commits June 10, 2026 12:18
This PR moves task-manager teardown out of the shell's RAII `scoped_task_manager` and into the runtime's `finalize()`, where it now runs after a new `finalize_libuv` hook so that libuv is finalized before the task-manager worker pool is drained.

The shell and the compiler-generated `main` already initialize the task manager explicitly (they need the thread count, which is only known after option parsing), so `scoped_task_manager` is removed and the shell relies on the `initializer` destructor for finalization. `finalize_libuv` is currently a documented no-op stub matching the prior behaviour where libuv was never finalized; only the ordering is wired up, leaving a real libuv shutdown to be slotted in ahead of the drain. The `-j0` (no task manager) semantics are unchanged.

Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
@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 Jun 12, 2026
@leanprover-bot

Copy link
Copy Markdown
Collaborator

Reference manual CI status:

  • ❗ Reference manual CI can not be attempted yet, as the nightly-testing-2026-06-09 tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto nightly-with-manual, reference manual CI should run now. You can force reference manual CI using the force-manual-ci label. (2026-06-12 22:49:59)

@github-actions github-actions Bot added the mathlib4-nightly-available A branch for this PR exists at leanprover-community/mathlib4-nightly-testing:lean-pr-testing-NNNN label Jun 12, 2026
@mathlib-lean-pr-testing

Copy link
Copy Markdown

Mathlib CI status (docs):

@mathlib-lean-pr-testing mathlib-lean-pr-testing Bot added the builds-mathlib CI has verified that Mathlib builds against this PR label Jun 12, 2026
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

builds-mathlib CI has verified that Mathlib builds against this PR changelog-library Library mathlib4-nightly-available A branch for this PR exists at leanprover-community/mathlib4-nightly-testing:lean-pr-testing-NNNN 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