From e9e78b57a77eefd55539d28666cdc59b81673e6a Mon Sep 17 00:00:00 2001 From: Bas van Dijk Date: Fri, 30 Oct 2026 15:19:23 +0000 Subject: [PATCH 1/8] 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 2/8] 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 3/8] 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 4/8] 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 5/8] 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 6/8] 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 7/8] 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 8/8] 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}