Skip to content

feat: teardown libuv - #15668

Open
algebraic-dev wants to merge 7 commits into
sofia/fix-task-sync-deadlockfrom
sofia/uv-exit-teardown
Open

algebraic-dev wants to merge 7 commits into
sofia/fix-task-sync-deadlockfrom
sofia/uv-exit-teardown

Conversation

@algebraic-dev

@algebraic-dev algebraic-dev commented Oct 13, 2026 •

Copy link
Copy Markdown
Member

This PR tears down the libuv event loop when a program returns from main, once its running tasks have finished:

  • every handle is closed.
  • in-flight requests complete or are cancelled
  • the runtime now uses its own uv_loop_t instead of uv_default_loop() so every handle on the loop belongs to it.
  • lean_init_task_manager after a finalization starts a fresh loop and loop thread
  • every libuv entry point fails with UV_ECANCELED while the loop is torn down

These changes fixes crashes at exit when a libuv callback ran during runtime shutdown.

@algebraic-dev
algebraic-dev requested a review from TwoFX as a code owner October 13, 2026 23:08
@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 13, 2026
@algebraic-dev
algebraic-dev force-pushed the sofia/uv-exit-teardown branch 2 times, most recently from 3278e49 to 5efb15a Compare October 14, 2026 12:21
@algebraic-dev
algebraic-dev force-pushed the sofia/uv-exit-teardown branch 3 times, most recently from 8f6eef1 to 2d338b5 Compare October 15, 2026 14:51
@algebraic-dev
algebraic-dev removed this pull request from stack #15595 October 23, 2026 15:59
@algebraic-dev
algebraic-dev changed the base branch from sofia/uv-fix-signal to sofia/fix-task-sync-deadlock October 23, 2026 16:01
@algebraic-dev
algebraic-dev force-pushed the sofia/uv-exit-teardown branch from 2d338b5 to 150404c Compare October 23, 2026 17:01
@algebraic-dev
algebraic-dev force-pushed the sofia/uv-exit-teardown branch from 150404c to 493dac2 Compare October 23, 2026 19:46
@algebraic-dev
algebraic-dev requested a review from kim-em as a code owner October 25, 2026 13:08
@algebraic-dev
algebraic-dev force-pushed the sofia/uv-exit-teardown branch from 493dac2 to 5a6d8fd Compare October 25, 2026 13:25
@algebraic-dev algebraic-dev added awaiting-review Waiting for someone to review the PR release-ci Enable all CI checks for a PR, like is done for releases labels Oct 27, 2026
@algebraic-dev
algebraic-dev force-pushed the sofia/uv-exit-teardown branch from eb80a43 to cdaf7ae Compare October 27, 2026 18:04
@algebraic-dev
algebraic-dev force-pushed the sofia/uv-exit-teardown branch from cdaf7ae to e1a7957 Compare October 28, 2026 01:59

This branch has not been deployed

No deployments
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

awaiting-review Waiting for someone to review the PR changelog-library Library release-ci Enable all CI checks for a PR, like is done for releases 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.

1 participant