basvandijk · Oct 30, 2026 · Oct 30, 2026 · Oct 30, 2026 · Oct 30, 2026 · Oct 30, 2026
@@ -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/")"

@@ -426,20 +426,28 @@ 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. 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.
             for (const job of matrix) {

diff --git 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}

diff --git 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/runtime/io.cpp b/src/runtime/io.cpp
@@ -57,12 +57,10 @@ Authors: Leonardo de Moura, Sebastian Ullrich
 #include <dirent.h>
 #endif
 
-#ifndef LEAN_WINDOWS
-#ifndef __APPLE__
+#if !defined(LEAN_WINDOWS) && !defined(__APPLE__) && !defined(LEAN_EMSCRIPTEN)
 #include <sys/syscall.h>
 #include <linux/fs.h> // 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;

diff --git 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()
diff --git a/src/stdlib.make.in b/src/stdlib.make.in
@@ -8,10 +8,18 @@ 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
 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}
@@ -54,9 +62,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
 

diff --git 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'")