From e9e78b57a77eefd55539d28666cdc59b81673e6a Mon Sep 17 00:00:00 2001 From: Bas van Dijk Date: Fri, 30 Oct 2026 15:19:23 +0000 Subject: [PATCH 01/18] fix: compile `IO.FS.renameIfNew` for Emscripten Co-Authored-By: Claude Opus 5.5 --- src/runtime/io.cpp | 14 +++++++++++--- 1 file changed, 11 insertions(+), 3 deletions(-) diff --git a/src/runtime/io.cpp b/src/runtime/io.cpp index 120f33d52ca0..9f77e95b8bce 100644 --- a/src/runtime/io.cpp +++ b/src/runtime/io.cpp @@ -57,12 +57,10 @@ Authors: Leonardo de Moura, Sebastian Ullrich #include #endif -#ifndef LEAN_WINDOWS -#ifndef __APPLE__ +#if !defined(LEAN_WINDOWS) && !defined(__APPLE__) && !defined(LEAN_EMSCRIPTEN) #include #include // RENAME_NOREPLACE #endif -#endif namespace lean { @@ -1273,6 +1271,16 @@ extern "C" LEAN_EXPORT obj_res lean_io_rename_if_new(b_obj_arg from, b_obj_arg t #else #if defined(__APPLE__) bool ok = renameatx_np(AT_FDCWD, from_str, AT_FDCWD, to_str, RENAME_EXCL) == 0; +#elif defined(LEAN_EMSCRIPTEN) + // Emscripten has no `renameat2`. Unlike the other branches, this check is not atomic. As with + // `renameat2`, a missing `from` is reported even when `to` exists. + struct stat st; + bool ok = false; + if (lstat(to_str, &st) != 0) { + ok = rename(from_str, to_str) == 0; + } else if (lstat(from_str, &st) == 0) { + errno = EEXIST; + } #else // glibc 2.26 does not yet have `renameat2` (2.28+) bool ok = syscall(SYS_renameat2, AT_FDCWD, from_str, AT_FDCWD, to_str, RENAME_NOREPLACE) == 0; From ff01a9b9cf4b2bfcbce34c339c5e1fddd710ac0a Mon Sep 17 00:00:00 2001 From: Bas van Dijk Date: Fri, 30 Oct 2026 15:19:23 +0000 Subject: [PATCH 02/18] fix: generate the `lean` launcher for the WebAssembly build again Co-Authored-By: Claude Opus 5.5 --- src/bin/lean.in | 2 +- src/shell/CMakeLists.txt | 5 +++++ 2 files changed, 6 insertions(+), 1 deletion(-) diff --git a/src/bin/lean.in b/src/bin/lean.in index 044b4cef365a..82a1104a094e 100755 --- a/src/bin/lean.in +++ b/src/bin/lean.in @@ -1,4 +1,4 @@ #!/usr/bin/env bash # ONLY FOR WEB ASSEMBLY BUILD -node --stack-size=8192 ${CMAKE_BINARY_DIR}/bin/lean.js $@ +exec node --stack-size=8192 "$(dirname "$(readlink -f "$0")")/lean.js" "$@" diff --git a/src/shell/CMakeLists.txt b/src/shell/CMakeLists.txt index 19ad5acb9a31..4baff21de872 100644 --- a/src/shell/CMakeLists.txt +++ b/src/shell/CMakeLists.txt @@ -42,3 +42,8 @@ add_custom_target( COMMAND $(MAKE) -f ${CMAKE_BINARY_DIR}/stdlib.make lean COMMAND_EXPAND_LISTS ) + +# `lean.js` needs a launcher so that tests and users can run `lean` +if(CMAKE_SYSTEM_NAME MATCHES "Emscripten") + configure_file("${LEAN_SOURCE_DIR}/bin/lean.in" "${CMAKE_BINARY_DIR}/bin/lean" COPYONLY) +endif() From 39246b93dee22dab8d39c39fbd73b9ff38576773 Mon Sep 17 00:00:00 2001 From: Bas van Dijk Date: Fri, 30 Oct 2026 15:19:24 +0000 Subject: [PATCH 03/18] fix: archive the WebAssembly libraries with `emar` and build only what `lean.js` links Co-Authored-By: Claude Opus 5.5 --- src/stdlib.make.in | 11 ++++++++++- 1 file changed, 10 insertions(+), 1 deletion(-) diff --git a/src/stdlib.make.in b/src/stdlib.make.in index 055547f4be5e..2253190953d1 100644 --- a/src/stdlib.make.in +++ b/src/stdlib.make.in @@ -8,6 +8,10 @@ SHELL := $(LEAN_BASH) -eo pipefail export LEAN_PATH= ifeq "${USE_LAKE}" "ON" export LEAN_CC=${CMAKE_C_COMPILER} + ifeq "${CMAKE_SYSTEM_NAME}" "Emscripten" + # Lake's fallback, GNU `ar`, writes no symbol index for wasm objects + export LEAN_AR=${CMAKE_AR} + endif else export LEAN_CC=${CMAKE_C_COMPILER_LAUNCHER} ${CMAKE_C_COMPILER} endif @@ -54,9 +58,14 @@ endif ifeq "${USE_LAKE}" "ON" +ifeq "${CMAKE_SYSTEM_NAME}" "Emscripten" + # only what `lean.js` links; Lake and the other tools are not built for Emscripten + LAKE_TARGETS ?= Init Std Lean +endif + # build in parallel Init: - LEAN_GITHASH=${LAKE_LEAN_GITHASH} ${PREV_STAGE}/bin/lake build -f ${CMAKE_BINARY_DIR}/lakefile.toml ${LEAN_EXTRA_LAKE_OPTS} $(LAKE_EXTRA_ARGS) + LEAN_GITHASH=${LAKE_LEAN_GITHASH} ${PREV_STAGE}/bin/lake build -f ${CMAKE_BINARY_DIR}/lakefile.toml ${LEAN_EXTRA_LAKE_OPTS} $(LAKE_TARGETS) $(LAKE_EXTRA_ARGS) Std Lean LeanExport Lake Leanc LeanChecker LeanIR: Init From 67ccbb66234ec72d467ff551e7a84822eed1e2bc Mon Sep 17 00:00:00 2001 From: Bas van Dijk Date: Fri, 30 Oct 2026 15:19:24 +0000 Subject: [PATCH 04/18] test: disable header snapshots on Emscripten Co-Authored-By: Claude Opus 5.5 --- tests/CMakeLists.txt | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/tests/CMakeLists.txt b/tests/CMakeLists.txt index 51e92ef7b831..a395bccecadd 100644 --- a/tests/CMakeLists.txt +++ b/tests/CMakeLists.txt @@ -46,6 +46,11 @@ string(APPEND TEST_VARS " CXX='${CMAKE_CXX_COMPILER} ${LEANC_OPTS}'") # fixture below; absent for manual `run_test.sh` runs, where # `maybe_use_lean_header_snapshot` skips them. option(LEAN_HEADER_SNAPSHOTS "Pre-elaborate Lean/Init header snapshots to speed up the elab test suites" OFF) +if(LEAN_HEADER_SNAPSHOTS AND CMAKE_SYSTEM_NAME MATCHES "Emscripten") + # saving a snapshot needs `dl_iterate_phdr`, which Emscripten does not provide + message(STATUS "LEAN_HEADER_SNAPSHOTS is not supported on Emscripten; disabling it") + set(LEAN_HEADER_SNAPSHOTS OFF) +endif() if(LEAN_HEADER_SNAPSHOTS) string(APPEND TEST_VARS " LEAN_HEADER_SNAPSHOT_LEAN='${MANGLED_CURRENT_BINARY_DIR}/lean_header_lean.snap'") string(APPEND TEST_VARS " LEAN_HEADER_SNAPSHOT_INIT='${MANGLED_CURRENT_BINARY_DIR}/lean_header_init.snap'") From 9b8893f24f96a5741dfe5ac2e3c6928096876a63 Mon Sep 17 00:00:00 2001 From: Bas van Dijk Date: Fri, 30 Oct 2026 15:19:24 +0000 Subject: [PATCH 05/18] chore: re-enable the Web Assembly CI job Co-Authored-By: Claude Opus 5.5 --- .github/workflows/build-template.yml | 9 ++++++- .github/workflows/ci.yml | 35 +++++++++++++++++----------- 2 files changed, 29 insertions(+), 15 deletions(-) diff --git a/.github/workflows/build-template.yml b/.github/workflows/build-template.yml index a4dd854b0e15..9582974324ca 100644 --- a/.github/workflows/build-template.yml +++ b/.github/workflows/build-template.yml @@ -85,6 +85,12 @@ jobs: version: 3.1.44 actions-cache-folder: emsdk if: matrix.wasm + - name: Setup Node.js + # `lean.wasm` has more than 100'000 exports, which V8 only accepts from Node.js 24 on + uses: actions/setup-node@v7 + with: + node-version: 26 + if: matrix.wasm - name: Install 32bit c libs run: | sudo dpkg --add-architecture i386 @@ -382,7 +388,8 @@ jobs: if: always() run: ccache -s - name: Show stacktrace for coredumps - if: failure() && runner.os == 'Linux' + # `$GDB` comes from the Nix shell + if: failure() && runner.os == 'Linux' && !matrix.cmultilib run: | for c in $(find . -name core); do progbin="$(file $c | sed "s/.*execfn: '\([^']*\)'.*/\1/")" diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 56cfc91607e7..37ff4d40e905 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -426,20 +426,27 @@ jobs: // "cross": true, // "shell": "bash -euxo pipefail {0}" //} - // { - // "name": "Web Assembly", - // "os": "ubuntu-latest", - // // Build a native 32bit binary in stage0 and use it to compile the oleans and the wasm build - // "CMAKE_OPTIONS": "-DCMAKE_C_COMPILER_WORKS=1 -DSTAGE0_USE_GMP=OFF -DSTAGE0_LEAN_EXTRA_CXX_FLAGS='-m32' -DSTAGE0_LEANC_OPTS='-m32' -DSTAGE0_CMAKE_CXX_COMPILER=clang++ -DSTAGE0_CMAKE_C_COMPILER=clang -DSTAGE0_CMAKE_EXECUTABLE_SUFFIX=\"\" -DUSE_GMP=OFF -DMMAP=OFF -DSTAGE0_MMAP=OFF -DCMAKE_AR=../emsdk/emsdk-main/upstream/emscripten/emar -DCMAKE_TOOLCHAIN_FILE=../emsdk/emsdk-main/upstream/emscripten/cmake/Modules/Platform/Emscripten.cmake -DLEAN_INSTALL_SUFFIX=-linux_wasm32 -DSTAGE0_CMAKE_LIBRARY_PATH=/usr/lib/i386-linux-gnu/", - // "wasm": true, - // "cmultilib": true, - // "release": true, - // "enabled": level >= 2, - // "cross": true, - // "shell": "bash -euxo pipefail {0}", - // // Just a few selected tests because wasm is slow - // "CTEST_OPTIONS": "-R \"leantest_1007\\.lean|leantest_Format\\.lean|leanruntest\\_1037.lean|leanruntest_ac_rfl\\.lean|leanruntest_tempfile.lean\\.|leanruntest_libuv\\.lean\"" - // } + { + "name": "Web Assembly", + // stage0 is built with this image's clang and i386 libraries (see "Install 32bit c libs") + "os": "ubuntu-24.04", + // Build a native 32bit binary in stage0 and use it to compile the oleans and the wasm build. + // The emsdk paths must be absolute: sub-builds such as libuv's resolve them from their own directories. + "CMAKE_OPTIONS": "-DCMAKE_C_COMPILER_WORKS=1 -DSTAGE0_USE_GMP=OFF -DSTAGE0_LEAN_EXTRA_CXX_FLAGS='-m32 -msse2 -mfpmath=sse -DLEAN_DEFAULT_THREAD_STACK_SIZE=33554432' -DSTAGE0_LEANC_OPTS='-m32 -msse2 -mfpmath=sse' -DSTAGE0_LEAN_EXTRA_LINKER_FLAGS=-m32 -DSTAGE0_CMAKE_C_FLAGS=-m32 -DSTAGE0_CMAKE_CXX_COMPILER=clang++ -DSTAGE0_CMAKE_C_COMPILER=clang -DSTAGE0_CMAKE_EXECUTABLE_SUFFIX=\"\" -DSTAGE0_PKG_CONFIG_EXECUTABLE=/usr/bin/i386-linux-gnu-pkg-config -DSTAGE0_CMAKE_LIBRARY_PATH=/usr/lib/i386-linux-gnu/ -DUSE_GMP=OFF -DMMAP=OFF -DSTAGE0_MMAP=OFF -DUSE_MIMALLOC=OFF -DCMAKE_AR=$GITHUB_WORKSPACE/emsdk/emsdk-main/upstream/emscripten/emar -DCMAKE_TOOLCHAIN_FILE=$GITHUB_WORKSPACE/emsdk/emsdk-main/upstream/emscripten/cmake/Modules/Platform/Emscripten.cmake -DLEAN_INSTALL_SUFFIX=-linux_wasm32", + "wasm": true, + "cmultilib": true, + "cross": true, + // not shipped: its oleans are built by stage0 + "release": false, + // must not block nightlies + "secondary": true, + "enabled": level >= 2 && target_stage < 2, + "test": true, + "binary-check": "file", + "shell": "bash -euxo pipefail {0}", + // Just a few selected tests because wasm is slow + "CTEST_OPTIONS": "--no-tests=error -R '^(elab_fail/1007|elab/(Format|1037|ac_rfl|tempfile|libuv))\\.lean$'" + } ]; // Stage that is built, tested and packed. Shipped (stamped) release builds use stage2. for (const job of matrix) { From 8f62523cde95734468895f73dc802a71f71bacc7 Mon Sep 17 00:00:00 2001 From: Bas van Dijk Date: Fri, 30 Oct 2026 16:11:36 +0000 Subject: [PATCH 06/18] fix: give emcc's JavaScript passes enough heap to link `lean.js` Co-Authored-By: Claude Opus 5.5 --- src/stdlib.make.in | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/src/stdlib.make.in b/src/stdlib.make.in index 2253190953d1..023980b3c9e6 100644 --- a/src/stdlib.make.in +++ b/src/stdlib.make.in @@ -16,6 +16,10 @@ else export LEAN_CC=${CMAKE_C_COMPILER_LAUNCHER} ${CMAKE_C_COMPILER} endif export LEAN_ABORT_ON_PANIC=1 +ifeq "${CMAKE_SYSTEM_NAME}" "Emscripten" + # emcc's JavaScript passes over the large `lean.js` need more than Node's default heap of about 4 GB + export NODE_OPTIONS += --max-old-space-size=8192 +endif # Short aliases for verbose CMake variables OUTLIB := ${CMAKE_LIBRARY_OUTPUT_DIRECTORY} From d4c6e32265484a6c67f9382f1ad92bb6ae190098 Mon Sep 17 00:00:00 2001 From: Bas van Dijk Date: Fri, 30 Oct 2026 17:49:17 +0000 Subject: [PATCH 07/18] chore: run the wasm tests one at a time Co-Authored-By: Claude Opus 5.5 --- .github/workflows/ci.yml | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 37ff4d40e905..09e26c71d341 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -444,8 +444,9 @@ jobs: "test": true, "binary-check": "file", "shell": "bash -euxo pipefail {0}", - // Just a few selected tests because wasm is slow - "CTEST_OPTIONS": "--no-tests=error -R '^(elab_fail/1007|elab/(Format|1037|ac_rfl|tempfile|libuv))\\.lean$'" + // Just a few selected tests because wasm is slow. A wasm `lean` process can need 10 GB, + // so they run one at a time (this `-j` overrides the step's `-j$NPROC`). + "CTEST_OPTIONS": "--no-tests=error -j1 -R '^(elab_fail/1007|elab/(Format|1037|ac_rfl|tempfile|libuv))\\.lean$'" } ]; // Stage that is built, tested and packed. Shipped (stamped) release builds use stage2. From d1904562e58521b3f0bbeb7f27f45538c098e847 Mon Sep 17 00:00:00 2001 From: Bas van Dijk Date: Fri, 30 Oct 2026 22:46:52 +0000 Subject: [PATCH 08/18] fix: build the shell library before linking `lean.js` Co-Authored-By: Claude Opus 5.5 --- src/CMakeLists.txt | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 4604704aff0f..5978894c6265 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -971,10 +971,11 @@ if(CMAKE_SYSTEM_NAME MATCHES "Emscripten") DEPENDS make_stdlib leanrt_initial-exec COMMAND touch ${CMAKE_LIBRARY_OUTPUT_DIRECTORY}/libInit_shared${CMAKE_SHARED_LIBRARY_SUFFIX} ) + # `leanshell` because `lean.js` links `libleanshell.a` directly (`LEAN_EXE_LINKER_FLAGS`) add_custom_target( leanshared ALL - DEPENDS Init_shared leancpp + DEPENDS Init_shared leancpp leanshell COMMAND touch ${CMAKE_LIBRARY_OUTPUT_DIRECTORY}/libleanshared_2${CMAKE_SHARED_LIBRARY_SUFFIX} COMMAND touch ${CMAKE_LIBRARY_OUTPUT_DIRECTORY}/libleanshared_1${CMAKE_SHARED_LIBRARY_SUFFIX} COMMAND touch ${CMAKE_LIBRARY_OUTPUT_DIRECTORY}/libleanshared${CMAKE_SHARED_LIBRARY_SUFFIX} From 0bde9b706ddb7ed70a37d6b49472fd9a33592895 Mon Sep 17 00:00:00 2001 From: Bas van Dijk Date: Sat, 31 Oct 2026 15:15:27 +0000 Subject: [PATCH 09/18] fix: stop building the dummy shared libraries on Emscripten On Emscripten the shared libraries are dummies: `lean.js` links the static archives (`LEAN_EXE_LINKER_FLAGS`), and `src/CMakeLists.txt` only touches `libInit_shared.so`, `libleanshared_1.so`, `libleanshared_2.so` and `libleanshared.so`. The `lean` rule in `stdlib.make` still depended on them, so once per build, after `lib/temp/empty.c` had been created, `make` ran their recipes, that is `emcc -shared`, which Emscripten before 6.0 emulated with a static object file and a warning and which Emscripten 6 turns into a real side-module link of all of Lean. And because the dummies are touched on every build, `make install` relinked `lean.js`, nine of the Web Assembly job's sixty minutes. `lean.js` now depends on `libInit.a`, `libStd.a`, `libLean.a`, `libleancpp.a`, `libleanrt.a`, `libleanshell.a` and `libleanmain.a`, with the Lake `.trace` files of the first three like the other binaries, and the dummy `leanshared` target depends on `leanrt`, which nothing ordered before `lean.js` so far. The shared-library recipes are no longer reachable on Emscripten; the native rule is unchanged. Co-Authored-By: Claude Fable 5.1 --- src/CMakeLists.txt | 4 ++-- src/stdlib.make.in | 11 ++++++++++- 2 files changed, 12 insertions(+), 3 deletions(-) diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 5978894c6265..800b00690a4b 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -971,11 +971,11 @@ if(CMAKE_SYSTEM_NAME MATCHES "Emscripten") DEPENDS make_stdlib leanrt_initial-exec COMMAND touch ${CMAKE_LIBRARY_OUTPUT_DIRECTORY}/libInit_shared${CMAKE_SHARED_LIBRARY_SUFFIX} ) - # `leanshell` because `lean.js` links `libleanshell.a` directly (`LEAN_EXE_LINKER_FLAGS`) + # `leanrt` and `leanshell` because `lean.js` links `libleanrt.a` and `libleanshell.a` directly (`LEAN_EXE_LINKER_FLAGS`) add_custom_target( leanshared ALL - DEPENDS Init_shared leancpp leanshell + DEPENDS Init_shared leancpp leanrt leanshell COMMAND touch ${CMAKE_LIBRARY_OUTPUT_DIRECTORY}/libleanshared_2${CMAKE_SHARED_LIBRARY_SUFFIX} COMMAND touch ${CMAKE_LIBRARY_OUTPUT_DIRECTORY}/libleanshared_1${CMAKE_SHARED_LIBRARY_SUFFIX} COMMAND touch ${CMAKE_LIBRARY_OUTPUT_DIRECTORY}/libleanshared${CMAKE_SHARED_LIBRARY_SUFFIX} diff --git a/src/stdlib.make.in b/src/stdlib.make.in index 023980b3c9e6..00012776a960 100644 --- a/src/stdlib.make.in +++ b/src/stdlib.make.in @@ -124,6 +124,9 @@ $(OUTBIN)/leanir$(EXE): $(OUTARC)/libLeanIR.a.trace $(OUTBIN)/leanchecker$(EXE): $(OUTARC)/libLeanChecker.a.trace $(OUTBIN)/leanchecker-paranoid$(EXE): $(OUTARC)/libLeanChecker.a.trace ${LIB}/lean/libInit.a.trace ${LIB}/lean/libStd.a.trace ${LIB}/lean/libLean.a.trace ${LIB}/lean/libLake.a.trace $(OUTBIN)/leanexport$(EXE): $(OUTARC)/libLeanExport.a.trace +ifeq "${CMAKE_SYSTEM_NAME}" "Emscripten" +$(OUTBIN)/lean$(EXE): ${LIB}/lean/libInit.a.trace ${LIB}/lean/libStd.a.trace ${LIB}/lean/libLean.a.trace +endif endif # we specify the precise file names here to avoid rebuilds @@ -206,7 +209,13 @@ $(OUTBIN)/lake$(EXE): ${LIB}/temp/LakeMain.*o.export $(OUTLIB)/libLake_shared$(S lake: $(OUTBIN)/lake$(EXE) -$(OUTBIN)/lean$(EXE): $(OUTLIB)/libInit_shared$(SO) $(OUTLIB)/libleanshared_2$(SO) $(OUTLIB)/libleanshared_1$(SO) $(OUTLIB)/libleanshared$(SO) ${LIB}/temp/libleanmain.a +ifeq "${CMAKE_SYSTEM_NAME}" "Emscripten" +# the shared libraries are dummies (see `src/CMakeLists.txt`); `lean.js` links these archives (`LEAN_EXE_LINKER_FLAGS`) +$(OUTBIN)/lean$(EXE): ${LIB}/lean/libInit.a ${LIB}/lean/libStd.a ${LIB}/lean/libLean.a ${LIB}/lean/libleancpp.a ${LIB}/lean/libleanrt.a ${LIB}/temp/libleanshell.a +else +$(OUTBIN)/lean$(EXE): $(OUTLIB)/libInit_shared$(SO) $(OUTLIB)/libleanshared_2$(SO) $(OUTLIB)/libleanshared_1$(SO) $(OUTLIB)/libleanshared$(SO) +endif +$(OUTBIN)/lean$(EXE): ${LIB}/temp/libleanmain.a $(link-preamble) $(LEANC_SH) ${LIB}/temp/libleanmain.a ${CMAKE_EXE_LINKER_FLAGS_MAKE} ${CMAKE_DYN_EXE_LINKER_FLAGS_MAKE} ${LEAN_EXE_LINKER_FLAGS} ${LEANC_OPTS} -o $@ From d77b22053b5f557139caea9c3e4716e210ded985 Mon Sep 17 00:00:00 2001 From: Bas van Dijk Date: Sat, 31 Oct 2026 15:17:27 +0000 Subject: [PATCH 10/18] fix: link the C++ runtime into `lean.js` with Emscripten 6 Since Emscripten 6.0.6, `emcc` links libc++ and libc++abi only when run as `em++` or with `-sDEFAULT_TO_CXX=1`, and it has always ignored `-lstdc++` for compatibility with GNU toolchains. `lean.js` is linked by `leanc.sh`, that is by `emcc`, with `ERROR_ON_UNDEFINED_SYMBOLS=0` and `MAIN_MODULE=1`, so on Emscripten 6 the link succeeds and `lean.js` fails when Node.js starts it. On Emscripten the C++ standard library flag is therefore `-sDEFAULT_TO_CXX=1`; before 6.0.6 the setting is on by default, so this changes nothing there. Co-Authored-By: Claude Fable 5.1 --- src/CMakeLists.txt | 3 +++ 1 file changed, 3 insertions(+) diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 800b00690a4b..f0353c3d3898 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -528,6 +528,9 @@ set(LEAN_CXX_STDLIB "-lstdc++" CACHE STRING "C++ stdlib linker flags") if(CMAKE_SYSTEM_NAME MATCHES "Darwin") set(LEAN_CXX_STDLIB "-lc++") +elseif(CMAKE_SYSTEM_NAME MATCHES "Emscripten") + # `emcc` ignores `-lstdc++`; since Emscripten 6.0.6 it links libc++ only when told to link as C++ + set(LEAN_CXX_STDLIB "-sDEFAULT_TO_CXX=1") endif() if(CADICAL_LIB) From 753d1bbab417376c42c6a0f4e453ea0baea83af7 Mon Sep 17 00:00:00 2001 From: Bas van Dijk Date: Sat, 31 Oct 2026 15:18:36 +0000 Subject: [PATCH 11/18] chore: pass Emscripten's link settings only when linking `-sALLOW_MEMORY_GROWTH=1` takes effect only when linking, but `EMSCRIPTEN_SETTINGS` passed it to every compilation as well, through `LEAN_EXTRA_CXX_FLAGS` and libuv's `CMAKE_C_FLAGS`, which emcc reports 147 times per build as `linker setting ignored during compilation`. The flags for compiling and linking, `-fwasm-exceptions -pthread -flto`, are now `EMSCRIPTEN_FLAGS` and the settings `EMSCRIPTEN_LINK_SETTINGS`; both go into `LEAN_EXTRA_LINKER_FLAGS`, which `leanc.sh` adds to every link, so `LEAN_EXE_LINKER_FLAGS` does not repeat them. Settings use the `-sKEY=VALUE` spelling that Emscripten documents. `LINKABLE=1` is dropped: `MAIN_MODULE=1` implies it in every Emscripten version from 3.1.44 to 6.0.13, and Emscripten 4.0.15 deprecated it, so newer versions warn about setting it explicitly. The comment quoting Emscripten's old advice to pass all `-s` flags at compile time went with it. Co-Authored-By: Claude Fable 5.1 --- src/CMakeLists.txt | 17 +++++++++-------- 1 file changed, 9 insertions(+), 8 deletions(-) diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index f0353c3d3898..4cf867ab0035 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -164,12 +164,12 @@ if(CMAKE_SYSTEM_NAME MATCHES "Emscripten") # - system libraries such as OpenGL are included in the JS but shouldn't be # - we need EMSCRIPTEN_KEEPALIVE annotations on exports to run meta-dce (-s MAIN_MODULE=2) - # From https://emscripten.org/docs/compiling/WebAssembly.html#backends: - # > The simple and safe thing is to pass all -s flags at both compile and link time. - set(EMSCRIPTEN_SETTINGS "-s ALLOW_MEMORY_GROWTH=1 -fwasm-exceptions -pthread -flto") + # `-s` settings only take effect when linking; emcc warns when they are passed to a compilation + set(EMSCRIPTEN_FLAGS "-fwasm-exceptions -pthread -flto") + set(EMSCRIPTEN_LINK_SETTINGS "-sALLOW_MEMORY_GROWTH=1") string(APPEND LEANC_EXTRA_CC_FLAGS " -pthread") - string(APPEND LEAN_EXTRA_CXX_FLAGS " -D LEAN_EMSCRIPTEN ${EMSCRIPTEN_SETTINGS}") - string(APPEND LEAN_EXTRA_LINKER_FLAGS " ${EMSCRIPTEN_SETTINGS}") + string(APPEND LEAN_EXTRA_CXX_FLAGS " -D LEAN_EMSCRIPTEN ${EMSCRIPTEN_FLAGS}") + string(APPEND LEAN_EXTRA_LINKER_FLAGS " ${EMSCRIPTEN_FLAGS} ${EMSCRIPTEN_LINK_SETTINGS}") endif() # Added for CTest @@ -347,7 +347,7 @@ endif() # LibUV if(CMAKE_SYSTEM_NAME MATCHES "Emscripten") # Only on WebAssembly we compile LibUV ourselves - set(LIBUV_EMSCRIPTEN_FLAGS "${EMSCRIPTEN_SETTINGS}") + set(LIBUV_EMSCRIPTEN_FLAGS "${EMSCRIPTEN_FLAGS}") # LibUV does not compile on WebAssembly without modifications because # building LibUV on a platform requires including stub implementations @@ -920,10 +920,11 @@ if(CMAKE_SYSTEM_NAME MATCHES "Emscripten") # SIDE_MODULE=2 on `lean`, and set CMAKE_SHARED_LIBRARY_SUFFIX to ".js". # We set `ERROR_ON_UNDEFINED_SYMBOLS=0` because our build of LibUV does not # define all symbols, see the comment about LibUV on WebAssembly further up - # in this file. + # in this file. `leanc.sh` adds `LEAN_EXTRA_LINKER_FLAGS`, which carries the Emscripten + # flags and settings, to every link. string( APPEND LEAN_EXE_LINKER_FLAGS - " ${LIB}/temp/libleanshell.a ${TOOLCHAIN_STATIC_LINKER_FLAGS} ${EMSCRIPTEN_SETTINGS} -lnodefs.js -s EXIT_RUNTIME=1 -s MAIN_MODULE=1 -s LINKABLE=1 -s EXPORT_ALL=1 -s ERROR_ON_UNDEFINED_SYMBOLS=0" + " ${LIB}/temp/libleanshell.a ${TOOLCHAIN_STATIC_LINKER_FLAGS} -lnodefs.js -sEXIT_RUNTIME=1 -sMAIN_MODULE=1 -sEXPORT_ALL=1 -sERROR_ON_UNDEFINED_SYMBOLS=0" ) endif() From 20a4eb607d074aa941e542655840797441779c82 Mon Sep 17 00:00:00 2001 From: Bas van Dijk Date: Sat, 31 Oct 2026 16:24:08 +0000 Subject: [PATCH 12/18] fix: keep Emscripten's profiling runtime from writing `default.profraw` Since Emscripten 4.0.11 the `libclang_rt.builtins` system library bundles LLVM's profiling runtime, and a main module (`-sMAIN_MODULE=1`) links its system libraries as whole archives, so the runtime's static initializer runs in every `lean.js` process and its `atexit` hook writes `default.profraw` into the current directory: 128 bytes after `lean --version`, 640 bytes after a test. That fails CI's check that the test suite leaves the source tree clean and would litter every user's working directory. `lean_main` now points the runtime at `/dev/null`. The symbol is weak, so Emscripten versions without the runtime, such as 3.1.44, link and behave as before. Reported upstream as emscripten-core/emscripten#28123. Co-Authored-By: Claude Fable 5.1 --- src/util/shell.cpp | 10 ++++++++++ 1 file changed, 10 insertions(+) diff --git a/src/util/shell.cpp b/src/util/shell.cpp index 1bf70ae2b1a5..88f89c65ef13 100644 --- a/src/util/shell.cpp +++ b/src/util/shell.cpp @@ -281,8 +281,18 @@ static void report_task_get_blocked_time(std::chrono::nanoseconds d) { } } +#ifdef LEAN_EMSCRIPTEN +// Emscripten's compiler-rt has bundled LLVM's profiling runtime since 4.0.11, and a main module links its system +// libraries as whole archives, so the runtime's `atexit` hook writes `default.profraw` into the current directory of +// every `lean.js` run (emscripten-core/emscripten#28123). Weak because older Emscripten versions do not have the symbol. +extern "C" void __llvm_profile_set_filename(const char *) __attribute__((weak)); +#endif + extern "C" LEAN_EXPORT int lean_main(int argc, char ** argv) { #ifdef LEAN_EMSCRIPTEN + if (__llvm_profile_set_filename) { + __llvm_profile_set_filename("/dev/null"); + } // When running in command-line mode under Node.js, we make system directories available in the virtual filesystem. // This mode is used to compile 32-bit oleans. EM_ASM( From e1ce2789e474f9832002c73623f8dbbeb9e4d048 Mon Sep 17 00:00:00 2001 From: Bas van Dijk Date: Sat, 31 Oct 2026 15:19:22 +0000 Subject: [PATCH 13/18] chore: update the Web Assembly CI job to Emscripten 6.0.13 Emscripten 3.1.44 is from July 2023; 6.0.13 is the current release. `setup-emsdk` installs it directly and keys its cache on the version. The previous commits cover the two changes in Emscripten 6 that affect this build: `-shared` builds real side modules, and `emcc` no longer links the C++ runtime by default. `lean.js` still runs on Node.js 26; emcc uses the Node.js bundled with the SDK for its own passes. Co-Authored-By: Claude Fable 5.1 --- .github/workflows/build-template.yml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.github/workflows/build-template.yml b/.github/workflows/build-template.yml index 9582974324ca..6518ea8cc9bd 100644 --- a/.github/workflows/build-template.yml +++ b/.github/workflows/build-template.yml @@ -82,7 +82,7 @@ jobs: - name: Setup emsdk uses: emscripten-core/setup-emsdk@4528d102f7230f0e7b276855c01ea1159be0e984 # v16 with: - version: 3.1.44 + version: 6.0.13 actions-cache-folder: emsdk if: matrix.wasm - name: Setup Node.js From e80c5658f3e7c15a79962f38d5a7595169a944c1 Mon Sep 17 00:00:00 2001 From: Bas van Dijk Date: Sat, 31 Oct 2026 15:19:22 +0000 Subject: [PATCH 14/18] doc: describe the WebAssembly build of `lean.js` The page described the Lean 3 build (`emconfigure`, the `lean_js_js` and `lean_js_wasm` targets, lean-web-editor) and was linked from nowhere. It now describes the build as the Web Assembly CI job runs it: a native 32-bit stage 0 compiles the `.olean` files, Emscripten cross-compiles stage 1 into `lean.js` and `lean.wasm`, Node.js 24 or newer runs them through the `bin/lean` launcher, and the tests run one at a time. `ci.yml` and `build-template.yml` remain the authoritative source of the flags and the SDK version. `doc/make/index.md` links the page. Co-Authored-By: Claude Fable 5.1 --- doc/make/emscripten.md | 40 +++++++++++++++++++++++++++++++++------- doc/make/index.md | 1 + 2 files changed, 34 insertions(+), 7 deletions(-) diff --git a/doc/make/emscripten.md b/doc/make/emscripten.md index 36c764b2f7fb..c3cbb53f0bce 100644 --- a/doc/make/emscripten.md +++ b/doc/make/emscripten.md @@ -1,12 +1,38 @@ -# Compiling lean.js via Emscripten +# Building `lean.js` with Emscripten -First install Emscripten via your distribution's package manager or [download and install it](https://kripken.github.io/emscripten-site/docs/getting_started/downloads.html) yourself. Then build asm.js and WebAssembly binaries using +Lean can be cross-compiled to WebAssembly with [Emscripten](https://emscripten.org/). The result is a command-line `lean` for Node.js: `bin/lean.js` and `bin/lean.wasm`, started through the `bin/lean` launcher script. Lake, `leanc` and the other tools are not built for this target, and the build is not released. The "Web Assembly" job in [`.github/workflows/ci.yml`](../../.github/workflows/ci.yml) builds and tests it on nightlies, on releases and on PRs labeled `release-ci`; its `CMAKE_OPTIONS` there and the Emscripten SDK version in [`.github/workflows/build-template.yml`](../../.github/workflows/build-template.yml) are the authoritative configuration. This page explains how that build is put together. + +## Requirements + +- The [Emscripten SDK](https://github.com/emscripten-core/emsdk) at the version `build-template.yml` installs, installed and activated. +- Node.js 24 or newer on the `PATH` to run `lean.js`: `lean.wasm` exports all of its about 250,000 symbols, and V8 accepts more than 100,000 exports only from Node.js 24 on. `emcc` itself uses the Node.js bundled with the SDK. +- A native toolchain and 32-bit libraries for stage 0; on Ubuntu `clang`, `gcc-multilib`, `g++-multilib`, `libuv1-dev:i386`, `libssl-dev:i386` and `pkgconf:i386`, in addition to the [usual build tools](index.md). + +## How the build works + +As in a native build, stage 0 compiles stage 1 (see [bootstrapping](../dev/bootstrap.md)), but the two stages target different platforms: + +1. Stage 0 is a native 32-bit `lean`, built with `clang -m32` against the i386 libraries, without GMP and without `mmap` (the `STAGE0_*` options). It compiles the `.olean` files of stage 1, which must come from a 32-bit compiler because `lean.wasm` is a 32-bit program and `.olean` files depend on the pointer size. +2. Stage 1 is cross-compiled with Emscripten's CMake toolchain file and archived with `emar`. It builds libuv itself, uses neither GMP, `mmap` nor mimalloc, and links `Init`, `Std`, `Lean`, the runtime and the shell statically into `lean.js` and `lean.wasm`. The link uses `-sMAIN_MODULE=1 -sEXPORT_ALL=1` so that every symbol stays available to the interpreter, as `-rdynamic` does natively; the Emscripten flags are set in `src/CMakeLists.txt`. + +Under Node.js, `lean.js` mounts the host's `/home` and `/tmp` into Emscripten's virtual file system and changes into the host's working directory there (`lean_main` in `src/util/shell.cpp`), so it can only read and write files below these two directories and must be started from a directory below one of them. + +## Building + +Take the "Web Assembly" entry's `CMAKE_OPTIONS` from `ci.yml`, replace `$GITHUB_WORKSPACE/emsdk/emsdk-main` with your emsdk directory, and run in a fresh `build` directory, with the emsdk activated and Node.js 24 or newer on the `PATH`: ```bash -mkdir -p build/emscripten -cd build/emscripten -emconfigure cmake ../../src -DCMAKE_BUILD_TYPE=Emscripten -make lean_js_js lean_js_wasm +cmake .. --preset release -B . -DLEAN_INSTALL_PREFIX=$PWD/.. +make stage1 -j$(nproc) +make -C stage1 install ``` -This will produce files `lean_js_js.js`, `lean_js_wasm.js`, and `lean_js_wasm.wasm` in `shell/`, which you can e.g. copy to the `dist/` directory in [lean-web-editor](https://github.com/leanprover/lean-web-editor) instead of calling `./fetch_lean_js.sh` there. +The last command installs into `lean--linux_wasm32`. Linking `lean.js` is the expensive part: one link of the C++ runtime's LTO bitcode together with the Lean-generated code, followed by emcc's JavaScript passes over a file of more than 100 MiB, for which `src/stdlib.make.in` raises Node.js's heap limit. + +## Running tests + +`stage1/bin/lean` runs `node --stack-size=8192 lean.js` with its arguments, so the test suite can call `lean` as usual. A WebAssembly `lean` process can need several gigabytes of memory and is slow, so CI runs only a few tests, one at a time. From the repository root: + +```bash +ctest --preset release --test-dir build/stage1 --no-tests=error -j1 -R '^(elab_fail/1007|elab/(Format|1037|ac_rfl|tempfile|libuv))\.lean$' +``` diff --git a/doc/make/index.md b/doc/make/index.md index 011a2523a189..06056267479a 100644 --- a/doc/make/index.md +++ b/doc/make/index.md @@ -19,6 +19,7 @@ Platform-Specific Setup - [Windows (WSL)](wsl.md) - [macOS (homebrew)](osx-10.9.md) - Linux/macOS/WSL via [Nix](https://nixos.org/nix/): Call `nix develop` in the project root. That's it. +- [WebAssembly via Emscripten](emscripten.md), the cross-compiled build that CI tests Generic Build Instructions -------------------------- From d02b4f3bd8b842afb5aed008879fb1431c84c488 Mon Sep 17 00:00:00 2001 From: Bas van Dijk Date: Sun, 1 Nov 2026 00:09:22 +0000 Subject: [PATCH 15/18] perf: resolve the interpreter's native symbols inside lean.wasm The interpreter switches to native code by looking up a declaration's mangled symbol at run time. In `lean.js` that lookup went through Emscripten's `dlsym`, which enumerates every export of the module on each call (`Object.keys(lib.exports).indexOf(symbol)` in `_dlsym_js`, Emscripten 6.0.13); with about 250,000 exports one lookup costs 65 to 130 ms, and `lean` performs one per imported module and two per imported parser constant at startup, 2,630 of them for `Init`, which is most of the time a test takes on the Web Assembly CI job. `lean.js` now carries its own symbol table. `script/wasm_symbols.py` reads the global symbols of the Lean archives that `lean.js` links (`libInit.a`, `libStd.a`, `libLean.a`) from their wasm object files, which also give each function's type, and writes a sorted name/address table with a binary-search lookup, `lean_lookup_native_symbol`, which `lookup_symbol_in_cur_exe` consults on Emscripten; since the table holds every symbol of those archives, only the runtime's symbols are still looked up with `dlsym`. `stdlib.make` builds the table and links it into `lean.js`. It is about 28 MB of static data (the names alone are 25 MB), so the link's initial memory is raised from Emscripten's default 16 MB to 64 MB. The script also writes the list of the runtime archives' global symbols, which the next commit uses as the export list. On an AMD EPYC 7302 with Emscripten 6.0.13 and Node.js 26, `lean` on an empty file takes 21 s instead of 236 s (210 s of which were the 2,630 `dlsym` calls; now there are none), `tests/elab/Format.lean` 27 s instead of 193 s, and the six tests of the CI job 2 m 42 s instead of about 20 m. Lean's own profiler reports import 2.1 s instead of 57 s and interpretation 10 ms instead of 161 s. Co-Authored-By: Claude Fable 5.1 --- script/wasm_symbols.py | 249 +++++++++++++++++++++++++++++++++ src/CMakeLists.txt | 4 +- src/library/ir_interpreter.cpp | 20 +++ src/stdlib.make.in | 18 ++- 4 files changed, 287 insertions(+), 4 deletions(-) create mode 100755 script/wasm_symbols.py diff --git a/script/wasm_symbols.py b/script/wasm_symbols.py new file mode 100755 index 000000000000..41ebbc23c2d6 --- /dev/null +++ b/script/wasm_symbols.py @@ -0,0 +1,249 @@ +#!/usr/bin/env python3 +# Copyright (c) 2026 Bas van Dijk. All rights reserved. +# Released under Apache 2.0 license as described in the file LICENSE. +# Author: Bas van Dijk +""" +Generate the native symbol table and the export list of `lean.js`. + +Usage: wasm_symbols.py --nm NM --registry OUT.c --exports OUT.json --lean ARCHIVE... --runtime ARCHIVE... + +The interpreter switches to native code by looking up a declaration's mangled symbol at run time +(`lookup_symbol_in_cur_exe` in `src/library/ir_interpreter.cpp`). Natively the dynamic symbol table of +`libleanshared.so` answers that; in `lean.js` the table lives inside the module instead, because Emscripten's +`dlsym` enumerates every export on each call and every export costs JavaScript in every pthread. + +The table holds every global symbol of the Lean archives (`libInit.a`, `libStd.a`, `libLean.a`): the compiled +declarations, their constants and the module initializers. Their wasm object files give each function's type, so +the table's declarations match the definitions exactly. The export list for `-sEXPORTED_FUNCTIONS=@file` holds the +global symbols of the runtime archives, which the interpreter still resolves through `dlsym`. +""" +import argparse +import json +import os +import struct +import subprocess +import sys + +# Emscripten's own metadata symbols never survive as wasm exports, and the link synthesizes `main` from its +# `__main_argc_argv`/`__main_void` alias, which therefore cannot be requested +NOT_EXPORTED = ('_Z', '__em_js__', '__em_lib_deps_', '__start_em_', '__stop_em_') +MAIN_ALIASES = ('__main_argc_argv', '__main_void') +VALTYPES = {0x7f: 'int', 0x7e: 'long long', 0x7d: 'float', 0x7c: 'double'} +SYM_BINDING_LOCAL, SYM_UNDEFINED, SYM_EXPLICIT_NAME = 0x2, 0x10, 0x40 + + +class Reader: + def __init__(self, data): + self.data, self.pos = data, 0 + + def byte(self): + self.pos += 1 + return self.data[self.pos - 1] + + def leb(self): + result = shift = 0 + while True: + b = self.byte() + result |= (b & 0x7f) << shift + shift += 7 + if not b & 0x80: + return result + + def bytes(self, n): + self.pos += n + return self.data[self.pos - n:self.pos] + + def name(self): + return self.bytes(self.leb()).decode() + + def done(self): + return self.pos >= len(self.data) + + +def archive_members(path): + """(name, data) of every member of a GNU `ar` archive""" + with open(path, 'rb') as f: + data = f.read() + if data[:8] != b'!\n': + sys.exit(f'wasm_symbols.py: {path} is not an ar archive') + pos, long_names = 8, b'' + while pos + 60 <= len(data): + header = data[pos:pos + 60] + name, size = header[:16].decode().rstrip(), int(header[48:58]) + body = data[pos + 60:pos + 60 + size] + pos += 60 + size + (size & 1) + if name == '//': + long_names = body + elif name.startswith('/') and name[1:].isdigit(): + start = int(name[1:]) + yield long_names[start:long_names.index(b'\n', start)].decode().rstrip('/'), body + elif name != '/': + yield name.rstrip('/'), body + + +def wasm_symbols(data): + """name -> (params, results) for the defined global functions, name -> None for the defined global data""" + r = Reader(data) + if r.bytes(4) != b'\0asm': + return None + r.bytes(4) + types, imported_functions, function_types, linking = [], 0, [], None + while not r.done(): + section_id, size = r.byte(), r.leb() + section = Reader(r.bytes(size)) + if section_id == 1: + for _ in range(section.leb()): + section.byte() + params = [VALTYPES[section.byte()] for _ in range(section.leb())] + results = [VALTYPES[section.byte()] for _ in range(section.leb())] + types.append((params, results)) + elif section_id == 2: + for _ in range(section.leb()): + section.name(), section.name() + kind = section.byte() + if kind == 0: + imported_functions += 1 + section.leb() + elif kind in (1, 2): # table: reftype then limits; memory: limits + if kind == 1: + section.byte() + flags = section.byte() + section.leb() + if flags & 1: + section.leb() + elif kind == 3: + section.byte(), section.byte() + elif kind == 4: + section.byte(), section.leb() + elif section_id == 3: + function_types = [section.leb() for _ in range(section.leb())] + elif section_id == 0 and section.name() == 'linking': + linking = section + symbols = {} + if linking is None: + return symbols + linking.leb() + while not linking.done(): + subsection_id, size = linking.byte(), linking.leb() + sub = Reader(linking.bytes(size)) + if subsection_id != 8: + continue + for _ in range(sub.leb()): + kind, flags = sub.byte(), sub.leb() + defined = not flags & SYM_UNDEFINED + if kind == 0: + index = sub.leb() + if defined or flags & SYM_EXPLICIT_NAME: + name = sub.name() + if defined and not flags & SYM_BINDING_LOCAL: + symbols[name] = types[function_types[index - imported_functions]] + elif kind == 1: + name = sub.name() + if defined: + sub.leb(), sub.leb(), sub.leb() + if not flags & SYM_BINDING_LOCAL: + symbols[name] = None + elif kind in (2, 4, 5): + sub.leb() + if defined or flags & SYM_EXPLICIT_NAME: + sub.name() + elif kind == 3: + sub.leb() + return symbols + + +def list_symbols(nm, archive): + """name -> set of `nm` type letters of the global symbols defined in `archive`""" + out = subprocess.run([nm, '--defined-only', '--extern-only', '--format=posix', archive], + check=True, capture_output=True, text=True).stdout + symbols = {} + for line in out.splitlines(): + fields = line.split() + if len(fields) < 2 or line.endswith(':'): + continue + symbols.setdefault(fields[0], set()).add(fields[1]) + return symbols + + +def write_if_changed(path, content): + if os.path.exists(path): + with open(path, encoding='utf-8') as f: + if f.read() == content: + return False + with open(path, 'w', encoding='utf-8') as f: + f.write(content) + return True + + +def declaration(name, signature): + if signature is None: + return f'extern char {name}[];' + params, results = signature + return f'extern {results[0] if results else "void"} {name}({", ".join(params) or "void"});' + + +def main(): + ap = argparse.ArgumentParser() + ap.add_argument('--nm', required=True, help='llvm-nm (or emnm) that understands the archives') + ap.add_argument('--registry', required=True, help='C file to write') + ap.add_argument('--exports', required=True, help='JSON file to write (EXPORTED_FUNCTIONS=@file)') + ap.add_argument('--lean', nargs='+', required=True, help='the archives of compiled Lean code (wasm objects)') + ap.add_argument('--runtime', nargs='+', required=True, help='the C and C++ archives') + args = ap.parse_args() + + table = {} + for archive in args.lean: + for member, data in archive_members(archive): + symbols = wasm_symbols(data) + if symbols is None: + sys.exit(f'wasm_symbols.py: {archive}({member}) is not a wasm object') + table.update(symbols) + listed = set(list_symbols(args.nm, archive)) + if listed != set(table) & listed or not listed <= set(table): + sys.exit(f'wasm_symbols.py: the symbols read from {archive} differ from what {args.nm} lists: ' + f'{sorted(listed ^ (set(table) & listed) | (listed - set(table)))[:10]}') + runtime = {} + for archive in args.runtime: + runtime.update(list_symbols(args.nm, archive)) + if not all(name.isascii() for name in list(table) + list(runtime)): + sys.exit('wasm_symbols.py: non-ASCII symbol name') + exported = sorted(name for name in runtime + if name not in table and name.isidentifier() + and not name.startswith(NOT_EXPORTED) and name not in MAIN_ALIASES) + + names = sorted(table) + lines = ['// Generated by script/wasm_symbols.py from the Lean archives that `lean.js` links; do not edit.', + '#include ', ''] + lines += [declaration(name, table[name]) for name in names] + lines += ['', 'static const struct { const char * name; void * addr; } lean_native_symbols[] = {'] + lines += [f' {{"{name}", (void *){"&" if table[name] is not None else ""}{name}}},' for name in names] + lines += ['};', '', + '// the interpreter\'s symbol lookup on Emscripten, see `lookup_symbol_in_cur_exe`', + 'void * lean_lookup_native_symbol(char const * name) {', + ' size_t lo = 0, hi = sizeof(lean_native_symbols) / sizeof(lean_native_symbols[0]);', + ' while (lo < hi) {', + ' size_t mid = lo + (hi - lo) / 2;', + ' int c = strcmp(name, lean_native_symbols[mid].name);', + ' if (c == 0) {', + ' return lean_native_symbols[mid].addr;', + ' } else if (c < 0) {', + ' hi = mid;', + ' } else {', + ' lo = mid + 1;', + ' }', + ' }', + ' return NULL;', + '}', ''] + registry_changed = write_if_changed(args.registry, '\n'.join(lines)) + + exports = sorted(set(['_' + name for name in exported] + ['_main', '_malloc', '_free', '_lean_lookup_native_symbol'])) + exports_changed = write_if_changed(args.exports, json.dumps(exports, indent=1) + '\n') + + functions = sum(1 for name in names if table[name] is not None) + print(f'wasm_symbols.py: {len(names)} symbols in the table ({functions} functions, {len(names) - functions} data), ' + f'{len(exports)} exports; {"rewrote" if registry_changed else "kept"} {args.registry}, ' + f'{"rewrote" if exports_changed else "kept"} {args.exports}') + + +if __name__ == '__main__': + main() diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 4cf867ab0035..27fa3b1fe708 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -166,7 +166,9 @@ if(CMAKE_SYSTEM_NAME MATCHES "Emscripten") # `-s` settings only take effect when linking; emcc warns when they are passed to a compilation set(EMSCRIPTEN_FLAGS "-fwasm-exceptions -pthread -flto") - set(EMSCRIPTEN_LINK_SETTINGS "-sALLOW_MEMORY_GROWTH=1") + # the interpreter's symbol table (`lib/temp/lean_symbols.c`, see `stdlib.make.in`) is about 30 MB of static + # data, more than Emscripten's default initial memory of 16 MB + set(EMSCRIPTEN_LINK_SETTINGS "-sALLOW_MEMORY_GROWTH=1 -sINITIAL_MEMORY=64MB") string(APPEND LEANC_EXTRA_CC_FLAGS " -pthread") string(APPEND LEAN_EXTRA_CXX_FLAGS " -D LEAN_EMSCRIPTEN ${EMSCRIPTEN_FLAGS}") string(APPEND LEAN_EXTRA_LINKER_FLAGS " ${EMSCRIPTEN_FLAGS} ${EMSCRIPTEN_LINK_SETTINGS}") diff --git a/src/library/ir_interpreter.cpp b/src/library/ir_interpreter.cpp index c08c4d65800a..241f1af39b8d 100644 --- a/src/library/ir_interpreter.cpp +++ b/src/library/ir_interpreter.cpp @@ -27,6 +27,7 @@ functions, which have a (relatively) homogeneous ABI that we can use without run `call/lookup_symbol` below. */ +#include #include #include #include @@ -339,7 +340,26 @@ void print_value(tout const & ios, value const & v, type t) { return print_value(const_cast(ios), v, t); } +#ifdef LEAN_EMSCRIPTEN +// `lean.js` keeps the interpreter's symbol table inside the module (see `script/wasm_symbols.py`): Emscripten's +// `dlsym` enumerates the export list on every call, and exporting all of Lean costs JavaScript per symbol in every +// pthread. Weak so that other Emscripten programs can link `libleancpp.a` without the table. +extern "C" void * lean_lookup_native_symbol(char const * sym) __attribute__((weak)); +#endif + void * lookup_symbol_in_cur_exe(char const * sym) { +#ifdef LEAN_EMSCRIPTEN + if (lean_lookup_native_symbol) { + if (void * addr = lean_lookup_native_symbol(sym)) { + return addr; + } + // the table holds every symbol of the Lean archives, so a compiled declaration that is not in it is not in + // `lean.js` at all; only the runtime's symbols are left to `dlsym` + if (strncmp(sym, "l_", 2) == 0 || strncmp(sym, "lp_", 3) == 0) { + return nullptr; + } + } +#endif #ifdef LEAN_WINDOWS std::vector hmods(128); DWORD bytes_needed; diff --git a/src/stdlib.make.in b/src/stdlib.make.in index 00012776a960..9a687cbe85d7 100644 --- a/src/stdlib.make.in +++ b/src/stdlib.make.in @@ -125,7 +125,7 @@ $(OUTBIN)/leanchecker$(EXE): $(OUTARC)/libLeanChecker.a.trace $(OUTBIN)/leanchecker-paranoid$(EXE): $(OUTARC)/libLeanChecker.a.trace ${LIB}/lean/libInit.a.trace ${LIB}/lean/libStd.a.trace ${LIB}/lean/libLean.a.trace ${LIB}/lean/libLake.a.trace $(OUTBIN)/leanexport$(EXE): $(OUTARC)/libLeanExport.a.trace ifeq "${CMAKE_SYSTEM_NAME}" "Emscripten" -$(OUTBIN)/lean$(EXE): ${LIB}/lean/libInit.a.trace ${LIB}/lean/libStd.a.trace ${LIB}/lean/libLean.a.trace +$(OUTBIN)/lean$(EXE) ${LIB}/temp/lean_symbols.stamp: ${LIB}/lean/libInit.a.trace ${LIB}/lean/libStd.a.trace ${LIB}/lean/libLean.a.trace endif endif @@ -211,13 +211,25 @@ lake: $(OUTBIN)/lake$(EXE) ifeq "${CMAKE_SYSTEM_NAME}" "Emscripten" # the shared libraries are dummies (see `src/CMakeLists.txt`); `lean.js` links these archives (`LEAN_EXE_LINKER_FLAGS`) -$(OUTBIN)/lean$(EXE): ${LIB}/lean/libInit.a ${LIB}/lean/libStd.a ${LIB}/lean/libLean.a ${LIB}/lean/libleancpp.a ${LIB}/lean/libleanrt.a ${LIB}/temp/libleanshell.a +WASM_LEAN_ARCHIVES := ${LIB}/lean/libInit.a ${LIB}/lean/libStd.a ${LIB}/lean/libLean.a +WASM_RUNTIME_ARCHIVES := ${LIB}/temp/libleanmain.a ${LIB}/temp/libleanshell.a ${LIB}/lean/libleancpp.a ${LIB}/lean/libleanrt.a +WASM_SYMBOLS_PY := ${LEAN_SOURCE_DIR}/../script/wasm_symbols.py +# the interpreter's symbol table and the export list of `lean.js` (see `script/wasm_symbols.py`); the script rewrites +# its outputs only when their content changes, so a stamp records the run +${LIB}/temp/lean_symbols.stamp: $(WASM_LEAN_ARCHIVES) $(WASM_RUNTIME_ARCHIVES) $(WASM_SYMBOLS_PY) + python3 $(WASM_SYMBOLS_PY) --nm "${CMAKE_NM}" --registry ${LIB}/temp/lean_symbols.c --exports ${LIB}/temp/lean_exports.json --lean $(WASM_LEAN_ARCHIVES) --runtime $(WASM_RUNTIME_ARCHIVES) && touch $@ +${LIB}/temp/lean_symbols.c ${LIB}/temp/lean_exports.json: ${LIB}/temp/lean_symbols.stamp ; +${LIB}/temp/lean_symbols.o: ${LIB}/temp/lean_symbols.c + @echo "[ ] Building $@" + $(LEANC_SH) -c ${LEANC_OPTS} $< -o $@ +WASM_LINK_INPUTS := ${LIB}/temp/lean_symbols.o +$(OUTBIN)/lean$(EXE): $(WASM_LEAN_ARCHIVES) $(WASM_RUNTIME_ARCHIVES) $(WASM_LINK_INPUTS) ${LIB}/temp/lean_exports.json else $(OUTBIN)/lean$(EXE): $(OUTLIB)/libInit_shared$(SO) $(OUTLIB)/libleanshared_2$(SO) $(OUTLIB)/libleanshared_1$(SO) $(OUTLIB)/libleanshared$(SO) endif $(OUTBIN)/lean$(EXE): ${LIB}/temp/libleanmain.a $(link-preamble) - $(LEANC_SH) ${LIB}/temp/libleanmain.a ${CMAKE_EXE_LINKER_FLAGS_MAKE} ${CMAKE_DYN_EXE_LINKER_FLAGS_MAKE} ${LEAN_EXE_LINKER_FLAGS} ${LEANC_OPTS} -o $@ + $(LEANC_SH) ${LIB}/temp/libleanmain.a $(WASM_LINK_INPUTS) ${CMAKE_EXE_LINKER_FLAGS_MAKE} ${CMAKE_DYN_EXE_LINKER_FLAGS_MAKE} ${LEAN_EXE_LINKER_FLAGS} ${LEANC_OPTS} -o $@ lean: $(OUTBIN)/lean$(EXE) From aab291407b30a390f88a54faf9c76043d860e68c Mon Sep 17 00:00:00 2001 From: Bas van Dijk Date: Sun, 1 Nov 2026 00:10:46 +0000 Subject: [PATCH 16/18] perf: export only the runtime from lean.wasm With the interpreter's symbol table inside the module, `lean.wasm` no longer has to export all of Lean for `dlsym`. `lean.js` is now linked with `-sMAIN_MODULE=2` and the export list that `script/wasm_symbols.py` writes, the global symbols of the C and C++ runtime archives (600 names instead of 247,834 exports), so Emscripten removes unused code and the JavaScript glue no longer declares a variable per export, which was 76% of the 113 MB `lean.js`. Every pthread is a Node.js worker that loads that file, so each thread now starts in 0.5 s instead of 5 s and a `lean` process needs a third of the memory. Such a module includes only the JavaScript library functions the linked code references, so the helpers that Lean's `EM_ASM` blocks use are requested with `EXPORTED_RUNTIME_METHODS`. The Node.js heap override for emcc's JavaScript passes and the two `TODO(WN)` items in `src/CMakeLists.txt` about dead-code elimination and unused system libraries are obsolete and removed, and the comment on the CI job's Node.js step no longer cites the export count. On an AMD EPYC 7302 with Emscripten 6.0.13 and Node.js 26: `lean.js` is 201 KB instead of 113 MB, `lean.wasm` 131 MB instead of 163 MB with the table (135 MB before it), `lean` on an empty file takes 5.0 s instead of 21 s with the table alone (236 s before), `tests/elab/Format.lean` 6.3 s and 1.5 GB instead of 27 s and 5.5 GB (193 s and 5.3 GB before), and the six tests of the CI job 42 s instead of 2 m 42 s (about 20 m before). The eight `uv__*` symbols the link reported undefined disappear with the unused libuv code; the five `lean_uv_*` ones and `dl_iterate_phdr` remain. Co-Authored-By: Claude Fable 5.1 --- .github/workflows/build-template.yml | 2 +- src/CMakeLists.txt | 15 +++++++++------ src/stdlib.make.in | 4 ---- 3 files changed, 10 insertions(+), 11 deletions(-) diff --git a/.github/workflows/build-template.yml b/.github/workflows/build-template.yml index 6518ea8cc9bd..a3f68246a0fd 100644 --- a/.github/workflows/build-template.yml +++ b/.github/workflows/build-template.yml @@ -86,7 +86,7 @@ jobs: actions-cache-folder: emsdk if: matrix.wasm - name: Setup Node.js - # `lean.wasm` has more than 100'000 exports, which V8 only accepts from Node.js 24 on + # `lean.js` runs on Node.js; 26 is the current Active LTS uses: actions/setup-node@v7 with: node-version: 26 diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 27fa3b1fe708..d625f73666aa 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -161,8 +161,6 @@ if(CMAKE_SYSTEM_NAME MATCHES "Emscripten") # TODO(WN): code size/performance tradeoffs # - we're using -O3; it's /okay/ # - -Oz produces quite slow code - # - system libraries such as OpenGL are included in the JS but shouldn't be - # - we need EMSCRIPTEN_KEEPALIVE annotations on exports to run meta-dce (-s MAIN_MODULE=2) # `-s` settings only take effect when linking; emcc warns when they are passed to a compilation set(EMSCRIPTEN_FLAGS "-fwasm-exceptions -pthread -flto") @@ -917,16 +915,21 @@ file(RELATIVE_PATH LIB ${LEAN_SOURCE_DIR} ${CMAKE_BINARY_DIR}/lib) if(CMAKE_SYSTEM_NAME MATCHES "Emscripten") # We do not use dynamic linking via leanshared for Emscripten to keep things - # simple. (And we are not interested in `Lake` anyway.) To use dynamic - # linking, we would probably have to set MAIN_MODULE=2 on `leanshared`, - # SIDE_MODULE=2 on `lean`, and set CMAKE_SHARED_LIBRARY_SUFFIX to ".js". + # simple. (And we are not interested in `Lake` anyway.) `lean.js` is still a main + # module so that the interpreter can look up the runtime's symbols with `dlsym`; the + # compiled Lean code it looks up is in the table that `script/wasm_symbols.py` + # generates (see `stdlib.make.in`), which also writes the list of exported symbols. + # `MAIN_MODULE=2` removes unused code and exports only that list; such a module + # includes only the JavaScript library functions the linked code references, so the + # helpers that the `EM_ASM` blocks in `src/util/shell.cpp` and `src/runtime/io.cpp` + # use are requested explicitly. # We set `ERROR_ON_UNDEFINED_SYMBOLS=0` because our build of LibUV does not # define all symbols, see the comment about LibUV on WebAssembly further up # in this file. `leanc.sh` adds `LEAN_EXTRA_LINKER_FLAGS`, which carries the Emscripten # flags and settings, to every link. string( APPEND LEAN_EXE_LINKER_FLAGS - " ${LIB}/temp/libleanshell.a ${TOOLCHAIN_STATIC_LINKER_FLAGS} -lnodefs.js -sEXIT_RUNTIME=1 -sMAIN_MODULE=1 -sEXPORT_ALL=1 -sERROR_ON_UNDEFINED_SYMBOLS=0" + " ${LIB}/temp/libleanshell.a ${TOOLCHAIN_STATIC_LINKER_FLAGS} -lnodefs.js -sEXIT_RUNTIME=1 -sMAIN_MODULE=2 -sEXPORTED_FUNCTIONS=@${LIB}/temp/lean_exports.json -sEXPORTED_RUNTIME_METHODS=FS,ENV,UTF8ToString,lengthBytesUTF8,stringToUTF8 -sERROR_ON_UNDEFINED_SYMBOLS=0" ) endif() diff --git a/src/stdlib.make.in b/src/stdlib.make.in index 9a687cbe85d7..ed17b3c58f2e 100644 --- a/src/stdlib.make.in +++ b/src/stdlib.make.in @@ -16,10 +16,6 @@ else export LEAN_CC=${CMAKE_C_COMPILER_LAUNCHER} ${CMAKE_C_COMPILER} endif export LEAN_ABORT_ON_PANIC=1 -ifeq "${CMAKE_SYSTEM_NAME}" "Emscripten" - # emcc's JavaScript passes over the large `lean.js` need more than Node's default heap of about 4 GB - export NODE_OPTIONS += --max-old-space-size=8192 -endif # Short aliases for verbose CMake variables OUTLIB := ${CMAKE_LIBRARY_OUTPUT_DIRECTORY} From cf685f6eab1f816b5caf9c68202832986c5588e1 Mon Sep 17 00:00:00 2001 From: Bas van Dijk Date: Sun, 1 Nov 2026 00:12:16 +0000 Subject: [PATCH 17/18] doc: describe the native symbol table of lean.js Replace the sentences in `doc/make/emscripten.md` about `lean.wasm` exporting about 250,000 symbols, the Node.js version that requires, `-sMAIN_MODULE=1 -sEXPORT_ALL=1` and the Node.js heap limit of the link with how the interpreter finds compiled code in `lean.js`: the table that `script/wasm_symbols.py` generates from the Lean archives and the export list of the runtime archives. Co-Authored-By: Claude Fable 5.1 --- doc/make/emscripten.md | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/doc/make/emscripten.md b/doc/make/emscripten.md index c3cbb53f0bce..141e33e8738d 100644 --- a/doc/make/emscripten.md +++ b/doc/make/emscripten.md @@ -5,7 +5,7 @@ Lean can be cross-compiled to WebAssembly with [Emscripten](https://emscripten.o ## Requirements - The [Emscripten SDK](https://github.com/emscripten-core/emsdk) at the version `build-template.yml` installs, installed and activated. -- Node.js 24 or newer on the `PATH` to run `lean.js`: `lean.wasm` exports all of its about 250,000 symbols, and V8 accepts more than 100,000 exports only from Node.js 24 on. `emcc` itself uses the Node.js bundled with the SDK. +- Node.js on the `PATH` to run `lean.js`; the CI job installs Node.js 26. `emcc` itself uses the Node.js bundled with the SDK. - A native toolchain and 32-bit libraries for stage 0; on Ubuntu `clang`, `gcc-multilib`, `g++-multilib`, `libuv1-dev:i386`, `libssl-dev:i386` and `pkgconf:i386`, in addition to the [usual build tools](index.md). ## How the build works @@ -13,13 +13,13 @@ Lean can be cross-compiled to WebAssembly with [Emscripten](https://emscripten.o As in a native build, stage 0 compiles stage 1 (see [bootstrapping](../dev/bootstrap.md)), but the two stages target different platforms: 1. Stage 0 is a native 32-bit `lean`, built with `clang -m32` against the i386 libraries, without GMP and without `mmap` (the `STAGE0_*` options). It compiles the `.olean` files of stage 1, which must come from a 32-bit compiler because `lean.wasm` is a 32-bit program and `.olean` files depend on the pointer size. -2. Stage 1 is cross-compiled with Emscripten's CMake toolchain file and archived with `emar`. It builds libuv itself, uses neither GMP, `mmap` nor mimalloc, and links `Init`, `Std`, `Lean`, the runtime and the shell statically into `lean.js` and `lean.wasm`. The link uses `-sMAIN_MODULE=1 -sEXPORT_ALL=1` so that every symbol stays available to the interpreter, as `-rdynamic` does natively; the Emscripten flags are set in `src/CMakeLists.txt`. +2. Stage 1 is cross-compiled with Emscripten's CMake toolchain file and archived with `emar`. It builds libuv itself, uses neither GMP, `mmap` nor mimalloc, and links `Init`, `Std`, `Lean`, the runtime and the shell statically into `lean.js` and `lean.wasm`. The interpreter finds compiled Lean code by symbol name; natively the dynamic symbol table answers that (`-rdynamic`), in `lean.js` a table inside the module does: `script/wasm_symbols.py` reads the symbols of the Lean archives from their object files and writes `lib/temp/lean_symbols.c`, which `stdlib.make` compiles and links into `lean.js`, and `lib/temp/lean_exports.json`, the symbols of the runtime archives that `lean.wasm` exports for `dlsym` (`-sMAIN_MODULE=2 -sEXPORTED_FUNCTIONS`). The Emscripten flags are set in `src/CMakeLists.txt`. Under Node.js, `lean.js` mounts the host's `/home` and `/tmp` into Emscripten's virtual file system and changes into the host's working directory there (`lean_main` in `src/util/shell.cpp`), so it can only read and write files below these two directories and must be started from a directory below one of them. ## Building -Take the "Web Assembly" entry's `CMAKE_OPTIONS` from `ci.yml`, replace `$GITHUB_WORKSPACE/emsdk/emsdk-main` with your emsdk directory, and run in a fresh `build` directory, with the emsdk activated and Node.js 24 or newer on the `PATH`: +Take the "Web Assembly" entry's `CMAKE_OPTIONS` from `ci.yml`, replace `$GITHUB_WORKSPACE/emsdk/emsdk-main` with your emsdk directory, and run in a fresh `build` directory, with the emsdk activated and Node.js on the `PATH`: ```bash cmake .. --preset release -B . -DLEAN_INSTALL_PREFIX=$PWD/.. @@ -27,7 +27,7 @@ make stage1 -j$(nproc) make -C stage1 install ``` -The last command installs into `lean--linux_wasm32`. Linking `lean.js` is the expensive part: one link of the C++ runtime's LTO bitcode together with the Lean-generated code, followed by emcc's JavaScript passes over a file of more than 100 MiB, for which `src/stdlib.make.in` raises Node.js's heap limit. +The last command installs into `lean--linux_wasm32`. Linking `lean.js` is the expensive part: one link of the C++ runtime's LTO bitcode together with the Lean-generated code, followed by emcc's JavaScript passes. ## Running tests From 6f1180cc50da91466a2819fc96af57e2719521c3 Mon Sep 17 00:00:00 2001 From: Bas van Dijk Date: Mon, 2 Nov 2026 13:30:15 +0100 Subject: [PATCH 18/18] chore: remove copyright statement in `script/wasm_symbols.py` --- script/wasm_symbols.py | 3 --- 1 file changed, 3 deletions(-) diff --git a/script/wasm_symbols.py b/script/wasm_symbols.py index 41ebbc23c2d6..bfe042f5e3eb 100755 --- a/script/wasm_symbols.py +++ b/script/wasm_symbols.py @@ -1,7 +1,4 @@ #!/usr/bin/env python3 -# Copyright (c) 2026 Bas van Dijk. All rights reserved. -# Released under Apache 2.0 license as described in the file LICENSE. -# Author: Bas van Dijk """ Generate the native symbol table and the export list of `lean.js`.