[basvandijk]

This PR makes lean.js, the WebAssembly build of lean, start about 50 times faster (5 s instead of 236 s on an empty file on a workstation), shrinks its JavaScript file from 113 MB to 201 KB and cuts the memory of a lean process by about two thirds.

Background

The interpreter switches to native code by looking up a declaration's mangled symbol at run time, which is why lean.wasm exported every symbol of Lean (247,834 of them) and why lean.js was linked with -sMAIN_MODULE=1 -sEXPORT_ALL=1. Emscripten's dlsym enumerates all exports of the module on every call (Object.keys(lib.exports).indexOf(symbol), emscripten-core/emscripten#28124), about 75 ms per call with that many exports, and lean performs one lookup per imported module and two per imported parser constant at startup, 2,630 for Init alone; that was most of the time a test took on the Web Assembly CI job.

Changes

• The new script script/wasm_symbols.py now reads the global symbols of the Lean archives that lean.js links (libInit.a, libStd.a, libLean.a) from their wasm object files, together with each function's type, and writes a sorted name/address table with a binary-search lookup, lean_lookup_native_symbol.
• The table is about 28 MB of static data, so the link's initial memory is raised from Emscripten's default 16 MB to 64 MB.
• lookup_symbol_in_cur_exe consults that new function on Emscripten instead of dlsym;
  only the symbols of the C and C++ runtime archives, which the script writes as the export list for the link (600 names), are still resolved through dlsym.
• With that table embedded in the module, lean.js is linked with -sMAIN_MODULE=2, so unused code is removed and the JavaScript glue no longer declares a variable per export, which was three quarters of the 113 MB file;
• doc/make/emscripten.md describes the symbol table and the export list.

Results

• Threads start in 0.5 s instead of 5 s.
• tests/elab/Format.lean peaks at 1.5 GB instead of 5.3 GB.

This PR is stacked on #16142 and carries its commits until that PR merges; it will be rebased onto master afterwards. Until then, the diff of this PR alone is basvandijk:wasm-emsdk-6...basvandijk:wasm-symbols.

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

🤖 Generated with Claude Code

[basvandijk]

How this was tested:

• The Web Assembly job runs only at check level 2 or higher, so the CI evidence is a run of this branch's job on my fork: https://github.com/basvandijk/lean4/actions/runs/41286288809 (emsdk 6.0.13, Node.js 26.13.0, ccache warm from an earlier run): green, all steps done 31 min after the start; Setup emsdk 9 s, Build Stage 0 37 s, Build Target Stage 22.6 min, Install 5 s, Pack 5.8 min, Test 17 s (1037 2.30 s, Format 2.69 s, ac_rfl 3.24 s, libuv 2.54 s, tempfile 3.03 s, 1007 2.83 s; 6/6), source tree clean; lean.js 196 KB and lean.wasm 125 MB in the install tree; warnings: 0 linker setting ignored during compilation, 0 function signature mismatch, the same three Emscripten notes as before, 6 undefined symbols (the five lean_uv_* and dl_iterate_phdr; the eight uv__* internals of before are eliminated with the unused libuv code). An earlier run of the branch with the untyped table declarations described below, https://github.com/basvandijk/lean4/actions/runs/41256450142, was green in 54 min with the same timings (Test 28 s) but logged the 58 function signature mismatch warnings. Baseline for comparison: run 41233382394 of chore: update the Web Assembly CI job to Emscripten 6.0.13 #16142 (Build Target Stage 40.1 min, Install 7 s, Pack 8.4 min, Test 13.3 min, 6/6).
• Local build in a Docker container mirroring the runner (ubuntu:24.04, clang 18.1.3, cmake 3.31.6, emsdk 6.0.13, Node.js 26.13.0) with the job's CMAKE_OPTIONS, on an AMD EPYC 7302 (slower per thread than the runner). Before, with the first commit (table, exports unchanged), and with all commits: lean -j4 on an empty file 236 s → 21 s → 5.0 s (three runs each, spread under 1 s); tests/elab/1037.lean 234 s → 20 s → 5.4 s; tests/elab/Format.lean 193 s and 5.3 GB → 27 s and 5.5 GB → 6.3 s and 1.5 GB; the six CI tests about 20 min → 2 min 42 s → 41 s, all passing, source tree clean, no default.profraw; lean --version 6.7 s → 7.1 s → 1.7 s; peak RSS of the empty-file run 2.5 GB → 2.6 GB → 1.0 GB. lean.js 113,180,992 B → 113,181,131 B → 200,852 B; lean.wasm 134,824,759 B → 163,278,667 B (the table is 28 MB of static data, hence -sINITIAL_MEMORY=64MB) → 130,973,589 B (dead-code elimination and the dropped export-name section outweigh the table); exports 247,834 → 247,835 → 629 (589 lean_*, 29 Emscripten runtime, calloc, pthread_self, segv_handler, three llvm_*, initialize_libuv, initialize_cadical); imports 410 → 410 → 74; the undefined symbols the link reports go from 14 to 6 (the eight uv__* internals are eliminated with the unused libuv code; the five lean_uv_* and dl_iterate_phdr remain, as before). Lean's --profile on the empty file: import 57.1 s → 2.1 s, interpretation 161 s → 10 ms, initialization 351 ms unchanged.
• Where the time went, measured by wrapping _dlsym_js in a copy of the generated lean.js: the baseline empty-file run makes 2,630 dlsym calls, 678 for the module initializers (initialize_Init_*), 502 for l_*___boxed symbols of imported parser constants and 725 pairs of a ___boxed miss followed by the unboxed hit, each 65-130 ms (median 75 ms), 210 s in total out of 236 s; with the table the same run makes 0 dlsym calls. A standalone main module with N exported functions shows the per-call cost growing from 0.5 ms at 1,000 exports to 80 ms at 250,000 (0.016 ms natively); reported at dlsym enumerates every export of the library on each call (Object.keys(lib.exports).indexOf) emscripten-core/emscripten#28124, fix proposed in Make dlsym O(1) in the number of exports. NFC emscripten-core/emscripten#28125. Loader phases per thread, before → after: parsing the glue and compiling the wasm 1.4 s → 0.8 s on the main thread, mergeLibSymbols 0.7 s → 0.02 s, updateGOT 2.5 s → 0.4 s, main entered at 5.1 s → 1.2 s, each pthread worker ready about 5 s → 0.5 s after it is spawned; Lean's first symbol lookup happened at 18.5 s, now its whole work runs from 2.7 s to 4.8 s.
• Interpreter probes on the final build: #eval Nat.gcd 12 18 (native ___boxed symbol reached from interpreted code) → 6; functions with scalar parameters and a constant (Nat.add 40 2, UInt8.ofNat 300, 2.5 + 0.25) → (42, 44, 2.750000); a macro defined in the file → (21, 21); an interpreted closure calling native code on a task thread (IO.asTask) → task 6; import Lean and Lean.Meta.whnf from #eval → whnf: 1 (12 s, 2.7 GB, 2,437 modules; 32 s and 6.6 GB with the table alone). Exit codes of IO.Process.exit 3, a failing file, a missing file, a kernel exception and panic! as before; --version, --run and --print-prefix still return the 32-bit garbage code of lean --version, --run and other options exit with a garbage code on 32-bit targets #16136; the LEAN_PATH and cwd controls of chore: update the Web Assembly CI job to Emscripten 6.0.13 #16142 behave as before, which also shows that the JavaScript helpers Lean's EM_ASM blocks use (ENV, FS, NODEFS, UTF8ToString, stringToUTF8, _malloc) are still present in the dead-code-eliminated link; lean -o still fails on dl_iterate_phdr (pre-existing), so an initialize in an imported uncompiled module could not be probed on wasm.
• Generator checks: the table holds every global symbol of libInit.a, libStd.a and libLean.a (239,781 entries: 231,036 functions, 8,745 data), the export list every global symbol of the four runtime archives that is a C identifier and not C++-mangled or Emscripten metadata (600 names, none of them l_*); the table object's undefined symbols are exactly the Lean archives' symbols plus strcmp. The declarations carry the functions' wasm types read from the archives' object files (type, import, function and linking sections), so they match the definitions exactly and the link reports no signature mismatch; the script cross-checks the symbols it reads against llvm-nm's listing and fails on any difference. An earlier version declared every function as void f(void) and relied on wasm-ld ignoring prototypes for address-only references; the table it produced was correct (every one of the 231,036 entries, resolved through lean_lookup_native_symbol in the running module, had its real type, checked with WebAssembly.Function.type()), but the link warned function signature mismatch for the 58 functions that the C++ runtime calls directly, which is why the types are now exact. The generator takes 6 s and the table C file compiles in 18 s with 1.2 GB.
• Controls: the first commit alone (table, EXPORT_ALL kept) attributes the startup gain to the lookup (236 s → 21 s, lean.js and per-thread loader time unchanged) and the second commit the size, per-thread and memory gains to the export list (21 s → 5 s, 113 MB → 201 KB, 2.6 GB → 1.0 GB); the baseline numbers above come from the same toolchain, host and day. A third variant, the unchanged baseline lean.js with only Emscripten's _dlsym_js patched to the O(1) form proposed upstream, starts in 20 s with its 2,630 dlsym calls taking 17 ms in total, so the table matches what a fixed Emscripten would give and the export list is the part a toolchain fix cannot provide. The generated export list of the first attempt contained __main_argc_argv, which emcc rejects as an export (it synthesizes main from it), hence its exclusion in the script.
• Not tested: browser embedding; Emscripten versions other than 6.0.13; a module-based importer (two initializer lookups per module, both table hits).

[basvandijk]

changelog-no