diff --git a/.github/workflows/build-template.yml b/.github/workflows/build-template.yml index a4dd854b0e15..6518ea8cc9bd 100644 --- a/.github/workflows/build-template.yml +++ b/.github/workflows/build-template.yml @@ -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/")" diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 56cfc91607e7..09e26c71d341 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -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 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 -------------------------- diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 4604704aff0f..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 @@ -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 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/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; 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() diff --git a/src/stdlib.make.in b/src/stdlib.make.in index 055547f4be5e..00012776a960 100644 --- 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 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( 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'")