[basvandijk]

This PR makes the Web Assembly CI job run 177 tests instead of six, in parallel instead of one at a time.

The job 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. Two grep patterns in ci.yml select them, less 15 tests that cannot work in lean.js because they spawn processes, run CaDiCaL, import Lake or LeanExport, set environment variables in their .init.sh, or expect Linux behaviour or a 64-bit word size. The misc scripts that test the command line and markdown_conformance, a lean --run program, complete the list. It is kept as wasmTests in ci.yml, from which the matrix entry builds the -R argument of ctest. A lean.js process spends about 10 s of CPU initializing Lean, so the whole elab pile would take hours; with the step's default -j$NPROC this selection takes 8 to 10 minutes, depending on the runner's speed. Every failed test is rerun once (--repeat until-pass:2, with --timeout 300) because of two rare failures of lean.js itself: a hang under load, about one in 1,300 test runs on four CPUs, and a trap at exit after the complete output of a lean --run process, a few percent of its runs. doc/make/emscripten.md describes the selection.

This PR is stacked on #16149 and carries its commits until that PR merges; it will be rebased onto master afterwards. Until then, the diff of this PR alone is basvandijk:wasm-symbols...basvandijk:wasm-tests.

Claude Code, an AI coding assistant, helped with the investigation, the changes, the testing and this description. I reviewed and checked them.

🤖 Generated with Claude Code

[basvandijk]

How this was tested:

