diff --git a/.github/workflows/build-template.yml b/.github/workflows/build-template.yml index a4dd854b0e15..a3f68246a0fd 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.js` runs on Node.js; 26 is the current Active LTS + 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..141e33e8738d 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 on the `PATH` to run `lean.js`; the CI job installs Node.js 26. `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 interpreter finds compiled Lean code by symbol name; natively the dynamic symbol table answers that (`-rdynamic`), in `lean.js` a table inside the module does: `script/wasm_symbols.py` reads the symbols of the Lean archives from their object files and writes `lib/temp/lean_symbols.c`, which `stdlib.make` compiles and links into `lean.js`, and `lib/temp/lean_exports.json`, the symbols of the runtime archives that `lean.wasm` exports for `dlsym` (`-sMAIN_MODULE=2 -sEXPORTED_FUNCTIONS`). 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 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. + +## 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/script/wasm_symbols.py b/script/wasm_symbols.py new file mode 100755 index 000000000000..bfe042f5e3eb --- /dev/null +++ b/script/wasm_symbols.py @@ -0,0 +1,246 @@ +#!/usr/bin/env python3 +""" +Generate the native symbol table and the export list of `lean.js`. + +Usage: wasm_symbols.py --nm NM --registry OUT.c --exports OUT.json --lean ARCHIVE... --runtime ARCHIVE... + +The interpreter switches to native code by looking up a declaration's mangled symbol at run time +(`lookup_symbol_in_cur_exe` in `src/library/ir_interpreter.cpp`). Natively the dynamic symbol table of +`libleanshared.so` answers that; in `lean.js` the table lives inside the module instead, because Emscripten's +`dlsym` enumerates every export on each call and every export costs JavaScript in every pthread. + +The table holds every global symbol of the Lean archives (`libInit.a`, `libStd.a`, `libLean.a`): the compiled +declarations, their constants and the module initializers. Their wasm object files give each function's type, so +the table's declarations match the definitions exactly. The export list for `-sEXPORTED_FUNCTIONS=@file` holds the +global symbols of the runtime archives, which the interpreter still resolves through `dlsym`. +""" +import argparse +import json +import os +import struct +import subprocess +import sys + +# Emscripten's own metadata symbols never survive as wasm exports, and the link synthesizes `main` from its +# `__main_argc_argv`/`__main_void` alias, which therefore cannot be requested +NOT_EXPORTED = ('_Z', '__em_js__', '__em_lib_deps_', '__start_em_', '__stop_em_') +MAIN_ALIASES = ('__main_argc_argv', '__main_void') +VALTYPES = {0x7f: 'int', 0x7e: 'long long', 0x7d: 'float', 0x7c: 'double'} +SYM_BINDING_LOCAL, SYM_UNDEFINED, SYM_EXPLICIT_NAME = 0x2, 0x10, 0x40 + + +class Reader: + def __init__(self, data): + self.data, self.pos = data, 0 + + def byte(self): + self.pos += 1 + return self.data[self.pos - 1] + + def leb(self): + result = shift = 0 + while True: + b = self.byte() + result |= (b & 0x7f) << shift + shift += 7 + if not b & 0x80: + return result + + def bytes(self, n): + self.pos += n + return self.data[self.pos - n:self.pos] + + def name(self): + return self.bytes(self.leb()).decode() + + def done(self): + return self.pos >= len(self.data) + + +def archive_members(path): + """(name, data) of every member of a GNU `ar` archive""" + with open(path, 'rb') as f: + data = f.read() + if data[:8] != b'!\n': + sys.exit(f'wasm_symbols.py: {path} is not an ar archive') + pos, long_names = 8, b'' + while pos + 60 <= len(data): + header = data[pos:pos + 60] + name, size = header[:16].decode().rstrip(), int(header[48:58]) + body = data[pos + 60:pos + 60 + size] + pos += 60 + size + (size & 1) + if name == '//': + long_names = body + elif name.startswith('/') and name[1:].isdigit(): + start = int(name[1:]) + yield long_names[start:long_names.index(b'\n', start)].decode().rstrip('/'), body + elif name != '/': + yield name.rstrip('/'), body + + +def wasm_symbols(data): + """name -> (params, results) for the defined global functions, name -> None for the defined global data""" + r = Reader(data) + if r.bytes(4) != b'\0asm': + return None + r.bytes(4) + types, imported_functions, function_types, linking = [], 0, [], None + while not r.done(): + section_id, size = r.byte(), r.leb() + section = Reader(r.bytes(size)) + if section_id == 1: + for _ in range(section.leb()): + section.byte() + params = [VALTYPES[section.byte()] for _ in range(section.leb())] + results = [VALTYPES[section.byte()] for _ in range(section.leb())] + types.append((params, results)) + elif section_id == 2: + for _ in range(section.leb()): + section.name(), section.name() + kind = section.byte() + if kind == 0: + imported_functions += 1 + section.leb() + elif kind in (1, 2): # table: reftype then limits; memory: limits + if kind == 1: + section.byte() + flags = section.byte() + section.leb() + if flags & 1: + section.leb() + elif kind == 3: + section.byte(), section.byte() + elif kind == 4: + section.byte(), section.leb() + elif section_id == 3: + function_types = [section.leb() for _ in range(section.leb())] + elif section_id == 0 and section.name() == 'linking': + linking = section + symbols = {} + if linking is None: + return symbols + linking.leb() + while not linking.done(): + subsection_id, size = linking.byte(), linking.leb() + sub = Reader(linking.bytes(size)) + if subsection_id != 8: + continue + for _ in range(sub.leb()): + kind, flags = sub.byte(), sub.leb() + defined = not flags & SYM_UNDEFINED + if kind == 0: + index = sub.leb() + if defined or flags & SYM_EXPLICIT_NAME: + name = sub.name() + if defined and not flags & SYM_BINDING_LOCAL: + symbols[name] = types[function_types[index - imported_functions]] + elif kind == 1: + name = sub.name() + if defined: + sub.leb(), sub.leb(), sub.leb() + if not flags & SYM_BINDING_LOCAL: + symbols[name] = None + elif kind in (2, 4, 5): + sub.leb() + if defined or flags & SYM_EXPLICIT_NAME: + sub.name() + elif kind == 3: + sub.leb() + return symbols + + +def list_symbols(nm, archive): + """name -> set of `nm` type letters of the global symbols defined in `archive`""" + out = subprocess.run([nm, '--defined-only', '--extern-only', '--format=posix', archive], + check=True, capture_output=True, text=True).stdout + symbols = {} + for line in out.splitlines(): + fields = line.split() + if len(fields) < 2 or line.endswith(':'): + continue + symbols.setdefault(fields[0], set()).add(fields[1]) + return symbols + + +def write_if_changed(path, content): + if os.path.exists(path): + with open(path, encoding='utf-8') as f: + if f.read() == content: + return False + with open(path, 'w', encoding='utf-8') as f: + f.write(content) + return True + + +def declaration(name, signature): + if signature is None: + return f'extern char {name}[];' + params, results = signature + return f'extern {results[0] if results else "void"} {name}({", ".join(params) or "void"});' + + +def main(): + ap = argparse.ArgumentParser() + ap.add_argument('--nm', required=True, help='llvm-nm (or emnm) that understands the archives') + ap.add_argument('--registry', required=True, help='C file to write') + ap.add_argument('--exports', required=True, help='JSON file to write (EXPORTED_FUNCTIONS=@file)') + ap.add_argument('--lean', nargs='+', required=True, help='the archives of compiled Lean code (wasm objects)') + ap.add_argument('--runtime', nargs='+', required=True, help='the C and C++ archives') + args = ap.parse_args() + + table = {} + for archive in args.lean: + for member, data in archive_members(archive): + symbols = wasm_symbols(data) + if symbols is None: + sys.exit(f'wasm_symbols.py: {archive}({member}) is not a wasm object') + table.update(symbols) + listed = set(list_symbols(args.nm, archive)) + if listed != set(table) & listed or not listed <= set(table): + sys.exit(f'wasm_symbols.py: the symbols read from {archive} differ from what {args.nm} lists: ' + f'{sorted(listed ^ (set(table) & listed) | (listed - set(table)))[:10]}') + runtime = {} + for archive in args.runtime: + runtime.update(list_symbols(args.nm, archive)) + if not all(name.isascii() for name in list(table) + list(runtime)): + sys.exit('wasm_symbols.py: non-ASCII symbol name') + exported = sorted(name for name in runtime + if name not in table and name.isidentifier() + and not name.startswith(NOT_EXPORTED) and name not in MAIN_ALIASES) + + names = sorted(table) + lines = ['// Generated by script/wasm_symbols.py from the Lean archives that `lean.js` links; do not edit.', + '#include ', ''] + lines += [declaration(name, table[name]) for name in names] + lines += ['', 'static const struct { const char * name; void * addr; } lean_native_symbols[] = {'] + lines += [f' {{"{name}", (void *){"&" if table[name] is not None else ""}{name}}},' for name in names] + lines += ['};', '', + '// the interpreter\'s symbol lookup on Emscripten, see `lookup_symbol_in_cur_exe`', + 'void * lean_lookup_native_symbol(char const * name) {', + ' size_t lo = 0, hi = sizeof(lean_native_symbols) / sizeof(lean_native_symbols[0]);', + ' while (lo < hi) {', + ' size_t mid = lo + (hi - lo) / 2;', + ' int c = strcmp(name, lean_native_symbols[mid].name);', + ' if (c == 0) {', + ' return lean_native_symbols[mid].addr;', + ' } else if (c < 0) {', + ' hi = mid;', + ' } else {', + ' lo = mid + 1;', + ' }', + ' }', + ' return NULL;', + '}', ''] + registry_changed = write_if_changed(args.registry, '\n'.join(lines)) + + exports = sorted(set(['_' + name for name in exported] + ['_main', '_malloc', '_free', '_lean_lookup_native_symbol'])) + exports_changed = write_if_changed(args.exports, json.dumps(exports, indent=1) + '\n') + + functions = sum(1 for name in names if table[name] is not None) + print(f'wasm_symbols.py: {len(names)} symbols in the table ({functions} functions, {len(names) - functions} data), ' + f'{len(exports)} exports; {"rewrote" if registry_changed else "kept"} {args.registry}, ' + f'{"rewrote" if exports_changed else "kept"} {args.exports}') + + +if __name__ == '__main__': + main() diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 4604704aff0f..d625f73666aa 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -161,15 +161,15 @@ if(CMAKE_SYSTEM_NAME MATCHES "Emscripten") # TODO(WN): code size/performance tradeoffs # - we're using -O3; it's /okay/ # - -Oz produces quite slow code - # - 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") + # the interpreter's symbol table (`lib/temp/lean_symbols.c`, see `stdlib.make.in`) is about 30 MB of static + # data, more than Emscripten's default initial memory of 16 MB + set(EMSCRIPTEN_LINK_SETTINGS "-sALLOW_MEMORY_GROWTH=1 -sINITIAL_MEMORY=64MB") 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) @@ -912,15 +915,21 @@ file(RELATIVE_PATH LIB ${LEAN_SOURCE_DIR} ${CMAKE_BINARY_DIR}/lib) if(CMAKE_SYSTEM_NAME MATCHES "Emscripten") # We do not use dynamic linking via leanshared for Emscripten to keep things - # simple. (And we are not interested in `Lake` anyway.) To use dynamic - # linking, we would probably have to set MAIN_MODULE=2 on `leanshared`, - # SIDE_MODULE=2 on `lean`, and set CMAKE_SHARED_LIBRARY_SUFFIX to ".js". + # simple. (And we are not interested in `Lake` anyway.) `lean.js` is still a main + # module so that the interpreter can look up the runtime's symbols with `dlsym`; the + # compiled Lean code it looks up is in the table that `script/wasm_symbols.py` + # generates (see `stdlib.make.in`), which also writes the list of exported symbols. + # `MAIN_MODULE=2` removes unused code and exports only that list; such a module + # includes only the JavaScript library functions the linked code references, so the + # helpers that the `EM_ASM` blocks in `src/util/shell.cpp` and `src/runtime/io.cpp` + # use are requested explicitly. # 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=2 -sEXPORTED_FUNCTIONS=@${LIB}/temp/lean_exports.json -sEXPORTED_RUNTIME_METHODS=FS,ENV,UTF8ToString,lengthBytesUTF8,stringToUTF8 -sERROR_ON_UNDEFINED_SYMBOLS=0" ) endif() @@ -971,10 +980,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/library/ir_interpreter.cpp b/src/library/ir_interpreter.cpp index c08c4d65800a..241f1af39b8d 100644 --- a/src/library/ir_interpreter.cpp +++ b/src/library/ir_interpreter.cpp @@ -27,6 +27,7 @@ functions, which have a (relatively) homogeneous ABI that we can use without run `call/lookup_symbol` below. */ +#include #include #include #include @@ -339,7 +340,26 @@ void print_value(tout const & ios, value const & v, type t) { return print_value(const_cast(ios), v, t); } +#ifdef LEAN_EMSCRIPTEN +// `lean.js` keeps the interpreter's symbol table inside the module (see `script/wasm_symbols.py`): Emscripten's +// `dlsym` enumerates the export list on every call, and exporting all of Lean costs JavaScript per symbol in every +// pthread. Weak so that other Emscripten programs can link `libleancpp.a` without the table. +extern "C" void * lean_lookup_native_symbol(char const * sym) __attribute__((weak)); +#endif + void * lookup_symbol_in_cur_exe(char const * sym) { +#ifdef LEAN_EMSCRIPTEN + if (lean_lookup_native_symbol) { + if (void * addr = lean_lookup_native_symbol(sym)) { + return addr; + } + // the table holds every symbol of the Lean archives, so a compiled declaration that is not in it is not in + // `lean.js` at all; only the runtime's symbols are left to `dlsym` + if (strncmp(sym, "l_", 2) == 0 || strncmp(sym, "lp_", 3) == 0) { + return nullptr; + } + } +#endif #ifdef LEAN_WINDOWS std::vector hmods(128); DWORD bytes_needed; 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..ed17b3c58f2e 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 @@ -111,6 +120,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}/temp/lean_symbols.stamp: ${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,9 +205,27 @@ $(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`) +WASM_LEAN_ARCHIVES := ${LIB}/lean/libInit.a ${LIB}/lean/libStd.a ${LIB}/lean/libLean.a +WASM_RUNTIME_ARCHIVES := ${LIB}/temp/libleanmain.a ${LIB}/temp/libleanshell.a ${LIB}/lean/libleancpp.a ${LIB}/lean/libleanrt.a +WASM_SYMBOLS_PY := ${LEAN_SOURCE_DIR}/../script/wasm_symbols.py +# the interpreter's symbol table and the export list of `lean.js` (see `script/wasm_symbols.py`); the script rewrites +# its outputs only when their content changes, so a stamp records the run +${LIB}/temp/lean_symbols.stamp: $(WASM_LEAN_ARCHIVES) $(WASM_RUNTIME_ARCHIVES) $(WASM_SYMBOLS_PY) + python3 $(WASM_SYMBOLS_PY) --nm "${CMAKE_NM}" --registry ${LIB}/temp/lean_symbols.c --exports ${LIB}/temp/lean_exports.json --lean $(WASM_LEAN_ARCHIVES) --runtime $(WASM_RUNTIME_ARCHIVES) && touch $@ +${LIB}/temp/lean_symbols.c ${LIB}/temp/lean_exports.json: ${LIB}/temp/lean_symbols.stamp ; +${LIB}/temp/lean_symbols.o: ${LIB}/temp/lean_symbols.c + @echo "[ ] Building $@" + $(LEANC_SH) -c ${LEANC_OPTS} $< -o $@ +WASM_LINK_INPUTS := ${LIB}/temp/lean_symbols.o +$(OUTBIN)/lean$(EXE): $(WASM_LEAN_ARCHIVES) $(WASM_RUNTIME_ARCHIVES) $(WASM_LINK_INPUTS) ${LIB}/temp/lean_exports.json +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 $@ + $(LEANC_SH) ${LIB}/temp/libleanmain.a $(WASM_LINK_INPUTS) ${CMAKE_EXE_LINKER_FLAGS_MAKE} ${CMAKE_DYN_EXE_LINKER_FLAGS_MAKE} ${LEAN_EXE_LINKER_FLAGS} ${LEANC_OPTS} -o $@ lean: $(OUTBIN)/lean$(EXE) 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'")