fix: match stub signature of lean_uv_dns_get_info to real implementation#13234
Merged
hargoniX merged 1 commit intoleanprover:masterfrom Apr 7, 2026
Merged
Conversation
The non-libuv stub of lean_uv_dns_get_info (in the #else branch for builds without libuv) has a 4-parameter signature including int8_t protocol, but the real implementation above the #else has only 3 parameters (name, service, family). The Lean @[extern] declaration also expects 3 parameters. This mismatch means the stub has never matched the real function's ABI. Remove the extra protocol parameter so both branches agree. Discovered while building Lean4 to WASM via Emscripten, where the stub branch is compiled. The fix has been in production use since v4.27.0.
github-actions
bot
added
the
toolchain-available
|
Mathlib CI status (docs):
|
Collaborator
|
Reference manual CI status:
|
hargoniX
approved these changes
Apr 7, 2026
wkrozowski
pushed a commit
to wkrozowski/lean4
that referenced
this pull request
Apr 10, 2026
…ion (leanprover#13234) This PR fixes a build issue when Lean is not linked against libuv. ## Problem In `src/runtime/uv/dns.cpp`, the non-libuv stub of `lean_uv_dns_get_info` (in the `#else` branch, compiled when building without libuv) has a **4-parameter** signature: ```cpp lean_uv_dns_get_info(b_obj_arg name, b_obj_arg service, uint8_t family, int8_t protocol) ``` But the real implementation above the `#else` has only **3 parameters**: ```cpp lean_uv_dns_get_info(b_obj_arg name, b_obj_arg service, uint8_t family) ``` The Lean `@[extern]` declaration also expects 3 parameters. The stub has an extra `int8_t protocol` parameter that the real function and the Lean FFI caller do not use. ## Fix Remove the extra `protocol` parameter from the stub so both branches have the same signature. ## Evidence Discovered while building Lean4 to WASM via Emscripten for a production project ([specify-lean](https://github.com/kjsdesigns/specify)) since v4.27.0. The stub branch is compiled in this configuration, and the signature mismatch was caught at link time. The fix has been stable in production across multiple Lean version bumps. Related: [Zulip thread on WASM build fixes](https://leanprover.zulipchat.com/#narrow/channel/270676-lean4/topic/WASM.20build.20fixes.3A.20libuv.20symbol.20leakage.20.28.236817.29.20and.20unique_lo/with/580836892) (2026-03-21). Co-authored-by: Keith Seim <keith@MacBook-Pro.local>
volodeyka
pushed a commit
that referenced
this pull request
Apr 16, 2026
…ion (#13234) This PR fixes a build issue when Lean is not linked against libuv. ## Problem In `src/runtime/uv/dns.cpp`, the non-libuv stub of `lean_uv_dns_get_info` (in the `#else` branch, compiled when building without libuv) has a **4-parameter** signature: ```cpp lean_uv_dns_get_info(b_obj_arg name, b_obj_arg service, uint8_t family, int8_t protocol) ``` But the real implementation above the `#else` has only **3 parameters**: ```cpp lean_uv_dns_get_info(b_obj_arg name, b_obj_arg service, uint8_t family) ``` The Lean `@[extern]` declaration also expects 3 parameters. The stub has an extra `int8_t protocol` parameter that the real function and the Lean FFI caller do not use. ## Fix Remove the extra `protocol` parameter from the stub so both branches have the same signature. ## Evidence Discovered while building Lean4 to WASM via Emscripten for a production project ([specify-lean](https://github.com/kjsdesigns/specify)) since v4.27.0. The stub branch is compiled in this configuration, and the signature mismatch was caught at link time. The fix has been stable in production across multiple Lean version bumps. Related: [Zulip thread on WASM build fixes](https://leanprover.zulipchat.com/#narrow/channel/270676-lean4/topic/WASM.20build.20fixes.3A.20libuv.20symbol.20leakage.20.28.236817.29.20and.20unique_lo/with/580836892) (2026-03-21). Co-authored-by: Keith Seim <keith@MacBook-Pro.local>
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
3 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 fixes a build issue when Lean is not linked against libuv.
Problem
In
src/runtime/uv/dns.cpp, the non-libuv stub oflean_uv_dns_get_info(in the#elsebranch, compiled when building without libuv) has a 4-parameter signature:But the real implementation above the
#elsehas only 3 parameters:The Lean
@[extern]declaration also expects 3 parameters. The stub has an extraint8_t protocolparameter that the real function and the Lean FFI caller do not use.Fix
Remove the extra
protocolparameter from the stub so both branches have the same signature.Evidence
Discovered while building Lean4 to WASM via Emscripten for a production project (specify-lean) since v4.27.0. The stub branch is compiled in this configuration, and the signature mismatch was caught at link time. The fix has been stable in production across multiple Lean version bumps.
Related: Zulip thread on WASM build fixes (2026-03-21).