Repository navigation

perf: resolve native symbols inside lean.wasm instead of exporting all of Lean - #16149

Draft

basvandijk wants to merge 18 commits into

leanprover:masterfrom

basvandijk:wasm-symbols

Draft

perf: resolve native symbols inside lean.wasm instead of exporting all of Lean#16149
basvandijk wants to merge 18 commits into
leanprover:masterfrom
basvandijk:wasm-symbols

Commits on Nov 2, 2026
- fix: compile `IO.FS.renameIfNew` for Emscripten
  
  basvandijk
  and
  claude
  committed
  e9e78b5
- fix: generate the `lean` launcher for the WebAssembly build again
  
  basvandijk
  and
  claude
  committed
  ff01a9b
- fix: archive the WebAssembly libraries with `emar` and build only what `lean.js` links
  
  basvandijk
  and
  claude
  committed
  39246b9
- test: disable header snapshots on Emscripten
  
  basvandijk
  and
  claude
  committed
  67ccbb6
- chore: re-enable the Web Assembly CI job
  
  basvandijk
  and
  claude
  committed
  9b8893f
- fix: give emcc's JavaScript passes enough heap to link `lean.js`
  
  basvandijk
  and
  claude
  committed
  8f62523
- chore: run the wasm tests one at a time
  
  basvandijk
  and
  claude
  committed
  d4c6e32
- fix: build the shell library before linking `lean.js`
  
  basvandijk
  and
  claude
  committed
  d190456
- fix: stop building the dummy shared libraries on Emscripten
  
  basvandijk
  and
  claude
  committed
  0bde9b7
- fix: link the C++ runtime into `lean.js` with Emscripten 6
  
  basvandijk
  and
  claude
  committed
  d77b220
- chore: pass Emscripten's link settings only when linking
  
  basvandijk
  and
  claude
  committed
  753d1bb
- fix: keep Emscripten's profiling runtime from writing `default.profraw`
  
  basvandijk
  and
  claude
  committed
  20a4eb6
- chore: update the Web Assembly CI job to Emscripten 6.0.13
  
  basvandijk
  and
  claude
  committed
  e1ce278
- doc: describe the WebAssembly build of `lean.js`
  
  basvandijk
  and
  claude
  committed
  e80c565
- perf: resolve the interpreter's native symbols inside lean.wasm
  
  basvandijk
  and
  claude
  committed
  d02b4f3
- perf: export only the runtime from lean.wasm
  
  basvandijk
  and
  claude
  committed
  aab2914
- doc: describe the native symbol table of lean.js
  
  basvandijk
  and
  claude
  committed
  cf685f6
- chore: remove copyright statement in `script/wasm_symbols.py`
  basvandijk
  authored
  6f1180c

Commits

Commits on Nov 2, 2026