Skip to content

fix: add missing release() and adopt_lock_t to single-threaded unique_lock stub#13233

Merged
hargoniX merged 1 commit intoleanprover:masterfrom
kjsdesigns:fix-wasm-unique-lock-stub
Apr 7, 2026
Merged

fix: add missing release() and adopt_lock_t to single-threaded unique_lock stub#13233
hargoniX merged 1 commit intoleanprover:masterfrom
kjsdesigns:fix-wasm-unique-lock-stub

Conversation

@kjsdesigns
Copy link
Copy Markdown
Contributor

@kjsdesigns kjsdesigns commented Apr 1, 2026

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:

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) 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 on 2026-03-21.

…_lock stub

When building with LEAN_MULTI_THREAD undefined (required for Emscripten/
WASM targets), the stub unique_lock<T> in thread.h is missing:

- release() — called by runtime code, causes compile error
- unique_lock(T const &, std::adopt_lock_t) — required by code that
  acquires a lock before constructing the unique_lock

The real std::unique_lock provides both. The stub should too.

Discovered while building Lean4 to WASM via Emscripten for a production
project (specify-lean) since v4.27.0. The fix has been proven stable
across multiple Lean version bumps.
@github-actions github-actions bot added the toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN label Apr 1, 2026
@mathlib-lean-pr-testing
Copy link
Copy Markdown

Mathlib CI status (docs):

  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 8b52f4e8f701a9b56a76e6e0e118ef587621c3e0 --onto fc0cf68539ad3b481a1802414c22c44506519c9d. You can force Mathlib CI using the force-mathlib-ci label. (2026-04-01 15:40:52)

@leanprover-bot
Copy link
Copy Markdown
Collaborator

Reference manual CI status:

  • ❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase 8b52f4e8f701a9b56a76e6e0e118ef587621c3e0 --onto cfa8c5a036d6990635c6ec50b02d0e806995cec3. You can force reference manual CI using the force-manual-ci label. (2026-04-01 15:40:54)

@hargoniX hargoniX added the changelog-compiler Compiler, runtime, and FFI label Apr 7, 2026
@hargoniX hargoniX added this pull request to the merge queue Apr 7, 2026
Merged via the queue into leanprover:master with commit db1e2ac Apr 7, 2026
25 of 28 checks passed
wkrozowski pushed a commit to wkrozowski/lean4 that referenced this pull request Apr 10, 2026
…_lock stub (leanprover#13233)

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>
volodeyka pushed a commit that referenced this pull request Apr 16, 2026
…_lock stub (#13233)

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>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

changelog-compiler Compiler, runtime, and FFI toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN

Projects

None yet

Development

Successfully merging this pull request may close these issues.

3 participants