Prerequisites
Please put an X between the brackets as you perform the following steps:
Description
linux_wasm32 libleanrt.a seems to incorrectly refer to libuv symbols
Context
I have a project based on Thea Brick's lean2wasm which I'm trying to upgrade to the latest Lean toolchain. I'm running into some errors during the final emscripten build step.
Steps to Reproduce
$ git clone git@github.com:ianh/lean2wasm.git lean2wasm
$ cd lean2wasm
$ lake build test
$ lake exe lean2wasm
Expected behavior:
The project builds as it did with the older version.
Actual behavior:
The project fails to build. There are various errors, but the relevant errors to this issue are:
error: undefined symbol: uv_fs_mkdtemp (referenced by root reference (e.g. compiled C/C++ code))
warning: _uv_fs_mkdtemp may need to be added to EXPORTED_FUNCTIONS if it arrives from a system library
error: undefined symbol: uv_fs_mkstemp (referenced by root reference (e.g. compiled C/C++ code))
warning: _uv_fs_mkstemp may need to be added to EXPORTED_FUNCTIONS if it arrives from a system library
error: undefined symbol: uv_os_tmpdir (referenced by root reference (e.g. compiled C/C++ code))
warning: _uv_os_tmpdir may need to be added to EXPORTED_FUNCTIONS if it arrives from a system library
error: undefined symbol: uv_strerror (referenced by root reference (e.g. compiled C/C++ code))
warning: _uv_strerror may need to be added to EXPORTED_FUNCTIONS if it arrives from a system library
The code tries to avoid using libuv if LEAN_EMSCRIPTEN is defined, so I'm assuming the WebAssembly libleanrt.a linking these symbols is not expected.
Versions
Lean 4.15.0
macOS 14.6.1
emcc (Emscripten gcc/clang-like replacement + linker emulating GNU ld) 3.1.57-git
Additional Information
The reason I think libleanrt.a is the one referencing these symbols is because I get the following output on my own project, which has different build settings:
wasm-ld: error: toolchains/lean-4.15.0-linux_wasm32/lib/lean/libleanrt.a(io.cpp.o): undefined symbol: uv_strerror
wasm-ld: error: toolchains/lean-4.15.0-linux_wasm32/lib/lean/libleanrt.a(io.cpp.o): undefined symbol: uv_os_tmpdir
wasm-ld: error: toolchains/lean-4.15.0-linux_wasm32/lib/lean/libleanrt.a(io.cpp.o): undefined symbol: uv_strerror
wasm-ld: error: toolchains/lean-4.15.0-linux_wasm32/lib/lean/libleanrt.a(io.cpp.o): undefined symbol: uv_fs_mkstemp
wasm-ld: error: toolchains/lean-4.15.0-linux_wasm32/lib/lean/libleanrt.a(io.cpp.o): undefined symbol: uv_os_tmpdir
wasm-ld: error: toolchains/lean-4.15.0-linux_wasm32/lib/lean/libleanrt.a(io.cpp.o): undefined symbol: uv_strerror
wasm-ld: error: toolchains/lean-4.15.0-linux_wasm32/lib/lean/libleanrt.a(io.cpp.o): undefined symbol: uv_fs_mkdtemp
Impact
Impact to anyone using the WebAssembly toolchain.
Add 👍 to issues you consider important. If others are impacted by this issue, please ask them to add 👍 to it.
Prerequisites
Please put an X between the brackets as you perform the following steps:
https://github.com/leanprover/lean4/issues
Avoid dependencies to Mathlib or Batteries.
https://live.lean-lang.org/#project=lean-nightly
(You can also use the settings there to switch to “Lean nightly”)
Description
linux_wasm32 libleanrt.a seems to incorrectly refer to libuv symbols
Context
I have a project based on Thea Brick's lean2wasm which I'm trying to upgrade to the latest Lean toolchain. I'm running into some errors during the final emscripten build step.
Steps to Reproduce
Expected behavior:
The project builds as it did with the older version.
Actual behavior:
The project fails to build. There are various errors, but the relevant errors to this issue are:
The code tries to avoid using libuv if
LEAN_EMSCRIPTENis defined, so I'm assuming the WebAssembly libleanrt.a linking these symbols is not expected.Versions
Lean 4.15.0
macOS 14.6.1
emcc (Emscripten gcc/clang-like replacement + linker emulating GNU ld) 3.1.57-git
Additional Information
The reason I think libleanrt.a is the one referencing these symbols is because I get the following output on my own project, which has different build settings:
Impact
Impact to anyone using the WebAssembly toolchain.
Add 👍 to issues you consider important. If others are impacted by this issue, please ask them to add 👍 to it.