This PR fixes a regression introduced in Lean 4.29.0-rc2 where `simp` no longer
simplifies inside type class instance arguments due to the
`backward.isDefEq.respectTransparency` change. This breaks proofs where a term
like `(a :: l).length` appears both in the main expression and inside implicit
instance arguments (e.g., determining a `BitVec` width). After
`simp only [List.length_cons]`, the main expression has `l.length + 1` but
instances still have `(a :: l).length`, and `isDefEq` won't unfold `List.length`
to reconcile them.
Marking `List.length` as `@[implicit_reducible]` allows `isDefEq` to unfold it
when checking implicit arguments, restoring the previous behavior.
The root cause is that `GetElem` carries complex proof obligations in its type
class instances, making the implicit arguments sensitive to definitional equality.
We are considering a longer-term redesign with a noncomputable `GetElemV` variant
based on `Nonempty` that avoids these casts entirely, but that is a larger change
planned for a future release.
Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
This PR modifies `#eval e` to elaborate `e` with section variables in
scope. While evaluating expressions with free variables is not possible,
this lets `#eval` give a better error message than "unknown identifier."
Example:
```lean
section
variable (n : Nat)
/-- error: Cannot evaluate, contains free variable `n` -/
#guard_msgs in #eval n
end
```
The error is localized to `#eval`. It would be more friendly if the
error were to be placed on uses of free variables.
[Zulip
discussion](https://leanprover.zulipchat.com/#narrow/channel/270676-lean4/topic/Unknown.20identifier.20error.20messages.20for.20.60.23eval.60/near/560864544)
This PR changes the elaboration of the `structure`/`class` commands so
that default values have later fields in context as well. This allows
field defaults to depend on fields that come both before and after them.
While this was already the case for inherited fields to some degree, it
now applies uniformly to all fields. Additionally, when elaborating the
default value for a field, all fields that depend on it are cleared from
the context to avoid situations where the default value depends on
itself.
This addresses an issue reported by Aaron Liu [on
Zulip](https://leanprover.zulipchat.com/#narrow/channel/270676-lean4/topic/default.20structure.20values.20can.20depend.20on.20themselves/near/578014370).
This PR changes "structure-like" terminology to "non-recursive
structure" across internal documentation, error messages, the
metaprogramming API, and the kernel, to clarify Lean's type theory. A
*structure* is a one-constructor inductive type with no indices — these
can be created by either the `structure` or `inductive` commands — and
are supported by the primitive `Expr.proj` projections. Only
*non-recursive* structures have an eta conversion rule. The PR
description contains the APIs that were renamed.
Addresses RFC #5891, which proposed this rename. The change is motivated
by the need to distinguish between `structure`-defined structures,
structures, and non-recursive structures. Especially since #5783, which
enabled the `structure` command to define recursive structures,
"structure-like" has been easy to misunderstand.
Changes:
- Kernel: `is_structure_like()` -> `is_non_rec_structure()`
- `Lean.isStructureLike` -> `Lean.isNonRecStructure`
- `Lean.matchConstStructLike` -> `Lean.matchConstNonRecStructure`
- `Lean.getStructureLikeCtor?` -> `Lean.getNonRecStructureCtor?`
- `Lean.getStructureLikeNumFields` -> `Lean.getNonRecStructureNumFields`
- `Lean.Expr.proj`: extended and corrected documentation (note: despite
the fact that not every projection can be written as a recursor
application, I left in this claim since it seems good to document a
more-restrictive specification, and some users have requested the kernel
be more restrictive in this way)
Closes#5891
This PR changes the default behavior of the `restoreAllArtifacts`
package configuration to mirror that of the workspace. If the workspace
also has it unset, the default remains the same (`false`).
This PR changes Lake to only emit `.nobuild` traces (introduced in
#12076) if the normal trace file already exists. This fixes an issue
where a `lake build --no-build` would create the build directory and
thereby prevent a cloud release fetch in a future build.
This PR migrates most remaining tests to the new test suite. It also
completes the migration of directories like `tests/lean/run`, meaning
that PRs trying to add tests to those old directories will now fail.
This PR solves three distinct issues with the handling of
`ite`/`dite`,`decide`.
1) We prevent the simprocs from picking up `noncomputable`, `Classical`
instances, such as `Classical.propDecidable`, when simplifying the
proposition in `ite`/`dite`/`decide`.
2) We fix a type mismatch occurring when the condition/proposition is
unchanged but the `Decidable` instance is simplified.
3) If we rewrite the proposition from `c` to `c'` and the evaluation of
the original instance `Decidable c` gets stuck we try fallback path of
of obtaining `Decidable c'` instance and evaluating it. This matters
when the instance is evaluated via `cbv_eval` lemmas.
---------
Co-authored-by: Claude Opus 4.6 <noreply@anthropic.com>
This PR implements a merge sort algorithm on arrays. It has been
measured to be about twice as fast as `List.mergeSort` for large arrays
with random elements, but for small or almost sorted ones, the list
implementation is faster. Compared to `Array.qsort`, it is stable and
has O(n log n) worst-case cost. Note: There is still a lot of potential
for optimization. The current implementation allocates O(n log n)
arrays, one per recursive call.
---------
Co-authored-by: Claude Opus 4.6 <noreply@anthropic.com>
This PR adjusts the module parser to set the leading whitespace of the
first token to the whitespace up to that token. If there are no actual
tokens in the file, the leading whitespace is set on the final (empty)
EOI token. This ensures that we do not lose the initial whitespace (e.g.
comments) of a file in `Syntax`.
(Tests generated/adjusted by Claude)
Co-authored-by: Claude Sonnet 4.6 <noreply@anthropic.com>
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 adds tests and a benchmark exercising `instantiateMVars` on
metavariable assignment graphs with nested delayed assignments, in
preparation for optimizing the delayed mvar resolution path.
- `tests/elab/instantiateMVarsShadow.lean`: Two test cases for
correctness when the same fvar is bound to different values at different
scope levels (fvar shadowing and late-bind patterns). A buggy cache
could return a stale result from one scope level in another.
- `tests/elab/instantiateMVarsSharing.lean`: Verifies correct resolution
and object sharing on a graph with nested delayed mvars producing `∀ s,
(s = s → (s = s) ∧ (s = s)) ∧ (s = s)`.
- `tests/elab_bench/delayed_assign.lean`: Constructs an O(n²) delayed
mvar graph (n=700) and measures `instantiateMVars` resolution time,
calibrated to ~1s total elaboration.
🤖 Generated with [Claude Code](https://claude.com/claude-code)
---------
Co-authored-by: Claude Opus 4.6 <noreply@anthropic.com>
This PR adds a warning to any `def` of class type that does not also
declare an appropriate reducibility.
The warning check runs after elaboration (checking the actual
reducibility status via `getReducibilityStatus`) rather than
syntactically checking modifiers before elaboration. This is necessary
to accommodate patterns like `@[to_additive (attr :=
implicit_reducible)]` in Mathlib, where the reducibility attribute is
applied during `.afterCompilation` by another attribute, and would be
missed by a purely syntactic check.
---------
Co-authored-by: Paul Reichert <6992158+datokrat@users.noreply.github.com>
Co-authored-by: Kim Morrison <kim@tqft.net>
Co-authored-by: Claude Opus 4.6 <noreply@anthropic.com>
This PR moves the universe-level-count check from
`unfold_definition_core` into `is_delta`, establishing the invariant
that if `is_delta` succeeds then `unfold_definition` also succeeds. This
prevents a crash (SIGSEGV or garbled error) that occurred when call
sites in `lazy_delta_reduction_step` unconditionally dereferenced the
result of `unfold_definition` even on a level-parameter-count mismatch.
Additionally, moves the `is_prop` check for theorem types in
`add_theorem` to occur after `check_constant_val`, so the type is
verified to be well-formed before `is_prop` evaluates it. This prevents
`is_prop` from being called on an ill-typed term when a malformed
theorem declaration is supplied.
Fixes#10577.
---------
Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
Co-authored-by: nomeata <148037+nomeata@users.noreply.github.com>
This PR reverts https://github.com/leanprover/lean4/pull/12757.
We suspect this caused the v4.29.0-rc5 tag CI to fail. All 6 test jobs
on the tag CI (run
https://github.com/leanprover/lean4/actions/runs/22699133179) are
failing with:
```
PANIC at _private.Lean.Environment.0.Lean.EnvExtension.getStateUnsafe Lean.Environment:1425:6:
called on `async` extension, must set `asyncDecl` or pass `(asyncMode := .local)` to explicitly access local state
```
29 tests fail, affecting deriving, grind, linter, interactive, and pkg
tests. The v4.29.0-rc4 tag CI passed, and the only code changes between
rc4 and rc5 are this PR and
https://github.com/leanprover/lean4/pull/12782. The failure only
manifests in release builds (with `LEAN_VERSION_IS_RELEASE=1` and
`CHECK_OLEAN_VERSION=ON`).
🤖 Prepared with Claude Code
This PR changes Lake to use the modification times of traces (where
available) for artifact modification times.
When artifacts are hard-linked from the cache, they retain the
modification time of the artifact in the cache. Thus, the artifact
modification time is an unreliable metric for determining whether an
artifact is up-to-date relative to other artifacts in the presence of
the cache. The trace file, however, is modified consistently when the
artifacts are updated, making it the most reliable indicator of
modification time.
This PR fixes a false positive in `release_checklist.py` where the check
for the dev cycle being started would fail even when it was correctly
set up.
The script was looking for `set(LEAN_VERSION_IS_RELEASE 0)` as an exact
prefix match, but CMakeLists.txt uses the CMake cache variable form:
`set(LEAN_VERSION_IS_RELEASE 0 CACHE STRING "")`. The fix uses a regex
that handles both syntaxes.
This was discovered during the v4.29.0-rc4 release when the checklist
incorrectly reported that a "begin dev cycle" PR was needed, even though
PR #12526 had already set `LEAN_VERSION_IS_RELEASE 0` and
`LEAN_VERSION_MINOR 30` on master.
🤖 Prepared with Claude Code
Co-authored-by: Claude Sonnet 4.6 <noreply@anthropic.com>
This PR marks `Id.run` as `[implicit_reducible]` to ensure that
`Id.instMonadLiftTOfPure` and `instMonadLiftT Id` are definitionally
equal when using `.implicitReducible` transparency setting.
This PR takes a more principled approach in deriving `String` pattern
lemmas by reducing to simpler cases similar to how the instances are
defined.
This reduces duplication of complex arguments (at the expense of having
to state more simple lemmas; however these lemmas are useful to users as
well).
This PR adds a `set_option cbv.maxSteps N` option that controls the
maximum
number of simplification steps the `cbv` tactic performs. Previously the
limit
was hardcoded to the `Sym.Simp.Config` default of 100,000 with no way
for
users to override it. The option is threaded through `cbvCore`,
`cbvEntry`,
`cbvGoal`, and `cbvDecideGoal`.
🤖 Generated with [Claude Code](https://claude.com/claude-code)
---------
Co-authored-by: Claude Opus 4.6 <noreply@anthropic.com>
This PR moves cbv tests to the correct test directories. `cbv4.lean` is
a
straightforward elaboration test and is moved to `tests/elab/`. The AES
and ARM
load/store tests are performance-oriented stress tests and are moved to
`tests/elab_bench/`.
Co-authored-by: Claude Opus 4.6 <noreply@anthropic.com>
This PR makes the compiler removes arguments to join points that are
void, avoiding a bunch of dead
stores in the bytecode and the initial C (though LLVM was surely able to
optimize these away further
down the line already).
This PR introduces the core HTTP data types: `Request`, `Response`,
`Status`, `Version`, and `Method`. Currently, URIs are represented as
`String` and headers as `HashMap String (Array String)`. These are
placeholders, future PRs will replace them with strict implementations.
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 skips the noncomputable pre-check in `processDefDeriving` when
the instance type is `Prop`. Since proofs are erased by the compiler,
computability is irrelevant for `Prop`-valued instances.
Previously (since https://github.com/leanprover/lean4/pull/12756),
`deriving instance` would reject instances that transitively depend on
noncomputable definitions, even when the class extends `Prop`. This came
up in mathlib where `Precoverage.IsStableUnderBaseChange` (a `Prop`
class) needs `deriving noncomputable instance` unnecessarily.
🤖 Prepared with Claude Code
Co-authored-by: Claude Opus 4.6 <noreply@anthropic.com>
This PR fixes `release_steps.py` for `verso`. After running `lake
update` in the root, the `test-projects/*/lake-manifest.json` files
retain stale subverso pins, causing verso's "SubVerso version
consistency" CI check to fail. The fix syncs the root manifest's
subverso rev into all test-project sub-manifests.
Root cause: verso has nested Lake projects in `test-projects/` each with
their own `lake-manifest.json`. Running `lake update` in the root
updates the root manifest but doesn't touch the nested ones.
🤖 Prepared with Claude Code
---------
Co-authored-by: Claude Sonnet 4.6 <noreply@anthropic.com>
This PR adds high priority to instances for `OfSemiring.Q` in the grind
ring envelope. When Mathlib is imported, instance synthesis for types
like `OfSemiring.Q Nat` becomes very expensive because the solver
explores many irrelevant paths before finding the correct instances. By
marking these instances as high priority and adding shortcut instances
for basic operations (`Add`, `Sub`, `Mul`, `Neg`, `OfNat`, `NatCast`,
`IntCast`, `HPow`), instance synthesis resolves quickly.
🤖 Generated with [Claude Code](https://claude.com/claude-code)
---------
Co-authored-by: Claude Opus 4.6 <noreply@anthropic.com>
Co-authored-by: Kim Morrison <kim@tqft.net>
This PR fixes `release_checklist.py` to report failing CI checks
immediately, even when other checks are still in progress. Previously,
having any in-progress checks would return `"pending"` status, masking
failures that had already occurred. Now it returns `"failure"` with a
message like `"1 check(s) failing, 2 still in progress"`.
Also adds a section to `.claude/commands/release.md` instructing the AI
assistant to investigate any CI failure immediately rather than
reporting it as "in progress" and moving on.
🤖 Prepared with Claude Code
Co-authored-by: Claude Sonnet 4.6 <noreply@anthropic.com>
This PR fixes a parsing bug in \`release_checklist.py\` introduced by
https://github.com/leanprover/lean4/pull/12700, which reformatted
\`src/CMakeLists.txt\` to use \`CACHE STRING \"\"\`:
\`\`\`cmake
set(LEAN_VERSION_MINOR 30 CACHE STRING "")
\`\`\`
The old code used \`split()[-1].rstrip(")")\` to extract the version
number, which now yields \`""\` (the empty string argument) instead of
the minor version. Use a regex to extract the digit directly.
🤖 Prepared with Claude Code
Co-authored-by: Claude Sonnet 4.6 <noreply@anthropic.com>
This PR adds user-facing API lemmas for `s.contains t`, where `s` and
`t` are both a string or a slice.
Under the hood these lemmas are backed by the correctness proof for KMP
that was added a few weeks ago.
This PR fixes a CMake scoping bug that made `-DLEAN_VERSION_*` overrides
ineffective.
The version variables (`LEAN_VERSION_MAJOR`, `MINOR`, `PATCH`,
`IS_RELEASE`) were declared with plain `set()`, which creates normal
variables that shadow cache variables set by `-D` on the command line.
The fix changes them to `CACHE STRING ""` to match the existing
`LEAN_SPECIAL_VERSION_DESC` pattern.
However, `CACHE STRING ""` alone isn't sufficient because `project(LEAN
CXX C)` implicitly creates empty `LEAN_VERSION_{MAJOR,MINOR,PATCH}`
normal variables (CMake sets `<PROJECT>_VERSION_*` for the project
name). These shadow the cache values, so we `unset()` them after the
cache declarations to let `${VAR}` fall through to the cache.
Closes https://github.com/leanprover/lean4/issues/12681🤖 Prepared with Claude Code
---------
Co-authored-by: Claude Opus 4.6 <noreply@anthropic.com>
This PR replaces `lean.code-workspace` with standard `.vscode/`
configuration
files (`settings.json`, `tasks.json`, `extensions.json`). The workspace
file
required users to explicitly "Open Workspace from File" (and moreover
gives a
noisy prompt whether or not they want to open it), while `.vscode/`
settings
are picked up automatically when opening the folder. This became
possible after
#12652 reduced the workspace to a single folder.
Also drops the `rewrap.wrappingColumn` markdown setting, as the Rewrap
extension
is no longer signed on the VS Code marketplace.
🤖 Prepared with Claude Code
Co-authored-by: Claude Opus 4.6 <noreply@anthropic.com>
This PR deprecates `levelZero` in favor of `Level.zero` and `levelOne`
in favor of the new `Level.one`, and updates all usages throughout the
codebase. The `levelZero` alias was previously required for computed
field `data` to work, but this is no longer needed.
🤖 Prepared with Claude Code
This PR adds general projection lemmas for `ExceptConds` conjunction:
- `ExceptConds.and_elim_left`: `(x ∧ₑ y) ⊢ₑ x`
- `ExceptConds.and_elim_right`: `(x ∧ₑ y) ⊢ₑ y`
The existing `and_true`, `true_and`, `and_false`, `false_and` are
refactored as one-line corollaries.
Suggested by @sgraf812 in
https://github.com/leanprover-community/cslib/pull/376#discussion_r2066993469.
🤖 Prepared with Claude Code
Co-authored-by: Claude Opus 4.6 <noreply@anthropic.com>
MacOS uses a very old version of bash where `"${FOO[@]}"` fails if `set
-u` is enabled and `FOO` is undefined. Newer versions of bash expand
this to zero arguments instead.
Also, `lint.py` used the shebang `#!/usr/bin/env python` instead of
`python3`, which fails on some systems.
In CI, all macos tests run on nscloud runners. Presumably, they have
installed newer versions of various software, hence this didn't break in
CI.
This PR fixes `@[implicit_reducible]` on well-founded recursive
definitions.
`addPreDefAttributes` sets WF-recursive definitions as `@[irreducible]`
by default, skipping this only when the user explicitly wrote
`@[reducible]` or `@[semireducible]`. It was missing
`@[instance_reducible]` and `@[implicit_reducible]`, causing those
attributes to be silently overridden.
Add `instance_reducible` and `implicit_reducible` to the check in
`src/Lean/Elab/PreDefinition/Mutual.lean` that guards against overriding
user-specified reducibility attributes, and add regression tests in
`tests/elab/wfirred.lean`.
## Example
```lean
-- Before fix: printed @[irreducible] def f : List Nat → Nat
-- After fix: printed @[implicit_reducible] def f : List Nat → Nat
@[instance_reducible] def f : ∀ _l : List Nat, Nat
| [] => 0
| [_x] => 1
| x :: y :: l => if h : x = y then f (x :: l) else f l + 2
termination_by l => sizeOf l
#print sig f
```
Fixes#12775
---------
Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
Co-authored-by: nomeata <148037+nomeata@users.noreply.github.com>
This PR provides a `ForwardPatternModel` for string patterns and deduces
theorems and lawfulness instances from the corresponding results for
slice patterns.
