basvandijk · Oct 30, 2026 · Oct 30, 2026 · Oct 30, 2026 · Oct 30, 2026 · Oct 30, 2026
@@ -82,9 +82,15 @@ 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
+        # `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/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 . <CMAKE_OPTIONS> -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-<version>-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
@@ -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
 --------------------------

diff --git 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
@@ -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)
@@ -917,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()
 
@@ -971,10 +975,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}
   )
+  # `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
+    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/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
 
@@ -111,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
@@ -193,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 $@
 

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

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