From db1e2ac34ce5cfb23c736c30a3c44b613d7cacf8 Mon Sep 17 00:00:00 2001
From: Keith Seim <keith@firestitch.com>
Date: Tue, 7 Apr 2026 05:30:13 -0400
Subject: [PATCH] fix: add missing release() and adopt_lock_t to
 single-threaded unique_lock stub (#13233)
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

This PR fixes runtime build issues when `LEAN_MULTI_THREAD` is not set.

## Problem

When building with `LEAN_MULTI_THREAD` undefined (required for
Emscripten/WASM targets), the stub `unique_lock<T>` in
`src/runtime/thread.h` is missing two members that the real
`std::unique_lock` provides:

1. **`release()`** — called by runtime code paths, causes a compile
error when the stub is active
2. **`unique_lock(T const &, std::adopt_lock_t)`** — required by code
that acquires a lock before constructing the `unique_lock`

The other stubs in this file (`mutex`, `lock_guard`,
`condition_variable`) are complete; only `unique_lock` is missing API
surface.

## Fix

Add the two missing members to the single-threaded `unique_lock` stub:

```cpp
unique_lock(T const &, std::adopt_lock_t) {}
T * release() { return nullptr; }
```

Both are no-ops, matching the semantics of a single-threaded
environment. `release()` returns `nullptr` (no mutex to release). The
`adopt_lock_t` constructor is a no-op (no lock to adopt).

## Evidence

I've been using this fix in a production project
([specify-lean](https://github.com/kjsdesigns/specify)) since v4.27.0 to
build the Lean4 runtime to WASM via Emscripten. The fix has been stable
across multiple Lean version bumps.

I posted about this on
[Zulip](https://leanprover.zulipchat.com/#narrow/channel/270676-lean4/topic/WASM.20build.20fixes.3A.20libuv.20symbol.20leakage.20.28.236817.29.20and.20unique_lo/with/580836892)
on 2026-03-21.

Co-authored-by: Keith Seim <keith@MacBook-Pro.local>
---
 src/runtime/thread.h | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/src/runtime/thread.h b/src/runtime/thread.h
index 69140ef167..57a3729c7c 100644
--- a/src/runtime/thread.h
+++ b/src/runtime/thread.h
@@ -181,9 +181,11 @@ public:
 template<typename T> class unique_lock {
 public:
     unique_lock(T const &) {}
+    unique_lock(T const &, std::adopt_lock_t) {}
     ~unique_lock() {}
     void lock() {}
     void unlock() {}
+    T * release() { return nullptr; }
 };
 inline unsigned hardware_concurrency() { return 1; }
 }