This PR adds warnings when registering `@[simp]` theorems whose
left-hand side has a problematic head symbol in the discrimination tree:
- **Variable head** (`.star` key): The theorem will be tried on every
`simp` step, which can be expensive. The warning notes this may be
acceptable for `local` or `scoped` simp lemmas. Controlled by
`warning.simp.varHead` (default: `true`).
- **Unrecognized head** (`.other` key, e.g. a lambda expression): The
theorem is unlikely to ever be applied by `simp`. Controlled by
`warning.simp.otherHead` (default: `true`).
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 introduces the H1 module, a pure HTTP/1.1 state machine that
incrementally parses incoming byte streams and emits response bytes
without side effects.
This contains the same code as #10478, divided into separate pieces to
facilitate easier review.
The pieces of this feature are:
- Core data structures: #12126
- Headers: #12127
- URI: #12128
- Body: #12144
- H1: #12146
- Server: #12151
- Client:
---------
Co-authored-by: Rob23oba <152706811+Rob23oba@users.noreply.github.com>
This PR changes the linear BEq derivation strategy to use `Nat.decEq`
instead of `decEq` when comparing constructor indices. Since constructor
indices are always `Nat`, using `Nat.decEq` directly is more appropriate
because it is `@[reducible]`, whereas the generic `decEq` is only
semireducible and does not unfold at `.reducible` transparency. This
makes the generated code more transparent-friendly.
Co-authored-by: Claude Opus 4.6 <noreply@anthropic.com>
This PR fixes#13268 where `local macro` (and other local declarations)
with compound names of depth ≥ 3 would silently lose their local
entries.
When `expandNamespacedDeclaration` rewrites e.g. `local macro (name :=
A.B.C) ...` into `namespace A.B.C; end_local_scope; ...; end A.B.C`, the
compound `namespace A.B.C` pushes multiple scopes, but `end_local_scope`
only marked the topmost scope as non-delimiting. This meant
`addLocalEntry`'s stack traversal would stop at the first unmarked
scope, and the local entry would be lost when the namespace scopes were
popped.
The fix parameterizes `end_local_scope` with a depth argument so it
marks exactly the right number of scope levels as non-delimiting.
`expandNamespacedDeclaration` now passes `ns.getNumParts` as the depth,
and `expandInCmd` passes `1`.
Closes#13268
This PR fixes a compiler panic when a structure constructor receives a
noncomputable instance as an instance-implicit argument.
The LCNF translation first visits the instance in an irrelevant position
(type parameter) where `ignoreNoncomputable` is `true`, caches the
result, and then reuses that cached entry in a relevant position,
bypassing `checkComputable`. Adding `ignoreNoncomputable` to the cache
key ensures the two contexts do not share cache entries.
Fixes#13371
This PR adds a `linter.redundantVisibility` option (default `true`) that
warns
when a visibility modifier has no effect because it matches the default
for the
current context:
- `private` outside a `public section` in a `module` file, where
declarations
are already module-scoped by default
- `public` in a non-`module` file or inside a `public section`, where
declarations are already public by default
The check is integrated directly into `elabModifiers` so it covers all
declaration types uniformly.
---------
Co-authored-by: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
This PR fixes `SizeOf` instance generation for public inductive types
that have
private constructors. The spec theorem proof construction needs to
unfold
`_sizeOf` helper functions which may not be exposed in the public view,
so
we use `withoutExporting` for the proof construction and type check.
Closes#13373
Co-authored-by: Claude Opus 4.6 <noreply@anthropic.com>
This PR fixes git revision detection in worktrees where the worktree's
gitdir path passes through another git repository.
The vendored `GetGitRevisionDescription.cmake` module detects worktrees
and then calls `_git_find_closest_git_dir` to find the shared git
directory by walking up the filesystem looking for a `.git` entry. This
fails when the worktree's gitdir is stored inside another git repository
(e.g. when the project is a git submodule whose objects live at
`~/.git/modules/...` and `~` is itself a git repo) — the walk finds the
wrong `.git`.
The fix reads the `commondir` file that git places in every worktree's
gitdir, which directly points to the shared git object directory. Falls
back to the old filesystem walk if `commondir` doesn't exist (shouldn't
happen with any modern git, but safe to keep).
🤖 Prepared with Claude Code
Co-authored-by: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
Previously, `elabInitialize` only checked for explicit `private` when
deciding whether to mangle `fullId`, ignoring the `module` system's
default-private semantics. It also overrode the user's visibility for
the generated `initFn` via `visibility.ofBool`.
Now, `elabInitialize` uses `elabVisibility` + `isInferredPublic` to
correctly handle all visibility contexts. The generated `initFn`
inherits the user's visibility rather than being forced public.
Also factors out `elabVisibility` from `elabModifiers` for reuse.
This PR is based on a systematic review of all read-only operations on
the default containers in core. Where sensible it applies specialize
annotations on higher order operations that lack them or borrow
annotations on parameters that should morally be borrowed (e.g. the
container when iterating over it).
This PR changes the `Inhabited` deriving handler for `structure` types
to use default field values when present; this ensures that `{}` and
`default` are interchangeable when all fields have default values. The
handler effectively uses `by refine' {..} <;> exact default` to
construct the inhabitant. (Note: when default field values cannot be
resolved, they are ignored, as usual for ellipsis mode.)
Implementation note: the handler now constructs the `Expr` directly and
adds it to the environment, though the `instance` is still added using
`elabCommand`.
Closes#9463
This PR adds a check for OS-forbidden names and characters in module
names. This implements the functionality of `modulesOSForbidden` linter
of mathlib.
Instead of unconditionally wrapping value of fields that were copied
from flattened parent structures, try finding an existing instance and
projecting it first.
This PR extends Lean's syntax to allow explicit universe levels in
expressions such as `e.f.{u,v}`, `(f e).g.{u}`, and `e |>.f.{u,v} x y
z`. It fixes a bug where universe levels would be attributed to the
wrong expression; for example `x.f.{u}` would be interpreted as
`x.{u}.f`. It also changes the syntax of top-level declarations to not
allow space between the identifier and the universe level list, and it
fixes a bug in the `checkWsBefore` parser where it would not detect
whitespace across `optional` parsers.
Closes#8743
This PR changes the Lake core build to use `weakLeanArgs` for the Lake
plugin.
This fixes a trace mismatch between local builds and the CI caused by
the differing paths.
This PR fixes universe unification for `for` loops with `mut` variables
whose types span multiple implicit universes. The old approach used
`ensureHasType (mkSort mi.u.succ)` per variable, which generated
constraints like `max (?u+1) (?v+1) =?= ?u+1` that the universe solver
cannot decompose. The new approach uses `getDecLevel`/`isLevelDefEq` on
the decremented level, producing `max ?u ?v =?= ?u` which `solveSelfMax`
handles directly.
Co-authored-by: Claude Opus 4.6 <noreply@anthropic.com>
This PR wraps the top-level command parser with `withPosition` to
enforce indentation in `by` blocks, combined with an empty-by fallback
for better error messages.
This subsumes #3215 (which introduced `withPosition commandParser` but
without the empty-by fallback). It is also related to #9524, which
explores elaboration with empty tactic sequences — this PR reuses that
idea for the empty-by fallback, so that a `by` not followed by an
indented tactic produces an elaboration error (unsolved goals) rather
than a parse error.
**Changes:**
- `topLevelCommandParserFn` now uses `(withPosition commandParser).fn`,
setting the saved position at the start of each top-level command
- `tacticSeqIndentGt` gains an empty tactic sequence fallback
(`pushNone`) so that missing indentation produces an elaboration error
(unsolved goals) instead of a parse error
- `isEmptyBy` in `goalsAt?` removed: with strict `by` indentation, empty
`by` blocks parse successfully via `pushNone` (producing empty nodes)
rather than producing `.missing` syntax, making the `isEmptyBy` check
dead code. The `isEmpty` helper in `isSyntheticTacticCompletion`
continues to work correctly because it handles both `.missing` and empty
nodes from `pushNone` (via the vacuously-true `args.all isEmpty` on
`#[]`)
- Test files updated to indent `by` blocks and expression continuations
that were previously at column 0
**Behavior:**
- Top-level `by` blocks now require indentation (column > 0 for commands
at column 0)
- Commands indented inside `section` require proofs to be indented past
the command's column
- `#guard_msgs in example : True := by` works because tactic indentation
is checked against the outermost command's column
- Expression continuations (not just `by`) must also be indented past
the command, which is slightly more strict but more consistent
- `have : True := by` followed by a dedent now correctly puts `this` in
scope in the outer tactic block (the `have` is structurally complete
with an unsolved-goal error, rather than a parse error)
**Code changes observed in practice (lean4 test suite + Mathlib):**
- `by` blocks: top-level `theorem ... := by` / `decreasing_by` followed
by tactics at column 0 must be indented
- `variable` continuations: `variable {A : Type*} [Foo A]\n{B : Type*}`
where the second line starts at column 0 must be indented (most common
category in Mathlib)
- Expression continuations: `def f : T :=\nexpr` or `#synth Foo\n[args]`
where the body/arguments start at column 0
- Structure literals: `.symm\n{ toFun := ...` where the struct literal
starts at column 0
🤖 Generated with [Claude Code](https://claude.com/claude-code)
Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
---------
Co-authored-by: Claude Opus 4.6 <noreply@anthropic.com>
This PR wires the `PowIdentity` typeclass (from
https://github.com/leanprover/lean4/pull/13086) into the `grind` ring
solver's Groebner basis engine.
When a ring has a `PowIdentity α p` instance, the solver pushes `x ^ p =
x` as a new fact for each variable `x`, which becomes `x^p - x = 0` in
the Groebner basis. Since `p` is an `outParam`, instance discovery is
decoupled from `IsCharP` — the solver synthesizes `PowIdentity α ?p`
with a fresh metavar and lets instance search find both the instance and
the exponent.
This correctly handles non-prime finite fields: for `F_4` (char 2, 4
elements), Mathlib would provide `PowIdentity F_4 4` and the solver
would discover `p = 4`, not `p = 2`.
Note: the original motivating example `(x + y)^2 = x^128 + y^2` from
https://github.com/leanprover/lean4/issues/12842 does not yet work
because the `ToInt` module lifts `Fin 2` expressions to integers and
expands `x^128` via the binomial theorem before the ring solver can
reduce it. Addressing that is a separate deeper change.
🤖 Prepared with Claude Code
---------
Co-authored-by: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
This PR adds an optional `markMeta : Bool := false` parameter to
`addAndCompile`, so that callers can propagate the `meta` marking
without manually splitting into `addDecl` + `markMeta` + `compileDecl`.
Also updates `ParserCompiler` to use the new parameter.
🤖 Prepared with Claude Code
---------
Co-authored-by: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
This PR adds a `Lean.Grind.PowIdentity` typeclass stating that `x ^ p =
x` for all elements of a commutative semiring, with `p` as an
`outParam`.
The primary source of instances is Fermat's little theorem: for a finite
field with `q` elements, `x ^ q = x`. Since `p` is an `outParam`,
instance synthesis discovers the correct exponent automatically — the
solver does not need to know the characteristic or cardinality in
advance.
A concrete instance for `Fin 2` is provided. Mathlib can provide
instances for general finite fields via `FiniteField.pow_card`.
🤖 Prepared with Claude Code
Co-authored-by: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
This PR amends #13317 to suggest `:= (rfl)` as the recommended way to
avoid a theorem to be automatically marked `[defeq]`, for consistency
with existing documentation. Rationale: the special treatment of `:=
rfl` is based on syntax, not the proof term, so it’s appropriate to use
different syntax. And also I like the way it reads like a “muted whisper
of `rfl`”.
This PR adds a warning preventing a user from applying global attribute
using `... in ...`, e.g.
```lean4
theorem a : True := trivial
attribute [simp] a in
def b : True := a
```
This PR adds an opt-in linter (`set_option simp.rfl.checkTransparency
true`) that warns when a `rfl` simp theorem's LHS and RHS are not
definitionally equal at `.instances` transparency. Bad rfl-simp theorems
— those that only hold at higher transparency — create problems
throughout the system because `simp` and `dsimp` operate at restricted
transparency. The linter suggests two fixes: use `id rfl` as the proof
(to remove the `rfl` status), or mark relevant constants as
`[implicit_reducible]`.
This is part of a broader effort to ensure `isDefEq` respects
transparency levels. The linter helps systematically identify
problematic rfl-simp theorems so they can be fixed incrementally.
Co-authored-by: Claude Opus 4.6 <noreply@anthropic.com>
This PR adds `prod` (multiplicative fold) for `List`, `Array`, and
`Vector`, mirroring the existing `sum` API. Includes basic simp lemmas
(`prod_nil`, `prod_cons`, `prod_append`, `prod_singleton`,
`prod_reverse`, `prod_push`, `prod_eq_foldl`), Nat-specialized lemmas
(`prod_pos_iff_forall_pos_nat`, `prod_eq_zero_iff_exists_zero_nat`,
`prod_replicate_nat`), Int-specialized lemmas (`prod_replicate_int`),
cross-type lemmas (`prod_toArray`, `prod_toList`), and `Perm.prod_nat`
with grind patterns.
The min/max pigeonhole-style bounds from the `sum` Nat/Int files are
omitted as they don't have natural multiplicative analogues.
🤖 Prepared with Claude Code
Co-authored-by: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
This PR introduces the `WFAIL` CMake setting that uses `--wfail` for
Lake builds of core.
This also, by extension, fixes a mismatch in the trace of core CI builds
vs local core builds.
This PR makes the delta-deriving handler create `theorem` declarations
instead of `def` declarations when the instance type is a `Prop`.
Previously, `deriving instance Nonempty for Foo` would always create a
`def`, which is inconsistent with the behavior of a handwritten
`instance` declaration.
For example, given:
```lean
def Foo (α : Type u) := List α
deriving instance Nonempty for Foo
```
Before: `@[implicit_reducible] def instNonemptyFoo ...`
After: `@[implicit_reducible] theorem instNonemptyFoo ...`
The implementation checks `isProp result.type` after constructing the
instance closure, and uses `mkThmOrUnsafeDef` for the Prop case (which
also handles the unsafe fallback correctly). The noncomputable check is
skipped for Prop-typed instances since theorems can freely reference
noncomputable constants.
Closes#13295🤖 Prepared with Claude Code
---------
Co-authored-by: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
This PR makes `release_steps.py` robust to release repos that have no
`nightly-testing` branch. Previously, `git merge origin/nightly-testing`
would fail with "not something we can merge" and the error handler
misinterpreted this as a merge conflict, then crashed trying to commit
with nothing to commit. Now we check for the branch with
`git ls-remote --heads` before attempting the merge.
🤖 Prepared with Claude Code
---------
Co-authored-by: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
This PR updates `release_steps.py` to sync all `lean-toolchain` files in
verso's `test-projects/` subdirectories to match the root toolchain
during release bumps. The verso CI "SubVerso version consistency" check
requires these to match, and the script was only syncing
`lake-manifest.json` sub-manifests but not toolchain files.
🤖 Prepared with Claude Code
Co-authored-by: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
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>
