This PR adds `checkSystem` calls to the `bv_decide` tactic's main loops
to improve IDE cancellation responsiveness. Previously, `bv_decide` had
zero `checkSystem` calls in its entire codebase, meaning long-running
invocations could not be cancelled promptly.
Insertion points:
- `fixpointPipeline` (normalization fixpoint loop)
- `ReifiedBVExpr.of.go` (recursive BitVec expression reification)
- `ReifiedBVLogical.of.go` (recursive boolean expression reification)
- `reflectBV` (hypothesis loop)
These cover the MetaM-based phases of `bv_decide`. The pure computation
phases (bitblasting via `IO.lazyPure`, AIG→CNF conversion) remain
without checks and would require restructuring to address.
Gap measurements (at 6.0 Ginstr/s, using
`LEAN_CHECK_SYSTEM_INTERVAL_INSN` from #13212):
- `bv_decide_large_aig.lean`: before ~3.3s max gap (19,899M insn),
after: pure bitblast/AIG gaps remain but reification and normalization
phases are now interruptible
- Other bv_decide bench files: normalization and reification loops are
now responsive to cancellation
Note: the largest remaining gaps in bv_decide benchmarks are in the
kernel type checker (proof term checking, up to 10.5s on
`bv_decide_mod.lean`) and in pure bitblasting — both out of scope for
this PR.
Co-authored-by: Claude Opus 4.6 <noreply@anthropic.com>
This PR fixes a typo.
---
Additional comment:
I found the description hard to read (in part because the term "constant
function" is not one I encounter frequently enough, and because there is
no explicit constant function in the signature). Would you consider
changing the first sentence from "Mapping a constant function" to
"Replaces the value in a functor with a constant, retaining the
functor's structure" (based on Functor.discard)?
Also, I would write `(fun _ => a)` rather than `Function.const _ a`.
---------
Co-authored-by: Joachim Breitner <mail@joachim-breitner.de>
This PR marks any exposed (non-private) auxiliary match declaration as
`[implicit_reducible]`. This is essential when the outer declaration is
marked as `instance_reducible` — without it, reduction is blocked at the
match auxiliary. We do not inherit the attribute from the parent
declaration because match auxiliary declarations are reused across
definitions, and the reducibility setting of the parent can change
independently. This change prepares for implementing the TODO at
`ExprDefEq.lean:465`, which would otherwise cause too many failures
requiring manual `[implicit_reducible]` annotations on match
declarations whose names are not necessarily derived from the outer
function.
---------
Co-authored-by: Claude Opus 4.6 <noreply@anthropic.com>
This PR adds a new option `backward.isDefEq.respectTransparency.types`
that controls the transparency used when checking whether the type of a
metavariable matches the type of the term being assigned to it during
`checkTypesAndAssign`. Previously, this check always bumped transparency
to `.default` (via `withInferTypeConfig`), which is overly permissive.
The new option uses `.instances` transparency instead (via
`withImplicitConfig`), matching the behavior already used for implicit
arguments.
The option defaults to `false` (preserving old behavior) until stage0 is
updated and breakage is assessed. If
`backward.isDefEq.respectTransparency` (already in v4.29) is set to
`false`, then `backward.isDefEq.respectTransparency.types` is
automatically treated as `false` too.
When `diagnostics` is enabled, a trace message is emitted if the
stricter transparency fails but `.default` would have succeeded, helping
identify affected code. To investigate failures when enabling
`backward.isDefEq.respectTransparency.types`, use:
```
set_option diagnostics true
set_option trace.diagnostics true
```
Also renames `withInstanceConfig` to `withImplicitConfig` since it now
serves implicit argument and type checking, not just instances.
Registers the `diagnostics` trace class in `CoreM`.
Co-authored-by: Claude Opus 4.6 <noreply@anthropic.com>
This PR adds a comprehensive public API for constructing maximally
shared
expression applications and performing beta reduction in the `Sym`
framework.
These functions were previously defined locally in the VC generator and
cbv
tactic, and are needed by downstream `SymM`-based tools.
New functions in `Lean.Meta.Sym.Internal` (generic over
`MonadShareCommon`):
- `mkAppS₆` through `mkAppS₁₁` (higher-arity application builders)
- `mkAppRangeS`, `mkAppNS` (forward application over arrays/ranges)
- `mkAppRevRangeS`, `mkAppRevS` (reversed application over
arrays/ranges)
New public functions in `Lean.Meta.Sym` (`SymM`):
- `betaRevS` and `betaS` (beta reduction with max sharing)
- `mkForallFVarsS` (forall abstraction with max sharing)
The `AlphaShareBuilderM`-specific `mkAppRevRangeS` in
`InstantiateS.lean` is
replaced by the generic version from `Internal`, and the internal
`betaRevS`
is renamed to `betaRevS'`. The `Cbv.mkAppNS` now delegates to
`Internal.mkAppNS`.
---------
Co-authored-by: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
This PR extends the sym canonicalizer to apply reductions (projection,
match/ite/cond, Nat
arithmetic) in all positions, not just inside types. Previously, a value
`v` appearing in a
type `T(v)` could remain unreduced while `T(v)` was normalized, breaking
the invariant that
definitionally equal types are structurally identical after
canonicalization.
Changes:
- Remove `insideType` guards from `canonApp` and `canonProj`, so
reductions apply unconditionally
(eta reduction remains type-only, to preserve lambda structure for
`grind`)
- Add `canonInstDecCore` to handle `Decidable` instances in
`if-then-else` expressions, dispatching
`Grind.nestedDecidable` to `canonInstDec` and falling back silently for
other instances
- Add `report` parameter to `canonInstCore`/`canonInst'`/`canonInst` to
allow suppressing issue
reporting for propositional and decidable instances that cannot be
resynthesized (common with
`haveI`-provided instances that propagate into types through forward
dependencies)
- Update module documentation to reflect the new reduction scope and the
`haveI` reporting tradeoff
Co-authored-by: Claude Opus 4.6 <noreply@anthropic.com>
This PR refactors instance canonicalization in the sym canonicalizer to
properly handle
\`Grind.nestedProof\` and \`Grind.nestedDecidable\` markers. Previously,
the canonicalizer
would report an issue when it failed to resynthesize propositional
instances that were
provided by \`grind\` itself or by the user via \`haveI\`. Now,
resynthesis failure gracefully
falls back to the original instance in value positions, while remaining
strict inside types.
Changes:
- Extract \`canonInstCore\` as the shared resynthesis + defEq-check
logic
- Add \`canonInstProp\` for \`Grind.nestedProof\`: canonicalize the
proposition, attempt resynthesis, fall back silently (proof irrelevance
means no defEq check needed)
- Add \`canonInstDec\`/\`canonInstDec'\` for \`Grind.nestedDecidable\`:
canonicalize the proposition, attempt resynthesis with defEq guard, fall
back silently
- Remove the separate \`cacheInsts\` cache in favor of the existing
type/value caches via \`withCaching\`
- Update module-level documentation
Co-authored-by: Claude Opus 4.6 <noreply@anthropic.com>
This PR verifies the `String.dropWhile` and `String.takeWhile`
functions.
It also includes a refactor of the `PatternModel` class so that the
`not_matches_empty` condition is moved into a separate typeclass
`StrictPatternModel`. This allows string patterns to implement
`LawfulForwardPatternModel` unconditionally, which means that more of
the general theory about patterns directly applies to string patterns
without having to do a case distinction for empty strings.
This PR also includes a study of the `PatternModel` machinery given to
slices `s` and `t` such that `s.copy = t.copy`. From these results, we
deduce statements like `s.copy.startsWith pat = s.startsWith pat` (which
is far from obvious!).
This PR changes the counter-example accumulator in the match compiler
from
a `List` (built with cons, producing reverse order) to an `Array` (built
with push, preserving declaration order). Missing cases are now reported
in
the order constructors appear in the inductive type definition.
For example, given `inductive Enum | a | b | c | d`, missing cases `c`
and
`d` were previously shown as `d, c` and are now shown as `c, d`.
Co-authored-by: Claude Opus 4.6 <noreply@anthropic.com>
privateConstantMap capacity was inflated by IR extraConstNames that are
only inserted into const2ModIdx. const2ModIdx capacity included
numPublicConsts even though public constants are never inserted into it.
This PR adds a `match.maxCounterExamples` option (default 5) to bound
the
number of "missing cases" counter-examples the match compiler generates.
When the match compiler runs out of alternatives for a variable, it
case-splits to explore missing cases. Previously, this would recursively
split all inductive-typed fields of each constructor, leading to
O(K^fields)
counter-examples for types with K constructors per field. For nested
incomplete matches on types like `Op w` (20 constructors with `Operand
w`
fields having 8 constructors each), this produced thousands of
counter-examples and took several seconds.
The fix checks the counter-example count in `isConstructorTransition`:
once
the limit is reached and there are no remaining alternatives, the match
compiler stops exploring further case splits. The error message notes
when
output has been truncated and names the option. The existing protection
against infinite recursion on recursive types is preserved.
Co-authored-by: Claude Opus 4.6 <noreply@anthropic.com>
This PR adds a `Core.checkInterrupted` call in `checkInferTypeCache` on
cache miss, allowing cancellation to be detected during large type
inference traversals. Previously, `inferTypeImp` could run for >100ms
without any interruption check when processing large expressions (e.g.
BVDecide proof terms), making IDE cancellation unresponsive.
The check is only on cache miss (actual computation), so cache hits have
zero overhead. `checkInterrupted` is used instead of the heavier
`checkSystem` to minimize performance impact — local benchmarks show no
measurable regression on `tests/elab/5664.lean`.
🤖 Generated with [Claude Code](https://claude.com/claude-code)
Co-authored-by: Claude Opus 4.6 <noreply@anthropic.com>
This PR changes elaboration of structure instance notation when used in
patterns (e.g. `s matches { x := 1, y := [] }`) so that the structure's
default values are not used to elaborate the pattern. The motivation is
that default values frequently lead to surprisingly over-specific
patterns. It will now report "field missing" errors. The error can be
suppressed using `{ x := 1, .. }` ellipsis notation, which has the same
behavior as before. The pretty printer is also modified to stay in sync
with this feature. **Breaking change:** patterns using structure
instance notation may need missing fields or a `..` added, as
appropriate.
The rationale for the previous behavior is that with `..` you could
opt-in to not using default values, and now with this PR's behavior you
cannot opt-in. However, default values in structure instance patterns
are very likely to silently cause bugs. There are a couple examples in
this PR of unintentional default values in patterns in core Lean
(luckily these were not triggering bugs). With the new behavior, you can
now tell for sure whether every explicit field in a structure is being
matched explicitly or not, by the absence or presence of `..`.
Closes#10753
This PR adds support for marking options as deprecated. When a
deprecated option is used via `set_option`, a warning is emitted
(controlled by `linter.deprecated.options`).
An `OptionDeprecation` structure with a required `since` field and an
optional `text?` field is added to `OptionDecl`. Each `set_option`
elaborator (command, term, tactic, grind) calls `checkDeprecatedOption`
to emit warnings. The C++ `register_option` is updated to account for
the new field.
As a first use, `backward.eqns.nonrecursive` and
`backward.eqns.deepRecursiveSplit` are marked deprecated. Continues
earlier work done in #11096.
This PR adds test infrastructure and tests for tactic completion in
empty `by` blocks.
**Test runner improvements (`src/Lean/Server/Test/Runner.lean`):**
- Add `--⬑` marker variant that targets the column of `--` itself,
enabling column 0 tests (which `--^` cannot reach since `^` is always at
column 2+).
**New test file (`tests/server_interactive/completionEmptyBy.lean`):**
- Tests tactic completion in empty `by` blocks for both top-level `by`
and nested `by` (inside `id <| have := by`).
- Tests at various column positions on the line below `by`: indented
past `by`, at column 2, and at column 0.
- Tests on the `by` token itself (no completions expected).
- All positions below `by` currently offer tactic completions.
🤖 Generated with [Claude Code](https://claude.com/claude-code)
---------
Co-authored-by: Claude Opus 4.6 <noreply@anthropic.com>
This PR adds support for let configuration options (`(eq := h)`,
`+nondep`, `+usedOnly`, `+zeta`) in `do` block `let` and `have`
declarations, matching the behavior available in term-level
`let`/`have`. Configuration options are rejected with `let mut` since
they are incompatible with mutable bindings. `+postponeValue` and
`+generalize` are also rejected in `do` blocks.
Follow-up to #13250 which added the parser support. Now that stage0 is
updated, this PR replaces the backward-compat index helpers with proper
quotation patterns and implements the actual `letConfig` elaboration.
🤖 Generated with [Claude Code](https://claude.com/claude-code)
Co-authored-by: Claude Opus 4.6 <noreply@anthropic.com>
This PR extends the `doLet`, `doLetElse`, `doLetArrow`, and `doHave`
parsers to accept `letConfig` (e.g. `(eq := h)`, `+nondep`, `+usedOnly`,
`+zeta`), matching the syntax of term-level `let`/`have`. The
elaborators are adjusted to handle the shifted syntax indices but do not
yet process the configuration; that will be done in a follow-up PR after
stage0 is updated, allowing the use of proper quotation patterns.
🤖 Generated with [Claude Code](https://claude.com/claude-code)
---------
Co-authored-by: Claude Opus 4.6 <noreply@anthropic.com>
This PR removes a FIXME in Sym-based mvcgen' concerning a hardcoded step
limit for grind simplification. I tested that this is no longer
necessary even at highest setting for the GetThrowSetGrind benchmark.
This PR extends Lean syntax for dotted function notation (`.f`) to add
support for explicit mode (`@.f`), explicit universes (`.f.{u,v}`), and
both simultaneously (`@.f.{u,v}`). This also includes a fix for a bug
involving overloaded functions, where it used to give erroneous
deprecation warnings about declarations that the function did not
elaborate to.
Closes#10984
This PR improves pretty printing of level metavariables: they now print
with a per-definition index rather than their per-module internal
identifiers. Furthermore, `+` is printed uniformly in level expressions
with surrounding spaces. **Breaking metaprogramming change:** level
pretty printing should use `delabLevel` or `MessageData.ofLevel`;
functions such as `format` or `toString` do not have access to the
indices, since they are stored in the current metacontext. Absent index
information, metavariables print with the raw internal identifier as
`?_mvar.nnn`. **Note:** The heartbeat counter also increases quicker due
to counting allocations that record level metavariable indices. In some
tests we needed to increase `maxHeartbeats` by 20–50% to compensate,
without a corresponding slowdown.
This PR fixes a panic when compiling mutually recursive definitions that
use `casesOn` on indexed inductive types (e.g. `Vect`). The
`splitMatchOrCasesOn` function in `WF.Unfold` asserted
`matcherInfo.numDiscrs = 1`, but for indexed types the casesOn recursor
has multiple discriminants (indices + major premise). The fix uses the
last discriminant (the major premise) and lets the `cases` tactic handle
index discriminants automatically.
Closes#13015
Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
Co-authored-by: Claude Opus 4.6 <noreply@anthropic.com>
This PR adds a `deprecated_module` command that marks the current module
as deprecated. When another module imports a deprecated module, a
warning is emitted during elaboration suggesting replacement imports.
Example usage:
```lean
deprecated_module "use NewModule instead" (since := "2026-03-30")
```
The warning message is optional but recommended. The `since` parameter
is required. Warnings can be disabled, by setting
`linter.deprecated.module` option to false in the command line. Because
the check happens when importing , using `set_option
linter.deprecated.module` in the source file won't affect the warnings.
Instead, a whole file can be marked not to display depreciation
warnings, by putting a comment `deprecated_module: ignore` next to
`module` keyword. Similarly, individual keywords can be silenced.
A `#show_deprecated_modules` command is also provided for inspecting
which modules in the current environment are deprecated.
`linter.deprecated.module` has no effect on this command, and hence one
can view deprecated modules, even when having warnings silenced.
This PR fixes `FirstTokens.seq (.optTokens s) .unknown` to return
`.unknown`. This occurs e.g. when an optional (with first tokens
`.optTokens s`) is followed by a parser category (with first tokens
`.unknown`). Previously `FirstTokens.seq` returned `.optTokens s`,
ignoring the fact that the optional may be empty and then the parser
category may have any first token. The correct behavior here is to
return `.unknown`, which indicates that the first token may be anything.
Closes#13203
This PR adds `checkSystem` calls to several code paths that can run for
extended periods without checking for cancellation, heartbeat limits, or
stack overflow. This improves responsiveness of the cancellation
mechanism
in the language server.
Affected paths:
- `simpLoop` step loop (`Simp/Main.lean`)
- `simp` rewrite candidate loops (`Rewrite.lean`)
- `simpAppUsingCongr` argument traversal (`Types.lean`)
- `synthesizeSyntheticMVarsStep` mvar loop (`SyntheticMVars.lean`)
- `abstractNestedProofs` visitor (`AbstractNestedProofs.lean`)
- `transform`/`transformWithCache` visitors (`Transform.lean`)
- LCNF compiler pass runner loop (`LCNF/Main.lean`)
- LCNF checker recursive traversal (`LCNF/Check.lean`)
- `whnfImp` top-level reduction (`WHNF.lean`)
Intentionally *not* instrumented (too hot, measurable regression):
- `whnfCore.go` inner recursion
- `simpImpl` entry point (redundant with `simpLoop`)
- LCNF `simp` inner recursion (0.4% regression on `big_do`)
Also adds a docstring to `checkInterrupted` clarifying its relationship
to
`checkSystem`.
Found using `LEAN_CHECK_SYSTEM_INTERVAL_MS` monitoring from #13218.
Co-authored-by: Claude Opus 4.6 <noreply@anthropic.com>
This PR adds a `deprecated_syntax` command that marks syntax kinds as
deprecated. When deprecated syntax is elaborated (in terms, tactics, or
commands), a linter warning is emitted. The warning is also emitted
during quotation precheck when a macro definition uses deprecated syntax
in its expansion.
The `deprecated_syntax` command takes a syntax node kind, an optional
message, and a `(since := "...")` clause. Deprecation warnings correctly
attribute the warning to macro call sites when the deprecated syntax is
produced by macro expansion, including through nested macro chains.
---------
Co-authored-by: Sebastian Ullrich <sebasti@nullri.ch>
This PR adds an `unlock_limits` command that sets `maxHeartbeats`,
`maxRecDepth`, and `synthInstance.maxHeartbeats` to 0, disabling all
core resource limits. Also makes `maxRecDepth 0` mean "no limit"
(matching the existing behavior of `maxHeartbeats 0`).
This PR updates `release_checklist.py` to handle the `CACHE STRING ""`
suffix on CMake version variables. The `CACHE STRING` format was
introduced in the `releases/v4.30.0` branch, but the script's parsing
wasn't updated to match, causing false failures.
🤖 Prepared with Claude Code
---------
Co-authored-by: Claude Opus 4.6 <noreply@anthropic.com>
This PR adds two safety notes to the Claude Code release command:
- Mathlib bump branches live on `mathlib4-nightly-testing`, not the main
`mathlib4` repo
- Never force-update remote refs without explicit user confirmation
🤖 Prepared with Claude Code
Co-authored-by: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
This PR moves `hasAssignableMVar`, `hasAssignableLevelMVar`, and
`isLevelMVarAssignable` from `MetavarContext.lean` to a new
`Lean.Meta.HasAssignableMVar` module, changing them from generic `[Monad
m] [MonadMCtx m]` functions to `MetaM` functions. This enables adding
`checkSystem` calls in the recursive traversal, which ensures
cancellation and heartbeat checks happen during what can be a very
expensive computation.
All callers of these functions were already in `MetaM`, so this change
is safe. The motivating case is the `4595_slowdown.lean` test, where
`hasAssignableMVar` (with `PersistentHashMap.find?` lookups on
`mctx.lDepth`) was the dominant CPU cost during elaboration of category
theory definitions. Without `checkSystem` calls, cancellation requests
could be delayed by over 2 seconds.
The test file `4595_slowdown.lean` gets a slightly increased
`maxHeartbeats` limit because `checkSystem` now detects heartbeat
exhaustion mid-traversal rather than after the function returns.
Co-authored-by: Claude Opus 4.6 <noreply@anthropic.com>
This commit ensures binaries are only stripped in the `release` build
preset, not in any of the other presets.
Since `release` is used for development, the commit adds a non-stripping
copy called `dev` that can be used via `cmake --preset dev`.
This PR fixes the Windows dev build by using
`CMAKE_RELATIVE_LIBRARY_OUTPUT_DIRECTORY` instead of the hardcoded
`lib/lean` path for the Lake plugin. On Windows, DLLs must be placed
next to executables in `bin/`, but the plugin path was hardcoded to
`lib/lean`, causing stage0 DLLs to not be found.
The `CMAKE_RELATIVE_LIBRARY_OUTPUT_DIRECTORY` variable was introduced
precisely for this purpose — it resolves to `bin` on Windows and
`lib/lean` elsewhere.
Closes#13126🤖 Prepared with Claude Code
Co-authored-by: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
Co-authored-by: Sebastian Ullrich <sebasti@nullri.ch>
This PR replaces eager let-expression zeta-reduction in the sym-based
mvcgen with on-demand unfolding that mirrors the production mvcgen's
behavior.
Previously, all let-expressions in the program head were immediately
zeta-reduced. Now, let-expressions are hoisted to the top of the goal
target, and the value is only inlined if it is duplicable (literals,
fvars, consts, `OfNat.ofNat`). Complex values are introduced into the
local context via `introsSimp`, preserving SymM's maximal sharing
invariants, and unfolded on demand when the fvar later appears as the
program head.
---------
Co-authored-by: Claude Opus 4.6 <noreply@anthropic.com>
This PR fixes several issues in `Init.Data.String`, most of them typos.
We also move the remaining material out of `Init.Data.String.Lemmas` to
`Init.Data.String.Lemmas.StringOrder`, which shortens the pole.
This PR extends the `missingDocs` linter to detect and warn about empty
doc strings (e.g. `/---/` or `/-- -/`), in addition to missing doc
strings. Previously, an empty doc comment would silence the linter even
though it provides no documentation value. Now empty doc strings produce
a distinct "empty doc string for ..." warning, while `@[inherit_doc]`
still suppresses warnings as before.
This PR switches the mvcgen worklist from BFS (queue) to DFS (stack)
ordering for subgoal processing.
With the new do elaborator, `if`-without-`else` generates asymmetric
bind depth between branches (`pure () >>= cont` is optimized to just
`cont` in the else branch). This caused BFS-based VC numbering to depend
on elaborator internals, swapping vc10/vc11 in test cases. DFS ordering
follows the syntactic program structure more naturally and is robust to
such bind-depth asymmetries.
---------
Co-authored-by: Claude Opus 4.6 <noreply@anthropic.com>
