This PR fixes a crash in the `cbv` tactic's `handleProj` simproc when
processing a dependent projection (e.g. `Sigma.snd`) whose struct is
rewritten via `@[cbv_eval]` to a non-definitionally-equal term that
cannot be further reduced.
- Previously, `handleProj` returned `.rfl (done := false)`, causing the
`.proj` expression to flow into `simpStep` which throws "unexpected
kernel projection term"
- The fix marks the result as `done := true` so that `cbv` gracefully
gets stuck instead of crashing
- Adds regression tests for dependent projections on `Sigma`, custom
structures, and `Subtype`
🤖 Generated with [Claude Code](https://claude.com/claude-code)
Co-authored-by: Claude Opus 4.6 <noreply@anthropic.com>
This PR registers the
[leanprover/skills](https://github.com/leanprover/skills) plugin
marketplace in `.claude/settings.json` so that Claude Code users working
on lean4 are automatically prompted to install it.
Also un-ignores `.claude/settings.json` in `.gitignore` — the blanket
`settings.json` rule was blocking it from being tracked.
🤖 Prepared with Claude Code
This PR makes the derived value analysis in RC insertion recognize
`Array.uget` as another kind of
"projection-like" operation. This allows it to reduce reference count
pressure on elements accessed
through uget.
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 `Subarray.foldl(M)`, `Subarray.toArray` and
`Subarray.size` in favor of the `Std.Slice`-namespaced operations. Dot
notation will continue to work. If, say, `Subarray.size` is explicitly
referred to, an error suggesting to use `Std.Slice.size` will show up.
This PR adds a system-wide Lake configuration file and uses it to
configure the remote cache services used by `lake cache`.
The system configuration is written in TOML. The exact location of the
file is system dependent and can be controlled via the `LAKE_CONFIG`
environment variable, but is usually located at `~/.lake/config.toml`.
As an example, one can configure a custom S3 cache service like so:
**~/.lake/config.toml**
```toml
cache.defaultService = "my-s3"
cache.defaultUploadService = "my-s3"
[[cache.service]]
name = "my-s3"
kind = "s3"
artifactEndpoint = "https://my-s3.com/a0"
revisionEndpoint = "https://my-s3.com/r0"
```
If no `cache.defaultService` is configured, Lake will use Reservoir for
downloads by default. A Reservoir mirror (or Reservoir-like service) can
be configured using `kind = "reservoir"` and setting an `apiEndpoint`. A
list of configured cache service (one name per line) can be obtained via
`lake cache services`.
This PR is part 2 of the `implicit_reducible` refactoring (part 1:
#12567).
**Background.** When Lean checks definitional equality of function
applications
`f a₁ ... aₙ =?= f b₁ ... bₙ`, it compares arguments `aᵢ =?= bᵢ` at a
transparency level determined by the binder type. Previously, only
instance-implicit (`[C]`) arguments received a transparency bump to
`.instances`. With `backward.isDefEq.implicitBump` enabled, ALL implicit
arguments (`{x}`, `⦃x⦄`, and `[x]`) are bumped to `.instances`, so that
definitions marked `[implicit_reducible]` unfold when comparing implicit
arguments. This is important because implicit arguments often carry type
information (e.g., `P (i + 0)` vs `P i`) where the mismatch is in
non-proof positions (Sort arguments to `cast`) — proof irrelevance does
not
help here, so the relevant definitions must actually unfold.
**`[implicit_reducible]`** (renamed from `[instance_reducible]` in part
1) marks
definitions that should unfold at `TransparencyMode.instances` — between
`[reducible]` (unfolds at `.reducible` and above) and the default
`[semireducible]` (unfolds only at `.default` and above). This is the
right
level for core arithmetic operations that appear in type indices.
## Changes
- **Enable `backward.isDefEq.implicitBump` by default** and set it in
`stage0/src/stdlib_flags.h` so stage0 also compiles with it
- **Mark `Nat.add`, `Nat.mul`, `Nat.sub`, `Array.size` as
`[implicit_reducible]`**
so they unfold when comparing implicit arguments at `.instances`
transparency
- **Remove redundant unification hints** (`n + 0 =?= n`, `n - 0 =?= n`,
`n * 0 =?= 0`) that are now handled by `[implicit_reducible]`
- **Rename all remaining `[instance_reducible]` attribute usages** to
`[implicit_reducible]` across the codebase (the old name remains as an
alias)
- **Remove 28 `set_option backward.isDefEq.respectTransparency false
in`**
workarounds that are no longer needed
🤖 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 adds a warning when using `cbv` or `decide_cbv` in tactic mode,
matching the existing warning in conv mode
(`src/Lean/Elab/Tactic/Conv/Cbv.lean`). The warning informs users that
these tactics are experimental and still under development. It can be
disabled with `set_option cbv.warning false`.
Co-authored-by: Claude Opus 4.6 <noreply@anthropic.com>
This PR ports the RC insertion from IR to LCNF.
In doing so it makes the entire code monadic as opposed to simulating a
ReaderT StateRefT stack manually.
Cmake only builds cadical if it isn't already installed on the user's
system. However, it then force-updates the cache variable with the new
path to the built cadical binary, leading subsequent cmake calls to
believe cadical is already installed on the user's system.
This only becomes a problem when cmake is called more than once before
the first call to make, which apparently happens roughly never.
This PR adds an `Std.Do` spec lemma for `ForIn` over strings.
This spec lemma does not use the list cursor machinery used by other
spec lemmas, but instead is stated in terms of `String.Pos`, to be used
together with `String.Pos.Splits` (which is basically the same as the
list cursors, but specialized to strings).
This PR removes unnecessary `simp` call in `simpAppFn` in `cbv` tactic
and updates the usage of `cbv_eval` attribute in
`tests/lean.run/cbv1.lean` to follow the new syntax that does not
require an explicit name of the function for which we are registering
the unfold lemma.
This PR fixes a bug with rendering of hygiene info nodes in embedded
Verso code examples. The embedded anonymous identifier was being
rendered as [anonymous] instead of being omitted.
This PR improves the Sym VCGen such that we can use Sym.simp to unfold
definitions in the benchmark driver. To do so, it adds support for
zeta-reduction in the VCGen and ensures that proof terms are maximally
shared before being sent to the kernel.
This PR removes unnecessary `trySynthInstance ` in `ite` and `dite`
simprocs used by `cbv` that previously contributed to too much of
unnecessary unrolling by the tactic.
This PR fixes the release checklist to update the lean-toolchain to the
latest
nightly on newly created bump branches for all repositories, not just
batteries
and mathlib4. Previously cslib (and any future repos with `bump-branch:
true`)
would inherit the toolchain from main, causing nightly testing warnings
like
https://leanprover.zulipchat.com/#narrow/channel/428973-nightly-testing/topic/Cslib.20status.20updates/near/574648029🤖 Prepared with Claude Code
Co-authored-by: Claude Opus 4.6 <noreply@anthropic.com>
This PR fixes#12554 where the `cbv` tactic throws "unexpected kernel
projection term during structural definitional equality" when a rewrite
theorem's pattern contains a lambda and the expression being matched has
a `.proj` (kernel projection) at the corresponding position.
The `Sym` pattern matching infrastructure (`isDefEqMain` in
`Pattern.lean`) does not handle `.proj` expressions and can throw an
exception. Rather than presenting it as an error in `cbv`, we fail
quietly and let the `cbv` tactic try other fallback paths.
---------
Co-authored-by: Claude Opus 4.6 <noreply@anthropic.com>
This PR inlines the accessor for the computed hash field of `Name`. This
ensures that accessing the
value is basically always just a single load instead of doing a full
function call.
This PR uses a `ptrEq` fast path for `Name.quickCmp`. It is particularly
effective at speeding up
`quickCmp` calls in `TreeMap`'s indexed by `FVarId` as usually there is
only one pointer per `FVarId`
so equality is always instantly detected without traversing the linked
list of `Name` components.
I had to use an `implemented_by` instead of just changing the definition
as lake proves things about
`quickCmp` for use in a `DTreeMap`.
This PR makes `computed_field` respect the inline attributes on the
function for computing the
field. This means we can inline the accessor for the field, allowing
quicker access.
This PR provides the necessary hooks for the new do elaborator to call
into the let and match elaborator.
The `do match` elaborator needs access to a couple of functions from the
term `match` elaborator to implement its own `elabMatchAlt`. In
particular, `withEqs`, `withPatternVars` and `checkNumPatterns` need to
be exposed. Furthermore, I think it makes sense to share
`instantiateAltLHSs`.
This PR adds `Sym.mkPatternFromDeclWithKey` to the Sym API to generalize
and implement `Sym.mkEqPatternFromDecl`. This is useful to implement
custom rewrite-like tactics that want to use `Pattern`s for
discrimination tree lookup.
This PR improves universe level inference for the `inductive` and
`structure` commands to be more reliable and to produce better error
messages. Recall that the main constraint for inductive types is that if
`u` is the universe level for the type and `u > 0`, then each
constructor field's universe level `v` satisfies `v ≤ u`, where a
*constructor field* is an argument that is not one of the type's
*parameters* (recall: the type's parameters are a prefix of the
parameters shared by the type former and all the constructors). Given
this constraint, the `inductive` elaborator attempts to find reasonable
assignments to metavariables that may be present:
- For the universe level `u`, choosing an assignment that makes this
level least is reasonable, provided it is unique.
- For constructor fields, choosing the unique assignment is usually
reasonable.
- For the type's parameters, promoting level metavariables to new
universe level parameters is reasonable.
The order of these steps led to somewhat convoluted error messages; for
example, metavariable->parameter promotion was done early, leading to
errors mentioning `u_1`, `u_2`, etc. instead of metavariables, as well
as extraneous level constraint errors. Furthermore, early parameter
promotion meant it was too late to perform certain kinds of inferences.
Now there is a straightforward order of inference:
1. If the type's universe level could be zero, it checks that the type
is an "obvious `Prop` candidate", which means it's non-recursive, has
one constructor with at least one field, and all the fields are proofs.
If it's a `Prop` candidate, the level is set to zero and we skip to step
4.
2. If the type's simplified universe level is of the form `?u + k`, it
will accumulate level constraints to find a least upper bound solution
for `?u`. To avoid sort polymorphism, it adds `1 ≤ ?u + k`, ensuring the
result stays in `Type _`, or at least `Sort (max 1 _)`. It allows other
metavariables to appear in the assignment for `?u`, provided they appear
in the type former, or for `structure` in the `extends` clause.
3. If the type's simplified universe level is then of the form `r + k`,
where `r` is a parameter, metavariable, or zero, then for every
constructor field it will take the `v ≤ r + k` constraint and extract
`?v ≤ r + k'` constraints. It will also *weakly* extract `1 ≤ ?v`
constraints, using the observation that it's surprising if fields are
automatically inferred to be proofs. Once the constraints are collected,
each metavariable is solved for independently. Heuristically, if there
is a unique non-constant solution we take that, or else a unique
constant solution.
4. Any remaining level metavariables in the type former (or `extends`
clause) become level parameters.
5. Remaining level metavariables in the constructor fields are reported
as errors.
6. Then, the elaborator checks that the level constraints actually hold
and reports an error if they don't.
In 2 and 3, there are procedures to simplify universe levels. You can
write `Sort (max 1 _)` for the resulting type now and it will solve for
`_`.
The "accidentally higher universe" error is now a warning. The
constraint solving is also done in a more careful way, which keeps it
from being reported erroneously. There are still some erroneous reports,
but these ones are hard for the checker to reject. As before, the
warning can be turned off by giving an explicit universe.
Note about `extends` clauses: in testing, there were examples where it
was surprising if the universe polymorphism of parent structures didn't
carry over to the type being defined, even though parent structures are
actually constructor fields.
**Breaking change.** Universe level metavariables present only in
constructor fields are no longer promoted to be universe level
parameters: use explicit universe level parameters. This promotion was
inconsistently done depending on whether the inductive type's universe
level had a metavariable, and also it caused confusion for users, since
these universe levels are not constrained by the type former's
parameters.
**Breaking change.** Now recursive types do not count as "obvious `Prop`
candidates". Use an explicit `Prop` type former annotation on recursive
inductive predicates.
Additional changes:
- level metavariable errors are now localized to constructors, and
`structure` fields have such errors localized to fields
- adds module docs for the index promotion algorithm and the universe
level inference algorithm for inductives
- factors out `Lean.Elab.Term.forEachExprWithExposedLevelMVars` for
printing out the context of an expression with universe level
metavariables
- makes universe level metavariable exposure more effective at exposing
level metavariables (with an exception of `sorry` terms, which are too
noisy to expose)
Supersedes #11513 and #11524.
This PR removes `tryMatchEquations` and `tryMatcher` from
`Lean.Meta.Tactic.Cbv.Main`, as both are already defined and used in
`Lean.Meta.Tactic.Cbv.ControlFlow`. The copies in `Main.lean` were
unreachable dead code.
🤖 Generated with [Claude Code](https://claude.com/claude-code)
Co-authored-by: Claude Opus 4.6 <noreply@anthropic.com>
This PR renames `instance_reducible` to `implicit_reducible` and adds a
new
`backward.isDefEq.implicitBump` option to prepare for treating all
implicit
arguments uniformly during definitional equality checking.
## Changes
**Rename `instance_reducible` → `implicit_reducible`:**
- Rename `ReducibilityStatus.instanceReducible` constructor to
`implicitReducible`
- Register new `[implicit_reducible]` attribute, keep
`[instance_reducible]` as alias
- Rename `isInstanceReducible` → `isImplicitReducible` (with deprecated
aliases)
- Update all references across src/ and tests/
The rename reflects that this reducibility level is used not just for
instances
but for any definition that needs unfolding during implicit argument
resolution
(e.g., `Nat.add`, `Array.size`).
**Add `backward.isDefEq.implicitBump` option:**
- When `true` (+ `respectTransparency`), bumps transparency to
`.instances` for
ALL implicit arguments in `isDefEqArgs`, not just instance-implicit ones
- Defaults to `false` for staging compatibility — will be flipped to
`true` after
stage0 update
- Adds `// update me!` to `stage0/src/stdlib_flags.h` to trigger CI
stage0 update
## Follow-up (after stage0 update)
- Flip `backward.isDefEq.implicitBump` default to `true`
- Fix resulting test/module failures
🤖 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>
## Summary
This PR adds documentation comments to the key transparency-related
definitions explaining the design rationale behind the transparency
hierarchy and the v4.29 changes:
- `TransparencyMode`: explains "try-hard" vs "speculative" `isDefEq`,
the transparency hierarchy (`none < reducible < instances < default <
all`), instance diamonds, and why implicit arguments received special
treatment
- `ReducibilityStatus`: documents each status with its corresponding
`TransparencyMode` level and typical use case
- `@[instance_reducible]`: explains decoupling of instance registration
from transparency
- `backward.isDefEq.respectTransparency`: explains the original
motivation for bumping transparency on implicit arguments, and why it
became a performance bottleneck
- `backward.whnf.reducibleClassField`: explains why `[reducible]` class
fields need special handling when the instance is only
`[instance_reducible]`
- `canUnfoldDefault` and `isDefEqArgs`: brief inline comments linking to
the design rationale
🤖 Generated with [Claude Code](https://claude.com/claude-code)
---------
Co-authored-by: Claude Opus 4.6 <noreply@anthropic.com>
This PR fixes a `(kernel) declaration has metavariables` error that
occurred when a `by` tactic was used in a dependent inductive type index
that refers to a previous index:
```lean
axiom P : Prop
axiom Q : P → Prop
-- Previously gave: (kernel) declaration has metavariables 'Foo'
inductive Foo : (h : P) → (Q (by exact h)) → Prop
```
The root cause: `elabDepArrow` calls `mkForallFVars [h_fvar] body`
before the `by` tactic's metavariable `?m` is resolved. Since `h_fvar`
is in `?m`'s local context, `elimMVarDeps` creates a delayed assignment
`?newMVar #[h_fvar] := ?m`. After `synthesizeSyntheticMVarsNoPostponing`
assigns `?m := h_fvar`, `instantiateMVars` can resolve the delayed
assignment (substituting `h_fvar` with the actual argument, `bvar 0`, in
the pending value), yielding the correct type `∀ (h : P), Q (bvar 0) →
Prop`. The fix is to call `instantiateMVars` on the header type right
after `synthesizeSyntheticMVarsNoPostponing` in `elabHeadersAux`.
Fixes#12543.
🤖 This PR was created with [Claude Code](https://claude.ai/claude-code).
Co-authored-by: Claude Sonnet 4.6 <noreply@anthropic.com>
This PR fixes an issue where commands that do not support incrementality
did not have their elaboration interrupted when a relevant edit is made
by the user. As all built-in variants of def/theorem share a common
incremental elaborator, this likely had negligible impact on standard
Lean files but could affect other use cases heavily relying on custom
commands such as Verso.
This PR fixes a bug where Lake recached artifacts already present within
the cache. As a result, Lake would attempt to overwrite the read-only
artifacts, causing a permission denied error.
This PR adds guidance to `.claude/CLAUDE.md` about the `module` +
`prelude` convention required for files in `src/Lean/`, `src/Std/`, and
`src/lake/Lake/`. CI enforces that these files contain `prelude`, but
with `prelude` nothing is auto-imported, so explicit `Init.*` imports
are needed for standard library features like `while`,
`String.startsWith`, etc.
🤖 Prepared with Claude Code
Co-authored-by: Claude Opus 4.6 <noreply@anthropic.com>
