MULTI_THREAD=OFF build fails: std::adopt_lock_t used in thread.h without including <mutex>

Prerequisites

• Check that your issue is not already filed: searched the tracker for adopt_lock_t
  and for MULTI_THREAD; the only hits are PRs #13233, #2094 and #2091, no issue.
• Reduce the issue to a minimal, self-contained, reproducible test case: this is a
  build-configuration failure in a header, so the reproduction is a cmake invocation
  on a clean checkout with no Mathlib/Batteries involvement. It cannot be reproduced on
  live.lean-lang.org, which does not expose build flags.
• Test against the latest nightly: not done as a build. Stated plainly rather than
  ticked: I verified by reading master's source that <mutex> is still included only
  under LEAN_MULTI_THREAD and that the stub still names std::adopt_lock_t, but I
  have not compiled a nightly with MULTI_THREAD=OFF.

Description

Building with -DMULTI_THREAD=OFF fails to compile. src/runtime/thread.h includes
<mutex> only inside the #if defined(LEAN_MULTI_THREAD) branch, while the
single-threaded stub in the #else branch declares a constructor taking
std::adopt_lock_t, which is defined in <mutex>.

Context

We are building Lean for WebAssembly, where a single-threaded build is required (no
SharedArrayBuffer), so MULTI_THREAD=OFF is not an optional configuration for us but the
one under test. No prior Zulip discussion.

Steps to Reproduce

1. Check out v4.34.0 (293d5d0c0c3f3dded4688b3ccd6a33939ac5102b).
2. Configure:

cmake -S . -B build -G "Unix Makefiles" \
  -DCMAKE_BUILD_TYPE=Release \
  -DCMAKE_C_COMPILER=clang -DCMAKE_CXX_COMPILER=clang++ \
  -DUSE_GMP=OFF -DMMAP=OFF -DMULTI_THREAD=OFF -DUSE_MIMALLOC=OFF

3. cmake --build build --target stage1 -j3

(Our build also passed -DCMAKE_C_FLAGS=-m32 -DCMAKE_CXX_FLAGS=-m32; the failure is in a
header and is not 32-bit specific. USE_GMP=OFF/MMAP=OFF/USE_MIMALLOC=OFF are likewise
incidental -- MULTI_THREAD=OFF alone selects the unguarded code path.)

Expected behavior: the build proceeds, or MULTI_THREAD=OFF is rejected at configure
time if it is no longer a supported configuration.

Actual behavior: compilation fails in src/runtime/thread.h (absolute paths shortened
to repository-relative ones, otherwise verbatim):

In file included from src/util/rc.h:10:
src/runtime/thread.h:184:33: error: no type named 'adopt_lock_t' in namespace 'std'
  184 |     unique_lock(T const &, std::adopt_lock_t) {}
      |                            ~~~~~^
1 error generated.
make[6]: *** [library/constructions/CMakeFiles/constructions.dir/build.make:93:
  library/constructions/CMakeFiles/constructions.dir/init_module.cpp.o] Error 1

Versions

Lean (version 4.34.0, x86_64-unknown-linux-gnu, commit 293d5d0c0c3f3dded4688b3ccd6a33939ac5102b, Release)

Linux 6.18 (Manjaro), clang 22.1.8, cmake 4.4.3, Unix Makefiles generator.

Additional Information

Mechanism, at v4.34.0:

• src/runtime/thread.h:21-23 -- <thread> and <mutex> are included only under
  #if defined(LEAN_MULTI_THREAD).
• src/runtime/thread.h:69-72 -- the #else branch includes only <utility> and
  <cstdlib>.
• src/runtime/thread.h:184 -- the stub unique_lock names std::adopt_lock_t.
• src/CMakeLists.txt:223-227 -- -D LEAN_MULTI_THREAD is appended only when
  MULTI_THREAD is ON, so OFF is exactly the configuration that takes the unguarded path.

The constructor was introduced by PR #13233 ("fix: add missing release() and
adopt_lock_t to single-threaded unique_lock stub", merged 2026-04-07), which added the
declaration without adding the include. Where this still builds, std::adopt_lock_t is
presumably reaching the translation unit transitively via another standard header; it does
not with clang 22 here.

A one-line fix that works for us:

--- a/src/runtime/thread.h
+++ b/src/runtime/thread.h
@@
 // NO MULTI THREADING SUPPORT
 #include <utility>
 #include <cstdlib>
+#include <mutex>   // std::adopt_lock_t, named by the stub unique_lock below
 #define LEAN_THREAD_LOCAL

Defining a local tag type in the stub instead would remove the dependency on <mutex>
altogether, if you prefer the single-threaded branch to stay free of it. I am happy to
open a PR for either shape if that is welcome.

---

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 compile failure is from
a real local build, not a hypothetical, and the cited file/line references, the CMake
mechanism and the origin PR were each checked against the source before filing.

Start with src/runtime/thread.h, especially the single-threaded stub around the std::adopt_lock_t constructor, and inspect src/CMakeLists.txt to confirm how MULTI_THREAD=OFF selects that branch. Reproduce with the provided CMake configuration and build target stage1. Done means the supported OFF configuration either builds successfully or is rejected clearly at configure time.