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/14] 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/14] 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/14] 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/14] 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/14] 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/14] 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/14] 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/14] 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/14] 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/14] 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/14] 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/14] 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/14] 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/14] 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 --------------------------