Emscripten build passes `-pthread` unconditionally, ignoring `MULTI_THREAD=OFF`

[zommuter]

Summary

The Emscripten branch of src/CMakeLists.txt adds -pthread unconditionally, with no reference to the MULTI_THREAD option. A WebAssembly build therefore always links a shared-memory artifact, which requires SharedArrayBuffer and so requires the embedding page to be cross-origin isolated (COOP/COEP). -DMULTI_THREAD=OFF does not change this.

The rest of the file already gates -pthread on the option, so this looks like an oversight in one branch rather than a deliberate choice.

Where

On master (41aa79c394d9d615f61cadcf4b3b053a4f016d6d), src/CMakeLists.txt:175-176, inside the if(EMSCRIPTEN) branch:

set(EMSCRIPTEN_SETTINGS "-s ALLOW_MEMORY_GROWTH=1 -fwasm-exceptions -pthread -flto")
string(APPEND LEANC_EXTRA_CC_FLAGS " -pthread")

EMSCRIPTEN_SETTINGS is then appended to LEAN_EXTRA_CXX_FLAGS, LEAN_EXTRA_LINKER_FLAGS and LIBUV_EMSCRIPTEN_FLAGS, so -pthread reaches compile, link and the vendored libuv.

Compare line 666, which is the pattern I would have expected the branch above to follow:

if(MULTI_THREAD AND NOT MSVC AND NOT CMAKE_SYSTEM_NAME MATCHES "Darwin")
  string(APPEND LEAN_EXTRA_LINKER_FLAGS " -pthread")
endif()

MULTI_THREAD=OFF reaches only the -D LEAN_MULTI_THREAD define at lines 224-228. Same on v4.34.0 (293d5d0c0c3f3dded4688b3ccd6a33939ac5102b), at lines 180-181.

Why this is awkward downstream

There is no supported way to negate -pthread on the consumer side. -no-pthread is not a recognised emcc flag, -sSHARED_MEMORY=0 has no effect, and -sPTHREADS=0 is rejected as an internal setting. The only mechanism that works is -sUSE_PTHREADS=0, which is deprecated in favour of -pthread and is a hard error under STRICT.

I raised that with Emscripten as emscripten-core/emscripten#27723. Their maintainer's response was reasonably that the build system passing -pthread unconditionally is the better place to fix it, which is why I am filing here. They have offered to keep -sUSE_PTHREADS=0 working as a negation-only setting, so this is not urgent for me, but it leaves Lean's wasm output unable to express a non-shared-memory build through its own options.

Suggested fix

Gate the Emscripten -pthread on MULTI_THREAD, the way line 666 already does, so that -DMULTI_THREAD=OFF produces a non-shared-memory wasm artifact.

What I have and have not tested

I have built Lean for wasm at v4.34.0 with emsdk 6.0.9 and MULTI_THREAD=OFF (which additionally needs #15172 and the two fixes in #14973 / PR #14974), and produced a working non-shared-memory bundle. But I got there by forcing -sUSE_PTHREADS=0 at the link step only: the intermediate objects were still compiled with -pthread and are byte-identical to the threaded build's. That bundle runs its 27 runtime checks correctly under Node.

So I can say a link-time negation yields a working artifact. I have not built with the CMake gate applied, and I cannot tell you whether a consistently pthread-free compile of the runtime works, or whether anything else in the tree assumes threads under Emscripten. Treat the report as "this option is silently ignored in one branch", not as "the gated build is known good".

Happy to open a PR for the gating and test it against my build if that would be useful.

---

Disclosure, per CONTRIBUTING.md's AI Contributions section: this report was researched and drafted by Claude Opus 5 (Claude Code) working at my direction. The line numbers and the master check are from real source reads, and the build and flag results from real local runs, not hypotheticals.

[zommuter]

Status update so the offer above doesn't read as abandoned.

Gating -pthread properly means compiling the runtime pthread-free, which I have not done. Everything I have measured so far negates at the final link only -- my -sUSE_PTHREADS=0 variant's stage1 archives are byte-identical to the pthread build's, so the runtime objects are still compiled with -pthread. I would rather not send a PR that just moves a link flag and calls it gating.

Happy to do the real thing if a maintainer signals the gating is wanted. Holding until then.

(Drafted with AI assistance, reviewed by me.)