chore: run more of the test suite on the Web Assembly job

.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/")"

.github/workflows/ci.yml

@@ -273,6 +273,68 @@ jobs:
             const isPr = "${{ github.event_name }}" == "pull_request";
             const isPushToMaster = "${{ github.event_name }}" == "push" && "${{ github.ref_name }}" == "master";
             const chonk = ${{ steps.runner-fallback.outputs.use-runner }};
+            // Tests the Web Assembly job runs (see its `CTEST_OPTIONS` below). A `lean.js` process spends about 10 s
+            // of CPU initializing Lean, so the job cannot afford a whole pile. It runs the `elab` and `elab_fail` tests
+            // that execute code whose behaviour depends on the platform: word size, floating point, byte arrays, bignums
+            // (the wasm build has no GMP), the file system, tasks, hashing and other platform APIs. Those are the files
+            // in tests/elab and tests/elab_fail matched by both of these patterns (the first one is wrapped here)
+            //   grep -lE '\b(USize|ISize|UInt(8|16|32|64)|Int(8|16|32|64)|Float(32|Array)?|ByteArray|toUSize
+            //     |toUInt(8|16|32|64)|IO\.(FS|getEnv|getRandomBytes|asTask|wait|waitAny|mapTask|bindTask|sleep)
+            //     |IO\.(monoMsNow|monoNanosNow|appPath|currentDir)|IO\.Process\.getCurrentDir|readDir|Thunk
+            //     |Task\.(spawn|get|map|bind)|System\.Platform|Std\.Time|ptrAddr\w*|withPtrAddr|unsafeCast
+            //     |isExclusiveUnsafe|dbgTraceIfShared|ptrEq|toUTF8|fromUTF8|utf8ByteSize|hash|mixHash|panic
+            //     |Nat\.(shiftLeft|shiftRight|land|lor|xor|testBit|log2|sqrt))\b|\b[0-9]{10,}\b'
+            //   grep -lE '#eval|#guard\b|native_decide|decide \+native|run_cmd|run_meta|run_elab|run_tac'
+            // except for 15 that cannot work in `lean.js`: `IO_test`, `Process`, `docstringRewrites`,
+            // `getenv_name_with_equals` and `importStructure` spawn processes, `bv_enums` and `rc_model` run CaDiCaL,
+            // `leanExportParse` and `newdo` import LeanExport and Lake, `nat_size_limit` sets `LEAN_NAT_MAX_SIZE` in
+            // its `.init.sh` (environment variables do not reach `lean.js`), `file_not_found` and `handleLocking`
+            // expect Linux behaviour (`EBADF`, `flock`), and `sint_div_overflow`, `float_conversions` and
+            // `interp_prims` expect a 64-bit `ISize` or `USize`.
+            // Plus the `misc` scripts that test the command line (all but `uint64_mul_mod_portable`, which needs
+            // `leanc`) and `markdown_conformance`, a `lean --run` program.
+            const wasmTests = {
+              elab: [
+                "10078", "11773", "11778", "1311", "13921", "13982", "14838", "15994", "1921", "2291", "303", "307",
+                "3546", "4306", "4573", "4677", "5818", "9806", "KyleAlg", "Ord", "Reformat", "Uri", "bigmul",
+                "bitwise", "bool2int", "bytearray", "bytearray_eq", "bytearray_order", "byteslice", "cancel_token",
+                "cleanupAnnotations", "closure_16_unique", "compiler_bug_neutral", "computedFields", "congrThm3",
+                "crashDiv0", "csimpCore", "currentDir", "dateTimeOrd", "dbgMacros", "decideNative",
+                "decideNativePanic", "derivingHashable", "elimDeadBranchesUInt64Literal", "envExtensionNameSearch",
+                "errorExplanationElab", "filePath", "float1", "float32", "floatBits", "floatEquality", "floatFma",
+                "floatMinMax", "float_model_tobits", "floatarray", "getline_crash", "grind_9825", "grind_hom_lemmas",
+                "grind_lia_split_facts", "guard_msgs", "hashMapIteratorLoop", "hashmap", "hlistOverload", "idbg_e2e",
+                "inlineWithNestedRecIssue", "instantiateMVarsCrossScope", "instantiateMVarsSharing", "intModBug",
+                "intNegSucc", "int_to_nat_bug", "ioNulBytes", "ioRandomBytes", "json", "json2", "kernel2",
+                "kernelInterrupt", "kernelProjIdx", "kernel_is_def_eq_equiv_manager_1",
+                "kernel_is_def_eq_equiv_manager_2", "lcnfInferProjTypeIssue", "lean_nat_gcd", "lean_nat_powmod",
+                "library_suggestions_shared_cache", "libuv", "lit_value_classify", "lit_values", "lrat_roundtrip",
+                "markdown_case_folding", "markdown_character_classes", "match_float", "meta6", "name_eq_bug",
+                "ofIntClamp", "openssl", "optionGetD", "patbug", "postprocess_traces", "ptrAddr",
+                "pullInstancesDecidable", "rangePolymorphic", "rangeSyntaxPrecedence", "ranges_infer", "readDir",
+                "realPath", "reduce1", "reduce3", "runtime_bignum_edge_cases", "sarray", "sharecommon",
+                "sharecommon_mpz", "sint-abs", "sint_basic", "sint_conversions", "st_test", "stdio", "string",
+                "string_cases", "string_fromUTF8Lossy", "string_slice", "sym_arith_classify", "sym_arith_ground",
+                "sym_arith_norm", "taskState", "task_iterators", "task_test", "task_test2", "task_test_io",
+                "tc_cache_check_hits", "tc_cache_check_hits_stale", "tempfile", "thunk", "thunkHeartbeats",
+                "thunkTaskCasesOn", "timeAPI", "timeCanonFormats", "timeClassOperations", "timeFormatRoundTrip",
+                "timeFormats", "timeHttpDate", "timeLimits", "timeLocalDateTime", "timeNegative", "timeOperations",
+                "timeOperationsOffset", "timeParse", "timePosixTzFooter", "timeSet", "timeSub", "timeTzifParse",
+                "timeUnitScalar", "toExpr", "trivial_uint", "try_panic", "ugetBorrowed", "uint64_modular",
+                "uintCtors", "uintMatch", "uint_sint_decidable_quantifiers", "unifHintAndTC", "unsafeTerm",
+                "updateExprIssue", "updateLevelIssues", "utf8英語", "versoDocBlockquoteErrors", "versoDocModuleScoped",
+                "versoDocRegionReprint", "withSetOptionIn",
+              ],
+              elab_fail: [
+                "1825", "277a", "277b", "phashmap_inst_coherence",
+              ],
+              misc: [
+                "lean_ghash", "lean_help", "lean_unknown_file", "lean_unknown_option", "lean_version",
+              ],
+            };
+            const wasmTestsRegex = "^(" +
+              ["elab", "elab_fail"].map((p) => p + "/(" + wasmTests[p].join("|") + ")\\.lean").join("|") +
+              "|misc/(" + wasmTests.misc.join("|") + ")\\.sh|markdown_conformance)$";
             let matrix = [
               /* TODO: to be updated to new LLVM
               {
@@ -426,20 +488,31 @@ 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}",
+                // `wasmTests` (above), with the step's `-j$NPROC`: a `lean.js` process needs up to about 3 GB (a 2 GB wasm
+                // heap plus V8), so the 15 GiB of the 4-core `ubuntu-24.04` runner hold four. Every failed test is rerun once
+                // (`until-pass` retries any failure; a rerun that passes shows only in the step's log) because of two rare
+                // failures of `lean.js` itself: a hang under load, which `--timeout` turns into a failure, and a trap at
+                // exit, after the complete output, of a `lean --run` process.
+                "CTEST_OPTIONS": "--no-tests=error --timeout 300 --repeat until-pass:2 -R '" + wasmTestsRegex + "'"
+              }
             ];
             // Stage that is built, tested and packed. Shipped (stamped) release builds use stage2.
             for (const job of matrix) {

doc/make/emscripten.md

@@ -1,12 +1,36 @@
-# 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 . <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.
+
+## 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 `lean.js` process spends about 10 s of CPU initializing Lean (V8 compiles the module lazily, so the time is Lean's own) and needs between one and three gigabytes of memory, so the whole `elab` pile would take hours. CI runs 177 tests in parallel. They are listed as `wasmTests` in the matrix script of `ci.yml`, next to the two `grep` patterns that select them: the `elab` and `elab_fail` tests that execute code whose behaviour depends on the platform (word size, floating point, byte arrays, bignums, the file system, tasks, hashing, platform APIs), without those that cannot work in `lean.js`, plus the `misc` scripts that test the command line and `markdown_conformance`. Tests that spawn processes (`bv_decide` runs CaDiCaL), import Lake or LeanExport, rely on environment variables from their `.init.sh`, on Linux-only behaviour or on a 64-bit word size cannot work in `lean.js`; `importModules` of `Lean` on top of `import Lean` exhausts the 2 GB wasm32 heap, and deep recursion overflows the 4 MB stack of a Node.js worker thread with a JavaScript `RangeError`. The other piles need `leanc`, Lake, the libuv bindings that the wasm build stubs out, or a `lean --server` child process.
+
+To run the job's tests locally, take the `ctest` command from the Test step of a `Web Assembly` job log and run it from the repository root, or pass your own `-R` to `ctest --preset release --test-dir build/stage1`. `lean` starts one Node.js worker thread per task-manager thread, so pass `-j4` (or the test suite's `TEST_LEAN_ARGS=-j4`) on machines with many cores. Two rare failures come from `lean.js` itself and are retried by the job: a hang under load, and a trap at exit after the complete output of a `lean --run` process.

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
 --------------------------