Skip to content

fix: prevent Loop.configure leaks and System.random size limits, Loop.alive and system error handling - #15175

Open
algebraic-dev wants to merge 5 commits into
masterfrom
sofia/libuv-loop-system-fixes
Open

algebraic-dev wants to merge 5 commits into
masterfrom
sofia/libuv-loop-system-fixes

Conversation

@algebraic-dev

Copy link
Copy Markdown
Member

This PR stops Loop.configure from leaking and rejects System.random values above 2^31-1 before allocating a huge array.

algebraic-dev and others added 3 commits September 15, 2026 12:16
This PR fixes Std.Internal.UV.Loop.configure, which leaked its options on every call and could not report errors; it now has type IO Unit.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
This PR makes Std.Internal.UV.System.random fail with UV_E2BIG for sizes above 2^31-1 instead of aborting the process.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
@algebraic-dev algebraic-dev self-assigned this Sep 16, 2026
@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 Sep 16, 2026
@algebraic-dev algebraic-dev added the awaiting-review Waiting for someone to review the PR label Sep 16, 2026
`Loop.alive` now returns `false` when nothing is pending, instead of always counting the handle that wakes the loop. `System.osHomedir`, `System.osTmpdir` and `System.cwd` return values longer than `PATH_MAX` instead of failing, `System.osSetPriority` rejects priorities outside the C `int` range instead of wrapping them, and a failing `System.osEnviron` raises a proper `IO.Error`.

Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
@algebraic-dev algebraic-dev changed the title fix: stop Loop.configure from leaking and System.randomsize limit fix: prevent Loop.configure leaks and System.random size limits, fix Loop.alive and system error handling Sep 17, 2026
@algebraic-dev algebraic-dev changed the title fix: prevent Loop.configure leaks and System.random size limits, fix Loop.alive and system error handling fix: prevent Loop.configure leaks and System.random size limits, Loop.alive and system error handling Sep 17, 2026
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>

@Chessing234 Chessing234 left a comment

Copy link
Copy Markdown

Choose a reason for hiding this comment

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

the @& Options + IO return type change for Loop.configure looks like the right fix for the exclusive-object leak, and the compile test checking isExclusiveUnsafe after configure is good evidence.

on the run_loop rewrite: holding the mutex across the uv_loop_alive check (with the note about lean_uv_event_loop_alive unreferencing async) seems necessary. one thing to double-check — removing async_callback/uv_stop means the only wake path is uv_async_send plus UV_RUN_ONCE returning; worth confirming a waiter that arrives while uv_run is inside a long callback still gets the mutex promptly (i.e. that async still interrupts that wait).

didn't rebuild the uv tests locally.

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 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.

2 participants