From ba33c3daa42b5cfb194e31dc5ca855307a84c1f2 Mon Sep 17 00:00:00 2001 From: Keith Seim Date: Tue, 7 Apr 2026 05:39:53 -0400 Subject: [PATCH] fix: match stub signature of lean_uv_dns_get_info to real implementation (#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 --- src/runtime/uv/dns.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/runtime/uv/dns.cpp b/src/runtime/uv/dns.cpp index d49a6a4e90..02ab27bdbd 100644 --- a/src/runtime/uv/dns.cpp +++ b/src/runtime/uv/dns.cpp @@ -173,7 +173,7 @@ extern "C" LEAN_EXPORT lean_obj_res lean_uv_dns_get_name(b_obj_arg addr) { #else // Std.Internal.IO.Async.DNS.getAddrInfo (host service : @& String) (family : UInt8) : IO (IO.Promise (Except IO.Error (Array IPAddr))) -extern "C" LEAN_EXPORT lean_obj_res lean_uv_dns_get_info(b_obj_arg name, b_obj_arg service, uint8_t family, int8_t protocol) { +extern "C" LEAN_EXPORT lean_obj_res lean_uv_dns_get_info(b_obj_arg name, b_obj_arg service, uint8_t family) { lean_always_assert( false && ("Please build a version of Lean4 with libuv to invoke this.") );