This PR moves `IO.CancelToken` from `Init.System.IO` to its own file
`Init.System.CancelToken`, backed by `IO.Promise Unit` instead of
`IO.Ref Bool`. This enables non-polling cancellation propagation: the
token's underlying promise can be used directly with `IO.waitAny`, and
callbacks can be registered to fire when cancellation is requested.
The structure carries both the promise *and* a plain `IO.Ref Bool` flag,
set in lockstep by `set`. `isSet` reads the flag directly (used on hot
paths like `Core.checkInterrupted`); `task`/`onSet` go through the
promise. The avoids a ~0.4% regression that a pure-promise
representation introduced.
API additions:
- `CancelToken.task : Task (Option Unit)`. Returns the underlying
promise's `result?` task directly — the same task object on every call,
so further `Task.map`/`BaseIO.bindTask` dependencies can be safely
attached. Resolves with `some ()` when `set` is called, or `none` if the
token is dropped without ever being set.
- `CancelToken.onSet : BaseIO Unit → BaseIO Unit`. Registers a callback
that runs synchronously on the cancelling thread when `set` is called
(or immediately if the token is already set). Implemented via
`BaseIO.chainTask` on `result?`, so no fresh `Task.map` per call and no
GC hazard.
Runtime cleanup:
- Add `LEAN_TASK_STATE_{WAITING,RUNNING,FINISHED}` constants in `lean.h`
matching `IO.TaskState`.
- Factor `lean::promise_is_resolved` inline in `object.h`, replacing
three open-coded `lean_io_get_task_state_core(...) == 2` checks (in
`interrupt.cpp`, `uv/timer.cpp`, `uv/signal.cpp`).
- Drop the manual `inc_ref(g_cancel_tk)` in `check_interrupted`; the
token is owned by the enclosing `scope_cancel_tk` for the duration of
the call (documented).
- Replace the bare `lean_always_assert(g_task_manager)` in
`lean_promise_new` with an explicit `lean_internal_panic` carrying a
message that names `Promise.new`, identifies the typical trigger
(`initialize` blocks, transitively via `IO.CancelToken.new`), and
recommends lazy construction. Without this, users got an opaque "LEAN
ASSERTION VIOLATION ... Condition: g_task_manager" with no actionable
hint.
Behavioural notes documented inline:
- `new` cannot be called from `initialize` blocks (task manager not
running yet); construct lazily.
- `task` documents the dropped-promise case (`none`) and steers callers
to `onSet` for callback chaining.
A consumer of `onSet` for parent → child cancel-token propagation in
parallel tactic combinators is in #13428 (fixes#13300).
Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
---------
Co-authored-by: Claude Opus 4.6 <noreply@anthropic.com>
This PR prevents memory exhaustion turning into segfaults when using
Lean functions which call into libuv
`malloc` can return `NULL`, in which case this code would previously go
on to dereference a null pointer.
Instead, it now returns a suitable `IO.Error`.
Calling `lean_internal_panic_out_of_memory` would also be an option
here, since the adjacent `lean_promise_new` calls would fail in this
way.
This PR replaces `exit(-1)` with `_exit(-1)` in the forked child
branches of `lean_io_process_spawn` (the `chdir` failure and `execvp`
failure paths). `exit` flushes inherited C stdio buffers, which share
underlying file descriptors with the parent. If the parent had a file
handle open with unflushed data, that data would be written to the file
in the child and then again when the parent later flushes, resulting in
duplicated output. `_exit` skips the stdio flush, so the parent's
buffered writes are no longer duplicated into inherited files.
Closes https://github.com/leanprover/lean4/issues/13463.
🤖 Prepared with [Claude Code](https://claude.com/claude-code)
Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
This PR fixes two minor bugs in `io.cpp`:
1. A resource leak in a Windows error path of
`Std.Time.Database.Windows.getNextTransition`
2. A buffer overrun in `IO.appPath` on linux when the executable is a
symlink at max path length.
This PR adds the option `LEAN_MI_SECURE` to our CMake build. It can be
configured with values `0`
through `4`. Every increment enables additional memory safety
mitigations in mimalloc, at the cost
of 2%-20% instruction count, depending on the benchmark. The option is
disabled by default in our
release builds as most of our users do not use the Lean runtime in
security sensitive situations.
Distributors and organization deploying production Lean code should
consider enabling the option as
a hardening measure. The effects of the various levels can be found at
https://github.com/microsoft/mimalloc/blob/v2.2.7/include/mimalloc/types.h#L56-L60.
This PR fixes a heap buffer overflow in `lean_io_prim_handle_read` that
was triggered through an
integer overflow in the size computation of an allocation. In addition
it places several checked
arithmetic operations on all relevant allocation paths to have potential
future overflows be turned
into crashes instead. The offending code now throws an out of memory
error instead.
Closes: #13388
This PR fixes a build issue when Lean is not linked against libuv.
## Problem
In `src/runtime/uv/dns.cpp`, the non-libuv stub of
`lean_uv_dns_get_info` (in the `#else` branch, compiled when building
without libuv) has a **4-parameter** signature:
```cpp
lean_uv_dns_get_info(b_obj_arg name, b_obj_arg service, uint8_t family, int8_t protocol)
```
But the real implementation above the `#else` has only **3 parameters**:
```cpp
lean_uv_dns_get_info(b_obj_arg name, b_obj_arg service, uint8_t family)
```
The Lean `@[extern]` declaration also expects 3 parameters. The stub has
an extra `int8_t protocol` parameter that the real function and the Lean
FFI caller do not use.
## Fix
Remove the extra `protocol` parameter from the stub so both branches
have the same signature.
## Evidence
Discovered while building Lean4 to WASM via Emscripten for a production
project ([specify-lean](https://github.com/kjsdesigns/specify)) since
v4.27.0. The stub branch is compiled in this configuration, and the
signature mismatch was caught at link time. The fix has been stable in
production across multiple Lean version bumps.
Related: [Zulip thread on WASM build
fixes](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)
(2026-03-21).
Co-authored-by: Keith Seim <keith@MacBook-Pro.local>
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>
This PR marks the `Inhabited` arguments of all functions in core marked
as `extern` as borrowed
(panicking array accessors and `panic!` itself). This in turn causes a
transitive effect throughout
the codebase and promotes most, if not all, `Inhabited` arguments to
functions to borrowed.
This PR increases Lean's default stack size, including for the main
thread of Lean executables, to 1GB.
As stack pages are allocated dynamically, this should not change the
memory usage of programs but can prevent them from stack overflowing.
The stack size (of any Lean thread) can now be customized via the
`LEAN_STACK_SIZE_KB` environment variable. `main` can be prevented from
running on a new thread by setting `LEAN_MAIN_USE_THREAD=0`, in which
case the default OS stack size management applies to the main thread
again.
This PR fixes some process signals that were incorrectly numbered.
From what I can tell, the code used signals and signal numbers for
Alpha/SPARC, not x86/ARM. The test was also broken and always green,
hiding the mistake.
This PR replaces three independent name demangling implementations
(Lean, C++, Python) with a single source of truth in
`Lean.Compiler.NameDemangling`. The new module handles the full
pipeline: prefix parsing (`l_`, `lp_`, `_init_`, `initialize_`,
`lean_apply_N`, `_lean_main`), postprocessing (suffix flags, private
name stripping, hygienic suffix stripping, specialization contexts),
backtrace line parsing, and C exports via `@[export]`.
The C++ runtime backtrace handler now calls the Lean-exported functions
instead of its own 792-line reimplementation. This is safe because
`print_backtrace` is only called from `lean_panic_impl` (soft panics),
not `lean_internal_panic`.
The Python profiler demangler (`script/profiler/lean_demangle.py`) is
replaced with a thin subprocess wrapper around a Lean CLI tool,
preserving the `demangle_lean_name` API so downstream scripts work
unchanged.
**New files:**
- `src/Lean/Compiler/NameDemangling.lean` — single source of truth (483
lines)
- `tests/lean/run/demangling.lean` — comprehensive tests (281 lines)
- `script/profiler/lean_demangle_cli.lean` — `c++filt`-style CLI tool
**Deleted files:**
- `src/runtime/demangle.cpp` (792 lines)
- `src/runtime/demangle.h` (26 lines)
- `script/profiler/test_demangle.py` (670 lines)
Net: −1,381 lines of duplicated C++/Python code.
🤖 Prepared with Claude Code
---------
Co-authored-by: Claude Opus 4.6 <noreply@anthropic.com>
This PR implements lazy initialization of closed terms. Previous work
has already made sure that ~70% of the closed terms occurring in core
can be statically initialized from the binary. With this the remaining
ones are initialized lazily instead of at startup.
For this we implement a small statically initializable lock that goes
with each term. When trying to access the term we quickly check a flag
to say whether it has already been initialized. If not we take the lock
and initialize it, otherwise we dereference the pointer and fetch the
value.
This PR removes the uses of `shared_timed_mutex` that were introduced
because we were stuck on C++14
with the `shared_mutex` available from C++17 and above.
This PR adds `IO.FS.Metadata.numLinks`, which contains the number of
hard links to a file.
This changes the implementation of `System.FilePath.metadata` and
`System.FilePath.symlinkMetadata` to use libuv. Otherwise, `st_nlink`
was not properly set on Windows. This also has the side benefit of
provided sub-second precision for file times on Windows (fulfilling an
old TODO). Also, while libuv supports `lstat` for Windows, enabling that
is left to a future PR.
This PR fixes a platform inconsistency in `IO.FS.removeFile` where it
could not delete read-only files on Windows.
The implementation now uses `uv_fs_unlink` instead of `std::remove`, as
libuv can delete read-only files. The PR also fixes a inconsistency in
`IO_test.lean` where it would generate files in the wrong directory when
run interactively.
---------
Co-authored-by: Markus Himmel <markus@himmel-villmar.de>
This PR avoids a potential deadlock on shutdown of a Lean program when
the number of pooled threads has temporarily been pushed above the
limit.
There's a potential race between the finalizer "waking up everyone"
after setting `m_shutting_down = true` and a worker that is about to be
throttled because of concurrency limits.
- `m_max_std_workers = 1`, `m_std_workers.size() = 2`, and the queue
still has tasks.
- Finalizer sets `m_shutting_down = true` and calls `notify_all()` while
a worker is running a task (outside of the mutex).
- Worker finishes a task, re-enters the loop, sees work, and "should
wait" because `active >= max`.
- Worker then calls `wait()` after the notify and never wakes, so
`join()` in the finalizer hangs.
This PR avoids the worker being blocked by not `wait()`ing if we are
already shutting down. The code is restructured a bit for readability,
where the first section is "there's no work in the queue" and the next
section is "there is some work in the queue"
This PR fixes a bug on Windows with `IO.Process.spawn` where setting an
environment variable to the empty string would not set the environment
variable on the subprocess.
Due to the way variable expansion and if interact in cmake, unquoted
variable expansions should essentially never be used inside if and may
lead to unexpected behavior. Also, quoted variable expansions can
usually be replaced by the unquoted variable name.
For more details, see this section in the cmake docs:
https://cmake.org/cmake/help/latest/command/if.html#variable-expansion
As one example of the kinds of issues that can occur with unquoted
variable expansions, consider this check from
`src/shell/CMakeLists.txt`, which tries to ensure that a test is only
run in non-WASM builds.
```cmake
if(NOT ${EMSCRIPTEN})
```
If the variable `EMSCRIPTEN` is empty or not defined (as is the case in
a non-WASM build), `${EMSCRIPTEN}` expands to 0 arguments, meaning the
check becomes
```cmake
if(NOT)
```
Since the `NOT` is unquoted, the if now tries to resolve it as a
variable. Since the variable `NOT` does not exist, the condition is
false and the test is never executed, even in non-WASM builds.
This PR fixes an issue that may sporadically trigger ASAN to got into a
deadlock when running a subprocess through the `IO.Process.spawn`
framework.
The general issue here is that we run `fork()` and then perform an
allocation in the child before going to `execvp` (for allocating the
arguments to `execvp`). As it turns out, doing this can cause a race
condition in ASAN that ultimately causes a deadlock in the child. This
was fixed upstream but then rolled back (see
https://github.com/google/sanitizers/issues/774). Thus, we must avoid
allocating any memory in between `fork` and `execvp`.
This PR adds a symbol to the runtime for marking `Array`
non-linearities. This should allow users to
spot them more easily in profiles or hunt them down using a debugger.
This PR improves the performance of `getLine` by coalescing the locking
of the underlying `FILE*`.
Unfortunately we cannot use `getline` or `fgets` for this as our code
needs to handle `\0` chars
and Windows.
This PR ensures that `Nat`s in `.olean` files use a deterministic
serialization in the case where `LEAN_USE_GMP` is not set.
This is a simplified version of
https://github.com/leanprover/lean4/pull/2908.
This PR moves the processing of options passed to the CLI from
`shell.cpp` to `Shell.lean`.
As with previous ports, this attempts to mirror as much of the original
behavior as possible, Benefits to be gained from the ported code can
come in later PRs. There should be no significant behavioral changes
from this port. Nonetheless, error reporting has changed some, hopefully
for the better. For instance, errors for improper argument
configurations has been made more consistent (e.g., Lean will now error
if numeric arguments fall outside the expected range for an option).
(Redo of #11345 to fix Windows issue.)
This PR moves the processing of options passed to the CLI from
`shell.cpp` to `Shell.lean`.
As with previous ports, this attempts to mirror as much of the original
behavior as possible, Benefits to be gained from the ported code can
come in later PRs. There should be no significant behavioral changes
from this port. Nonetheless, error reporting has changed some, hopefully
for the better. For instance, errors for improper argument
configurations has been made more consistent (e.g., Lean will now error
if numeric arguments fall outside the expected range for an option).
Given its run time of >2hrs, the job is added as a secondary job for
nightly releases and a primary job for full releases. A new check level
for differentiating between nightlies and full releases is added for
this.
(Trying to) reactivate lsan will happen in a follow-up PR.
This PR fixes several memory leaks in the new `String` API.
These leaks are mostly situations where we forgot to put borrowing
annotations. The single
exception is the new `String` constructor `ofByteArray`. It cannot take
the `ByteArray` as
a borrowed argument anymore and must thus free it on its own.
