RFC: re-enable the Web Assembly CI job #16134

Proposal

I propose to re-enable the Web Assembly job in ci.yml as a secondary, test-only job for nightlies, releases and release-ci runs (check level 2 and up), so that changes that break the WebAssembly build are noticed again. It would not (yet) gate merges, nightlies or releases, and it would not (yet) ship a linux_wasm32 archive. The changes are in the stack of PRs:

• PR: fix: return the right exit code from lean on 32-bit targets #16137.
  Issue: lean --version, --run and other options exit with a garbage code on 32-bit targets #16136.
• PR: fix: match the parameters of eight FFI definitions to the generated C #16090.
  Issue: Eight FFI definitions have the wrong number of parameters, so calls to them can trap on WebAssembly #16089.
• PR: chore: re-enable the Web Assembly CI job #16135.
• PR: chore: update the Web Assembly CI job to Emscripten 6.0.13 #16142.
• PR: perf: resolve native symbols inside lean.wasm instead of exporting all of Lean #16149.
• PR: chore: run more of the test suite on the Web Assembly job #16191.

Background

#6424 disabled the job on 2024-12-20. That day's nightly built lean.wasm, but its tests failed because V8 rejected the module: exports count of 100019 exceeds internal limit of 100000. lean.js is linked with -s EXPORT_ALL=1, so that the interpreter can find compiled code with dlsym, and the number of exports grows with the library. V8 raised the limit to 1,000,000 in December 2024 (v8/v8@285bfe195f), and Node.js has included that change since version 24. Today's lean.wasm has 251,027 exports: Node.js 26 loads it, while the runner's default Node.js 22 still rejects it with the same error, exports count of 251027 exceeds internal limit of 100000.

Since v4.15.0 (2025-01-04), the last release with a linux_wasm32 archive, nothing upstream has built Lean for WebAssembly, and breakage has only been found downstream, for example #14973 and #15181 (Emscripten libuv stubs that no longer matched their declarations), #13952 (a C++ declaration of an exported Lean function with the wrong parameter type, which made initialization trap), #15816 (LEAN_SCALAR_PTR_LITERAL chosen by LEAN_EMSCRIPTEN instead of by pointer size) and #16089 (eight FFI definitions with the wrong number of parameters, which make lean.js trap during initialization). On master, the WebAssembly build currently fails: the runtime does not compile, as IO.FS.renameIfNew uses renameat2, and Lake builds Leanc, whose source CMake does not generate for Emscripten. The lean launcher for lean.js is also no longer generated, and Lake archives the WebAssembly libraries without a symbol index.

The stack of PRs mentioned above fixes these issues and a few other problems.

Why?

• User Experience: People who run Lean on WebAssembly run into fewer regressions: CI builds lean.js and runs about 180 tests with it under Node.js, the ones whose behaviour depends on the platform, so it catches changes to the runtime, the FFI or the build that break the WebAssembly build or make one of those tests fail, instead of users finding them later. Builds for a browser or another WebAssembly host share the runtime and the FFI, but CI does not build or test them.

• Beneficiaries: Projects that run Lean in the browser, such as lean4-wasm-in-browser, projects that compile Lean programs to WebAssembly, such as Lasm and my personal interest is compiling lean to the Internet Computer.

• Maintainability: Apart from the workflows, the FFI definitions of fix: match the parameters of eight FFI definitions to the generated C #16090 and the 32-bit exit-code fix of fix: return the right exit code from lean on 32-bit targets #16137, the stack changes only code for Emscripten: fixes to the WebAssembly build (chore: re-enable the Web Assembly CI job #16135), the toolchain update (chore: update the Web Assembly CI job to Emscripten 6.0.13 #16142) and the interpreter's symbol table for lean.js (perf: resolve native symbols inside lean.wasm instead of exporting all of Lean #16149), all behind if(Emscripten), #ifdef LEAN_EMSCRIPTEN or Emscripten-only make rules. The job blocks nothing, and I will watch it and fix what breaks. On a standard GitHub-hosted runner the job takes about 30 minutes with the caches of a previous run (run 41286288809: stage 0 in 37 s, stage 1 in 23 min, Pack in 6 min, its six tests in 17 s) and roughly 75 minutes with empty caches, mostly to build the native 32-bit stage 0, to build stage 1 with it and to link lean.js. With chore: run more of the test suite on the Web Assembly job #16191 the job runs 177 tests in parallel instead (the elab and elab_fail tests whose behaviour depends on the platform, the misc scripts that test the command line and markdown_conformance), which adds 8 to 10 minutes on the slower runners of its two trial runs, where the whole job took 48 and 60 minutes. With perf: resolve native symbols inside lean.wasm instead of exporting all of Lean #16149 a lean.js process starts in 2 to 3 seconds instead of about 2 minutes, because the interpreter finds native code through a table inside the module instead of Emscripten's dlsym, which searched all 251,027 exports on every lookup (dlsym enumerates every export of the library on each call (Object.keys(lib.exports).indexOf) emscripten-core/emscripten#28124), and a lean process needs about 1.5 GiB instead of up to 10 GiB, because lean.wasm exports 629 symbols instead of 251,027 and lean.js shrinks from more than 100 MB to 200 KB.

Questions for the maintainers:

1. Is a non-blocking WebAssembly job acceptable, given that WebAssembly is not a supported target?
2. Should PRs be able to run it without the rest of release-ci, for example with a wasm-ci label?
3. Would you consider publishing linux_wasm32 archives again once the job has been green for a while?

Claude Code, an AI coding assistant, helped with the investigation, the changes and this proposal. I reviewed and checked them.

Community Feedback

• #lean4 > wasm build: in June 2025, Sam Wáng noticed that the WebAssembly toolchain was missing from the releases since v4.16. On 2025-10-14, Kim Morrison replied that "WASM is no longer supported." In 2023, signature mismatches that a WebAssembly build reported in the same thread led to fix: FFI signature mismatches #2433.
• #general > what is lean.js: Markus Himmel explained that the target was dropped because of "an Emscripten limitation which would have taken a lot of engineering effort to overcome": the EXPORT_ALL build exceeded V8's limit of 100,000 exports, as the CI log he quoted shows. Cauli Ziani then re-enabled the job in a fork (chore: reactivate WASM (Web Assembly) CI builds  cauli/lean4#1) and built lean.wasm on a GitHub-hosted runner, and Robin Arnez posted the error that Node.js gave him: exports count of 201107 exceeds internal limit of 100000. On 2026-01-05, Kim Morrison found that the fork's build loads under Node.js 25 but traps in initialize_Lean with RuntimeError: unreachable, which Cauli traced to mismatched function signatures. Eight FFI definitions have the wrong number of parameters, so calls to them can trap on WebAssembly #16089 reports them, and fix: match the parameters of eight FFI definitions to the generated C #16090 fixes them. This proposal builds on that work.

Impact

Add 👍 to issues you consider important. If others benefit from the changes in this proposal being added, please ask them to add 👍 to it.