[basvandijk]

This PR updates the Web Assembly CI job from Emscripten 3.1.44, released in July 2023, to 6.0.13, the current release, so that the WebAssembly build of lean is checked against a maintained toolchain.

Three changes in newer Emscripten versions affect lean.js. emcc links the C++ runtime only when asked to since 6.0.6 and has always ignored -lstdc++, so on Emscripten the C++ standard library flag is now -sDEFAULT_TO_CXX=1; without it lean.js links but fails to start, with 109 unresolved C++ runtime imports. -shared builds a real side module since 6.0 instead of an object file, so lean.js now depends on the static archives it links instead of on the dummy libInit_shared.so, libleanshared_1.so, libleanshared_2.so and libleanshared.so, whose recipes no longer run; as the dummies are touched on every build, this also stops make install from relinking lean.js, which took nine minutes of the job. Since 4.0.11 Emscripten's compiler-rt bundles LLVM's profiling runtime, which a main module links whole, so every lean.js run wrote a default.profraw into its working directory (emscripten-core/emscripten#28123); lean_main now points that runtime at /dev/null.

The Emscripten -s settings are now passed only when linking, which removes the 147 linker setting ignored during compilation warnings, use the -sKEY=VALUE spelling, and no longer include LINKABLE, which MAIN_MODULE=1 implies and Emscripten deprecated in 4.0.15.

doc/make/emscripten.md, which still described the Lean 3 lean_js_js and lean_js_wasm targets, now describes the WebAssembly build as the CI job runs it and is linked from doc/make/index.md.

This PR is stacked on #16135 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-ci...basvandijk:wasm-emsdk-6.

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 (nightlies, release-ci), so the CI evidence is a run of this branch's job on my fork: https://github.com/basvandijk/lean4/actions/runs/41233382394 (emsdk 6.0.13 installed cold, Node.js 26.13.0, stage-0 ccache warm, stage-1 ccache cold): green in 1 h 5 min; Setup emsdk 45 s, Build Target Stage 40.1 min, Install 7 s (9.3 min before: lean.js is no longer relinked at install), Pack 8.4 min, Test 13.3 min, 6/6 tests, source tree clean. Warnings: 0 linker setting ignored during compilation (147 before), 0 -shared emulation warnings (4 before), 0 LINKABLE warnings, 1 dynamic linking + pthreads is experimental (2 before, one per link), the same 14 undefined symbols as before, once each (libuv internals, lean_uv_*, dl_iterate_phdr). Baselines on 3.1.44: run 41141309853 (warm caches: Build Target Stage 32.5 min, Install 9.3 min, Test 10.9 min, 1 h 1 min) and 41127897324 (cold: 54.3 min, 13.9 min, 13.4 min, 1 h 53 min). The run tested f662d3b, which differs from this branch only by the issue reference added to one comment afterwards.
• Local build in a Docker container mirroring the runner (ubuntu:24.04, clang 18.1.3, cmake 3.31.6, i386 multilib, emsdk 6.0.13, Node.js 26.13.0) with the job's CMAKE_OPTIONS, the Install, Pack and Test steps and the six tests; lean --version, lean --run, lean --print-prefix (which now works; on 3.1.44 it crashed because __filename was undefined on the worker thread), exit codes of IO.Process.exit 3 and of a failing file, a kernel exception, IO.asTask, IO.getEnv via LEAN_PATH. lean.wasm: 247,834 exports (3.1.44: 251,027; the V8 limit is 1,000,000), 410 imports, 0 C++ runtime imports, the same 14 undefined imports as before. Peak RSS: 3.1 GB for the largest process of the lean.js link, 5.2 GB for elab/Format.lean with 4 threads (3.1.44: 10.7 GB).
• Controls. Without -sDEFAULT_TO_CXX=1 on emsdk 6.0.13, lean.js links but lean --version prints nothing and fails in Emscripten's dynamic loader with TypeError: Cannot read properties of undefined (reading 'value') at reportUndefinedSymbols; lean.wasm imports 109 C++ runtime symbols (std::__2::cout, std::__2::cerr, the basic_streambuf and basic_stringbuf vtables, typeinfo for std::bad_alloc, ...) versus 0 with the flag. The old shared-library recipes, run by name on 6.0.13, build real side modules: libInit_shared.so becomes a 238-byte module with a dylink section, and the libleanshared.so recipe is a 76-second, 3.2 GB side-module LTO link of all of Lean producing an unused 140 MB file (0.1 s of emulation on 3.1.44); with the change neither runs and make install no longer relinks lean.js. Reverting the warning-cleanup commit and rebuilding brings the 147 compile-time warnings and the LINKABLE deprecation warning back; lean.js is byte-identical and lean.wasm has the same size, sections, imports, exports (247,834) and memory limits with and without it; the only difference inside lean.wasm is the respelled flag string that Lean.Compiler.FFI.getLinkerFlags embeds (src/util/ffi.cpp), which shifts later data addresses by two bytes. Without the default.profraw guard, every lean.js run on 6.0.13 left a 128-640 byte default.profraw in its working directory and the test step failed the source-tree check; with it, none (the file is LLVM's raw profile, written by compiler-rt's profiling runtime that Emscripten bundles into libclang_rt.builtins since 4.0.11 and that MAIN_MODULE=1 links whole; a two-line C program linked with -sMAIN_MODULE=1 reproduces it, see MAIN_MODULE programs write default.profraw at exit (profile runtime force-linked from libclang_rt.builtins) emscripten-core/emscripten#28123). The commits before the version bump were also built with emsdk 3.1.44 in the same harness: green, 6/6 tests, source tree clean, no -shared and no linker setting ignored warnings, one lean.js link per build and install.
• Not tested: browser embedding (not a CI target); Emscripten versions between 3.1.44 and 6.0.13.

[basvandijk]

changelog-no