[basvandijk]

This PR re-enables the Web Assembly CI job as a secondary, test-only job for nightlies, releases and PRs with the release-ci label, so that breakage of the WebAssembly build is caught again.

#6424 disabled the job because V8 rejected lean.wasm, which exports every symbol, once it had more than 100,000 exports. Node.js has accepted up to 1,000,000 since version 24, and lean.wasm has 251,027 today, so the job now runs its tests with Node.js 26. It runs six tests, one at a time, as a WebAssembly lean process can need 10 GiB of memory. It does not ship a linux_wasm32 archive, does not gate merges, nightlies or releases, and is skipped when the target stage is 2, which the cross-compiled stage 1 cannot build. Its native 32-bit stage 0 now finds libuv through the i386 pkg-config, does floating-point arithmetic with SSE as lean.h requires, and uses 32 MiB thread stacks instead of the native default of 1 GiB, of which a 32-bit address space holds only a few. Linux jobs without Nix, which provides gdb, now skip the step that prints backtraces of core dumps.

This PR also fixes the WebAssembly build itself:

• IO.FS.renameIfNew compiles for Emscripten, which has no renameat2: it checks that the target does not exist and then renames, which, unlike on other platforms, is not atomic.
• The lean launcher for lean.js is generated again, now locating lean.js relative to itself and passing its arguments quoted.
• Lake archives the WebAssembly libraries with emar, as GNU ar writes no symbol index for them, and builds only Init, Std and Lean, which are what lean.js links. Before, it also tried to build Leanc, whose Leanc.lean is not generated for Emscripten, and failed.
• Header snapshots for the elab tests (LEAN_HEADER_SNAPSHOTS, which CI turns on) are turned off on Emscripten, as saving one needs dl_iterate_phdr, which Emscripten does not have.
• emcc's JavaScript passes get a heap limit of 8 GiB: with Node.js's default of about 4 GiB, they ran out of memory on the 145 MiB lean.js.
• lean.js is linked only after the shell library, which it links directly, is rebuilt; before, an incremental build could link the old one.

Stacked follow ups:

• chore: update the Web Assembly CI job to Emscripten 6.0.13 #16142.
• perf: resolve native symbols inside lean.wasm instead of exporting all of Lean #16149.

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

Closes #16134

🤖 Generated with Claude Code

[basvandijk]

How this was tested:

Hosted runs. On my fork, a throwaway branch ran only this job, through this branch's build-template.yml, unmodified, with the matrix entry that a nightly run of this branch's ci.yml produces, on standard ubuntu-24.04 runners (4 CPUs, 15 GiB of memory, 3 GiB of swap):

Step	Run 1: empty caches	Run 2: caches of run 1
Setup emsdk	51 s	5 s
Build Stage 0 & Configure Stage 1	20 min	33 s
Build Target Stage	54 min	32 min
Install	14 min	9 min
Pack	9 min	6 min
Test	13 min: 6 of 6 passed, 124–138 s each	11 min: 6 of 6 passed, 104–114 s each
Whole job	1 h 53 min	1 h 1 min

Run 2 used 8e0b12d, the current head of this branch. Run 1 used af58d75, an earlier revision without three later changes: the dependency of lean.js on the shell library, renameIfNew reporting a missing source even when the target exists (as renameat2 does), and the condition on the "Show stacktrace for coredumps" step. In neither run did wasm-ld report a function signature mismatch when linking lean.js.

Local replay. I also generated the job's steps from build-template.yml and ran them from a clean clone in a 4-vCPU Ubuntu 24.04 VM, with the runner's 15 GiB of memory but 4 GiB of swap instead of 3 GiB, that mirrors what the job uses from the runner image (clang 18, CMake 3.31.6, Node.js 22 as the default node, Node.js 26 from setup-node, emsdk 3.1.44 as setup-emsdk installs it). The first replay, with empty caches, used run 1's source with two tests at a time; its Test step peaked at 14.7 GiB of memory plus 3.6 GiB of swap, more swap than the runner has. The second, on a fresh VM with the caches of the first, used the revision of run 1, with one test at a time, and peaked at 10.2 GiB without swap. Both were green, including "Check Source Tree Clean". The job used up to 11 GiB of disk, and the 32-bit stage 0 processes stayed below 1.7 GiB of their 4 GiB address space.

Controls, on local builds of earlier revisions of this branch, and of this branch for the last one:

