max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

fix: match stub signature of lean_uv_dns_get_info to real implementation (#13234)

Browse source 
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 commit is contained in:
Keith Seim 2026-04-07 05:39:53 -04:00 • committed by GitHub
parent db1e2ac34c
commit ba33c3daa4
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/runtime/uv/dns.cpp
View file

@ -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.")
);