Emscripten libuv stub definitions do not match their declarations

Prerequisites

• Check that this issue has not already been filed.
• Reduce the issue to a minimal, self-contained reproduction without Mathlib or Batteries.
• Test the reproduction against the current master branch.

Description

While trying to build the Lean runtime as WebAssembly using Emscripten, I found that two UV runtime stub definitions selected by LEAN_EMSCRIPTEN do not match their header declarations:

1. lean_uv_event_loop_alive is declared to return uint8_t, but its Emscripten stub returns lean_obj_res.
2. lean_uv_os_get_group is declared with a uint64_t gid parameter, but its Emscripten stub takes no parameters.

These mismatches produce C++ conflicting-type errors when compiling the Lean runtime for Emscripten.

Context

The non-Emscripten implementations have signatures that agree with their header declarations. Only the fallback implementations selected by LEAN_EMSCRIPTEN are inconsistent.

The history suggests that the lean_uv_event_loop_alive mismatch remained after the zero-cost BaseIO FFI changes in #10625: the non-Emscripten implementation was changed to return uint8_t, while the Emscripten stub retained its previous return type.

The lean_uv_os_get_group mismatch appears to have been introduced with the system information functions in #8109: the regular implementation has the gid parameter, while the Emscripten stub does not.

#6817 is also related to building the runtime for WebAssembly without libuv, but it reports different unresolved libuv symbols rather than these declaration mismatches.

Steps to Reproduce

Clone the current Lean repository:

git clone https://github.com/leanprover/lean4
cd lean4

Configure a runtime build using Emscripten:

emcmake cmake src \
  -B build/emscripten-probe \
  -G "Unix Makefiles" \
  -DSTAGE=0 \
  -DUSE_GITHASH=OFF \
  -DUSE_GMP=OFF \
  -DUSE_MIMALLOC=OFF \
  -DMMAP=OFF \
  -DMULTI_THREAD=OFF \
  -DUSE_LAKE=OFF \
  -DCMAKE_BUILD_TYPE=Release

Build leanrt:

cmake --build build/emscripten-probe --target leanrt -j 4

The build first fails on lean_uv_event_loop_alive:

src/runtime/uv/event_loop.cpp:149:37: error: conflicting types for
'lean_uv_event_loop_alive'

src/runtime/uv/event_loop.h:48:32: note: previous declaration is here

Both errors can be reproduced independently after the configure step:

em++ -std=c++17 \
  -DLEAN_EMSCRIPTEN \
  -Ibuild/emscripten-probe/include \
  -Isrc \
  -Isrc/include \
  -fsyntax-only \
  src/runtime/uv/event_loop.cpp

em++ -std=c++17 \
  -DLEAN_EMSCRIPTEN \
  -Ibuild/emscripten-probe/include \
  -Isrc \
  -Isrc/include \
  -fsyntax-only \
  src/runtime/uv/system.cpp

The second command reports:

src/runtime/uv/system.cpp:637:37: error: conflicting types for
'lean_uv_os_get_group'

src/runtime/uv/system.h:26:37: note: previous declaration is here

Expected behavior: The Emscripten stub definitions have the same C ABI as their headers and the corresponding Lean extern declarations, and leanrt compiles successfully.

Actual behavior: The definitions have incompatible return types or parameters, preventing leanrt from compiling.

Versions

Observed in:

• Lean master at 2a5b1a2f7ec519ab9f6196acd8c8e735c7e5a2b2
• Lean v4.34.0-rc2
• Lean v4.33.1
• Lean v4.31.0
• Emscripten 5.0.6
• macOS 15.6 on Apple Silicon

Additional Information

The corresponding Lean declarations are:

@[extern "lean_uv_event_loop_alive"]
opaque alive : BaseIO Bool

@[extern "lean_uv_os_get_group"]
opaque osGetGroup : UInt64 → IO (Option GroupInfo)

A minimal correction would be to:

• make the Emscripten lean_uv_event_loop_alive stub return uint8_t;
• return false because no event loop is available; and
• make the Emscripten lean_uv_os_get_group stub accept and ignore uint64_t gid before reaching the existing unsupported-operation assertion.

Impact

The Lean runtime cannot be built for Emscripten from an unmodified Lean source tree.

AI Assistance Disclosure

Generative AI was used to assist with investigating the issue, checking affected versions, and drafting this report. I manually reviewed the reproduction steps and the report before submission.

Start with the declarations in src/runtime/uv/event_loop.h and system.h, then compare the LEAN_EMSCRIPTEN definitions in src/runtime/uv/event_loop.cpp and system.cpp. Configure the runtime with emcmake as described and run the two em++ syntax checks first. Done means the stub signatures match their headers and leanrt builds successfully for Emscripten.