• With fix: match the parameters of eight FFI definitions to the generated C #16090 reverted, wasm-ld reports a function signature mismatch for each of its eight functions, lean --version fails with RuntimeError: unreachable, and all six tests fail. With only its two temp-file functions reverted, there are two warnings, and only elab/tempfile.lean fails.
• One changed line in tests/elab_fail/1007.lean.out.expected makes the Test step fail, and test-results.xml lists the six tests with one failure.
• With only the workflow changes on master, the Build Target Stage step fails: em++ cannot find linux/fs.h for src/runtime/io.cpp, and Lake fails to build Leanc, whose Leanc.lean is not generated for Emscripten.
• Node.js 22, the runner's default, rejects today's lean.wasm with exports count of 251027 exceeds internal limit of 100000.
• The job's CTEST_OPTIONS select exactly the six tests. With the old regex, which matches no test today, --no-tests=error fails the step.
• In the 32-bit stage 0, eight concurrent dedicated tasks all finish with the job's 32 MiB thread stacks, but with LEAN_STACK_SIZE_KB=1048576, the native default of 1 GiB, lean aborts with failed to create thread: Resource temporarily unavailable. Without -msse2 -mfpmath=sse, clang -m32 stops at lean.h's FLT_EVAL_METHOD check.
• IO.FS.renameIfNew gives the same results on WebAssembly as in the native i386 stage 0, which uses Linux's renameat2, when renaming an existing file to a new path, to another existing file, to itself and to a directory, and when renaming a missing file to a new path and to an existing file.
• Before lean.js depended on the shell library, a rebuild after a change to src/util/shell.cpp linked lean.js before archiving the new libleanshell.a, and the rebuilt lean still ran the old code. With the dependency, four rebuilds that applied or reverted a fix for lean --version, --run and other options exit with a garbage code on 32-bit targets #16136 each picked up the change: lean --version exited with 0 after applying it and with 178 after reverting it. Two of them used the fix in fix: return the right exit code from lean on 32-bit targets #16137, and two an earlier one-line version of it.

Not addressed here:

• Each test takes about 2 minutes, almost all of it to start lean: locally, lean on an empty file takes as long as a test, and 81% of the time of the thread that runs Lean goes to Emscripten's dlsym, which looks up each symbol with Object.keys(lib.exports).indexOf(symbol), linear in the 251,027 exports. Current Emscripten still does this.
• Each Emscripten pthread is a Node.js worker that loads the 145 MiB lean.js again. A lean process grows to about 4.7 GiB before Lean's task manager starts its threads; elab/Format.lean then peaks at 10.2 GiB, or at 5.7 GiB with --threads=1.
• lean -o fails on WebAssembly: saving a compacted region calls dl_iterate_phdr, which Emscripten lacks, and the JavaScript stub that the lean.js link generates for the undefined symbol calls itself until the stack overflows (Maximum call stack size exceeded). Header snapshots, which this PR turns off for Emscripten, are the same case.
• On 32-bit targets, lean exits with a code derived from a heap address after options such as --version and after --run: lean --version, --run and other options exit with a garbage code on 32-bit targets #16136, fixed by fix: return the right exit code from lean on 32-bit targets #16137.
• lean --print-prefix and --print-libdir fail on WebAssembly with ReferenceError: __filename is not defined: IO.appPath reads Node.js's __filename in JavaScript that runs on the calling thread, and the shell runs on an Emscripten pthread, a Node.js worker, where it is not defined.
• The lean.js link accepts undefined symbols (-s ERROR_ON_UNDEFINED_SYMBOLS=0), so a runtime function without an Emscripten definition fails only when it is called. Today 14 are undefined: eight libuv internals, dl_iterate_phdr and five TCP and UDP functions whose Emscripten stubs are missing; those take a socket, which the Emscripten build cannot create.
• emcc 3.1.44 does not support --print-target-triple, so System.Platform.target is empty in the WebAssembly build.
• emsdk 3.1.44 dates from 2023. Since Emscripten 6.0.0, -shared builds side modules, so with a current emsdk the rules in stdlib.make.in that build libInit_shared.so and libleanshared*.so would no longer produce plain objects unless the build passes -s FAKE_DYLIBS=1 or those rules change. I have not tried a current emsdk.
• The Emscripten dummy targets Init_shared and leanshared in src/CMakeLists.txt touch libInit_shared.so and libleanshared*.so on every build, and lean.js depends on those files in stdlib.make.in, so the Install step links lean.js again.
• On nightlies, the Pack step spends 6 to 9 minutes compressing archives that this job does not upload.

This PR is stacked on #16090 and contains its commit until that PR is merged.