• The Web Assembly job runs only at check level 2 or higher, so the CI evidence is a run of the job on this branch's current head, on my fork: https://github.com/basvandijk/lean4/actions/runs/41464801005 (emsdk 6.0.13, Node.js 26.13.0, a 4-CPU ubuntu-24.04 runner). All 177 tests passed, no retries, ctest in 10 min 3 s (2 to 34 s per test, median 12 s), the Test step in 10.1 min and the whole job in 60 min with warm caches (Build Target Stage 37.4 min, Pack 9 min); the build prints the same warnings as perf: resolve native symbols inside lean.wasm instead of exporting all of Lean #16149's trial run, https://github.com/basvandijk/lean4/actions/runs/41286288809.
• An earlier run, from before this branch was rebased onto a master that brought four more tests into the selection, passed the 173 tests then selected in 7 min 51 s of ctest (https://github.com/basvandijk/lean4/actions/runs/41344542135, job 48 min). Apart from those four tests, the difference is the runner, not the code: in the later run the 173 tests took 25 % longer, in total and test by test (median ratio 1.25), and so did the build's compilation of the same 1,139 sources of Emscripten's libc (8.97 s instead of 7.19 s), while in the local 4-CPU container below the same 173 tests took 1 % longer after the rebase.
• Local builds in a Docker container mirroring the runner (ubuntu:24.04, clang 18.1.3, cmake 3.31.6, emsdk 6.0.13, Node.js 26.13.0) with the job's CMAKE_OPTIONS plus -DLEAN_EXTRA_OPTS=-j4, on a 64-thread AMD EPYC 7302 host. To find out what works in lean.js at all, every pile that needs only lean (elab, elab_fail, elab_bench, docparse, misc, markdown_conformance, doc/examples) ran once with ctest -j16: 4,195 tests, 88 failures, 1 h 04 min. 62 of the 77 failures in the piles that are relevant here (elab, elab_fail, docparse, misc, markdown_conformance) were read and sorted: 44 bv_decide tests fail with "unsupported operation (error code: 52, function not implemented)" when the tactic spawns cadical; six tests spawn processes (importStructure does so through findSysroot); newdo imports Lake and leanExportParse imports LeanExport, which the wasm build does not have; nat_size_limit reads LEAN_NAT_MAX_SIZE from its .init.sh, and lean_main copies only LEAN_PATH into Emscripten's environment; file_not_found expects EBADF where Emscripten reports EACCES, handleLocking expects exclusive flocks that Emscripten's libc does not implement, sint_div_overflow and float_conversions assume a 64-bit ISize; instances cannot importModules Lean on top of import Lean (a standalone run traps at 3.2 GB of RSS, past the 2 GB wasm32 heap); grind_11081, grind_nestedDecidable_kernel_issue and issue9018 end with "RangeError: Maximum call stack size exceeded" in a Node.js worker thread, whose stack is 4 MB (node --stack-size=8192 covers only the main thread, and Lean's own stack check assumes the 8 MB it asked for); misc/uint64_mul_mod_portable.sh needs leanc. The other 26 failures: 13 docparse traps (below), two timeouts without output (csimpAttrFn, specInvariantAttr, which pass alone in 12 s and 7 s), and 11 elab_bench and doc/examples tests outside the selection.
• A second run of these piles without those 77 failures (ctest -j16, 4,026 tests) failed only 13 docparse tests, each with "memory access out of bounds" after its complete expected output.
• A third run in a container limited like the runner (docker run --cpus=4 --memory=15g --memory-swap=18g, a cgroup quota of four CPUs rather than four dedicated cores; ctest -j4; every lean given -j4 as the runner's four hardware threads would; CTest's default 1500 s timeout) of the 4,041 tests that can work: 18 failures, that is 15 docparse traps at exit (4.5 % of the pile's lean --run processes) and three tests that hung without output until the timeout (9366, 15605, grind_canon_bug_2; 7 to 15 s normally, and they pass in the first two runs), 5 h 58 min, peak memory of the container's cgroup 8.9 GiB, no OOM kill. This run gives the per-test costs behind the selection: a lean.js process elaborating a file needs 9 to 10 s of CPU at least (lean --version needs 3 s), the median test 16 s, so the elab pile alone costs more than four hours of wall time on four such cores; Node.js 26 already compiles the module lazily, and --wasm-lazy-compilation, --no-wasm-tier-up and --liftoff-only change nothing. Over the nine ctest runs of this branch reported here, 6 of 13,352 test runs hung, in 5 tests (15605 twice, both times under the 4-CPU quota, while it passed 8 times in a row under a synthetic four-way load and in both 64-CPU runs): 4 of the 5,131 test runs on four CPUs (under this quota and in the two CI runs, which had none) and 2 of the 8,221 on 64 CPUs, hence the retry.
• The selection itself, in the same container with the job's exact options (--timeout 300 --repeat until-pass:2, the generated -R), twice, the second time on the current head: 177 tests, all passed, no retries, 15 min 17 s and 15 min 20 s of wall time for 3,643 s and 3,655 s of CPU (CPU-bound on the four-CPU quota; per elab or elab_fail test 9 to 57 s of CPU, median 19 s), peak memory 9.3 and 9.1 GiB. Before the rebase, the 173 tests then selected passed in the same way in 14 min 46 s. An earlier 212-test variant of the list, before the criterion required the tests to execute code, also passed in 17 min 41 s, with one test (15605, no longer selected) killed at 300 s and passing on its retry.
• The -R argument was checked rather than trusted: wasmTests evaluated as the matrix script does yields a regex that matches exactly the 177 intended names and nothing else among the 4,780 registered tests, ctest -N -R on the wasm build selects 177, and the two grep patterns in the ci.yml comment select 186 files, which minus the 15 named exceptions are the 171 elab and elab_fail names (--no-tests=error would only catch an empty selection, and a mistyped name matches nothing). The names contain no regex metacharacters.
• Controls: tempfile and libuv, two of the six tests the job ran before, are in the list and pass in every run (positive); 14 of the 15 exceptions failed for the stated reasons in the one run that included them, elab/Process.lean with the unsupported-operation error, and interp_prims, new on master since that run, fails because its expected output has 64-bit USize values where lean.js prints the correct 32-bit ones (4294967293 for (-1 : USize) - 2) (negative); ctest --repeat until-pass:2 --timeout 3 reruns a test that timed out (checked with a toy project under cmake 3.31.6).
• Not tested: a wasm build with -sMAXIMUM_MEMORY=4GB; the docparse pile in the job (left out: 44 s of CPU per test and the exit trap); the --run piles that spawn processes (server, server_interactive) and the compile piles, which need leanc.

[basvandijk]

changelog-no