fix: guard libuv symbols in io.cpp for Emscripten WASM builds (#6817)#13298
Open
kjsdesigns wants to merge 1 commit intoleanprover:masterfrom
Open
fix: guard libuv symbols in io.cpp for Emscripten WASM builds (#6817)#13298kjsdesigns wants to merge 1 commit intoleanprover:masterfrom
kjsdesigns wants to merge 1 commit intoleanprover:masterfrom
Conversation
The linux_wasm32 libleanrt.a release artifact contains unresolved references to uv_strerror, uv_os_tmpdir, uv_fs_mkstemp, and uv_fs_mkdtemp (issue leanprover#6817). These symbols are called from lean_decode_uv_error, lean_io_create_tempfile, and lean_io_create_tempdir, which are compiled into the WASM artifact even though they cannot function in a browser environment. This commit adds #if defined(LEAN_EMSCRIPTEN) guards following the same pattern already used in src/runtime/uv/dns.cpp (PR leanprover#9258): - lean_decode_uv_error: provides a numeric fallback error string instead of calling uv_strerror, since the rest of the function (error classification via UV_* constants) works without libuv - lean_io_create_tempfile: returns unsupported operation error in Emscripten (no filesystem temp directory in browser WASM) - lean_io_create_tempdir: same treatment as createTempFile Discovered and proven in a production project that builds a Lean module to WASM via Emscripten. The equivalent fix has been running in production since Lean v4.27.0. Closes leanprover#6817
github-actions
Bot
added
the
toolchain-available
|
Mathlib CI status (docs):
|
Collaborator
|
Reference manual CI status:
|
Contributor
Author
|
Could a maintainer please add the I've also updated the PR body to follow the changelog convention (starts with "This PR ..."). |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
This PR guards libuv symbols in
src/runtime/io.cppbehind#if defined(LEAN_EMSCRIPTEN)to fix unresolved references touv_strerror,uv_os_tmpdir,uv_fs_mkstemp, anduv_fs_mkdtempin thelinux_wasm32libleanrt.arelease artifact (issue #6817).Details
Adds
#if defined(LEAN_EMSCRIPTEN)guards following the same pattern already used insrc/runtime/uv/dns.cpp(PR #9258):lean_decode_uv_error: provides a numeric fallback error string ("libuv error %d") instead of callinguv_strerror. The rest of the function (error classification viaUV_*constants fromuv.h) is unchanged and works without linking libuv.lean_io_create_tempfile: returns an unsupported operation error in Emscripten (no filesystem temp directory in browser WASM).lean_io_create_tempdir: same treatment ascreateTempFile.How I know it works
I've been using an equivalent patch in a production project that builds a Lean module to WASM via Emscripten since v4.27.0. The fix eliminates the 4 unresolved symbols without affecting any other code paths.
Context
Discussed on Zulip: #lean4 > WASM build fixes: libuv symbol leakage (#6817) and unique_lock
Closes #6817