This PR adds the option `grind.ematch.diagnostics`, which tracks how
E-matching theorem instances depend on each other. When enabled, `grind`
records, for every new theorem instance, the set of previous instances
whose generated terms participated in the match. This produces a
hyper-graph `{thm_1, ..., thm_n} => thm` describing the provenance of
each instantiation.
The hyper-graph is stored in `Grind.Result` so downstream tooling can
inspect it. The trace class `trace.grind.ematch.diagnostics.compact`
prints a compact textual view of the hyper-graph, restricted to
constant-name origins. Example output:
```
[grind.ematch.diagnostics.compact] ✅️ instances
[inst] [] => th1
[inst] [th1] => th3
[inst] [th1] => th2
[inst] [th2, th3] => th4
[inst] [th4] => th5
```
The implementation stores an `ematchDiagSource` field on each `ENode`
and threads a `withEmatchDiagSource` reader through fact assertion so
that newly internalized terms inherit the origin of the instance that
produced them. During E-matching, `Choice` collects the sources of every
matched argument, and the resulting set becomes the predecessor set of
the new instance.
This PR addresses two review points on `IO.CancelToken`:
* `set` now resolves the underlying promise *before* writing the `Bool`
fast-path flag, so observing `isSet = true` implies any synchronously
chained `onSet` callback has already run. The previous order (flag
first,
then resolve) was a subtle footgun: code seeing `isSet = true` could not
rely on the cancellation task having fired.
* The underlying promise and the task it produces are kept private. The
prior `task : Task (Option Unit)` accessor is removed; consumers should
use `onSet` to react to cancellation. A comment on the structure records
that re-exposing the task in the future requires re-auditing the order
in `set` for races between the promise and the `Bool` flag.
Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
Co-authored-by: Claude Opus 4.7 <noreply@anthropic.com>
This PR fixes a bug in `propagateBetaEqs` (in
`Lean.Meta.Tactic.Grind.Beta`)
where new equalities/terms introduced by beta reduction were added to
the goal
without checking the generation threshold. The generation of the new
fact
is the maximum generation of the lambda, the function `f`, and its
arguments, plus one. Without the threshold check, beta reduction can
cascade indefinitely on self-similar lambdas such as
`(fun b => f (b + 1)) = fun b => f b`, which kept producing
`f n = f (n + 1)` for every `n`. The fix aggregates argument generations
before the threshold check and bails out when the resulting generation
reaches `maxGeneration`.
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 extends `lake lint --builtin-lint` to also support text linters
(i.e. those using `logLint`/`logLintIf`), in addition to the environment
linters added in #13431. Text-linter warnings emitted during the build
are persisted into each module's `.olean` via a new
`Lean.Linter.lintLogExt` environment extension; `lake lint` re-runs the
build for the target modules and reads the entries back, reporting them
alongside the environment linter output.
---------
Co-authored-by: Mac Malone <tydeu@hatpress.net>
Co-authored-by: Thomas R. Murrills <68410468+thorimur@users.noreply.github.com>
This PR adds a `try? => tac` syntax that runs `evalSuggest` directly on
a given tactic, useful for testing the `try?` machinery in isolation. It
also adds a server_interactive test (`cancellation_par.lean`) that
demonstrates a cancellation bug with parallel tactic combinators.
The test contrasts three combinators:
- **`first`** (sequential): cancellation works correctly — the tactic
runs on the main elaboration thread and shares its cancel token.
- **`attempt_all_par`** (parallel): cancellation is broken — the subtask
spawned via `asTask` gets a fresh cancel token that is never set on
re-elaboration.
- **`first_par`** (parallel): same bug as `attempt_all_par`.
The test uses a `check_cancel <label>` helper tactic that detects leaked
cancel tokens without any timing dependency: the second invocation (from
re-elaboration) signals the first, which then checks whether its cancel
token was set.
Related issue: #13300
---------
Co-authored-by: Claude Opus 4.6 <noreply@anthropic.com>
This PR replaces the catch-all "unsupported pattern in syntax match"
error that the new `do` elaborator produces for typical pattern mistakes
(#2215, #8304, #10393) with the proper diagnostics from the regular
pattern-var collector (e.g. "Invalid pattern: Expected a constructor or
constant marked with `[match_pattern]`", "ambiguous pattern, use fully
qualified name"), pointing at the offending pattern.
`getPatternVarsEx` / `getPatternsVarsEx` in `Lean.Elab.Do` now try the
syntax-quotation collector first (cheaply handling identifiers, holes,
and antiquotations) and fall back to the regular pattern-var collector
for everything else. When both fail, the regular collector's error wins
via `<|>` semantics.
The legacy `do` elaborator is intentionally left untouched, so the
existing `tests/elab/doSyntaxPatternError.lean` guards (which capture
the cryptic messages produced under legacy default) are unchanged. They
will need updating when the new `do` elaborator becomes default.
Fixes#2215, #8304, and #10393 for the new `do` elaborator.
This PR adds a `linter.redundantExpose` option (default `true`) that
warns when `@[expose]` or `@[no_expose]` attributes have no effect:
- `@[expose]` on `abbrev` (always exposed) or non-Prop `instance`
(always exposed)
- `@[expose]` on a `def` inside an `@[expose] section` (already exposed
by the section)
- `@[expose]`/`@[no_expose]` in a non-`module` file (no module system)
- `@[no_expose]` on a declaration that wouldn't be exposed by default
---------
Co-authored-by: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
This PR introduces stricter inference for the `@[defeq]` attribute and a
companion `@[backward_defeq]` attribute that preserves the pre-PR
behavior
as an opt-in.
### What changed
* `@[defeq]` is now inferred only when the equation holds at
`.instances` transparency (the transparency `dsimp` operates at).
* `@[backward_defeq]` is the old set: every theorem whose `rfl` proof
the legacy inference would have accepted is tagged `@[backward_defeq]`,
so `defeq ⊆ backward_defeq` holds by construction.
* The option `backward.defeqAttrib.useBackward` (default `false`) makes
`dsimp` also use `@[backward_defeq]` theorems, restoring the pre-PR
behavior for a specific proof or file.
* The option is eqn-affecting: its value at the point of a function's
definition is recorded so that the equation lemmas later generated for
that function use the same value, regardless of the ambient option at
the use site.
### Mathlib adaption
A companion adaption branch (`lean-pr-testing-backward-defeq-attrib` on
mathlib4) builds cleanly against this PR and passes `lake test` without
warnings. Most adaption changes are scoped
`set_option backward.defeqAttrib.useBackward true in` additions on the
failing declarations; a small number of files needed proof-level edits
where the stored form of a `dsimp%`/`@[reassoc]`/`@[elementwise]`
/`@[simps]`/`@[to_app]`-generated lemma had drifted under the stricter
regime.
---------
Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
This PR generalizes the `while` syntax in `do` blocks so that the
condition can be any `doIfCond`, the same condition form already
accepted by `if`. As a result, `while let pat := e do …` and `while let
pat ← e do …` are now supported in addition to `while cond do …` and
`while h : cond do …`. The previously separate `doWhile` and `doWhileH`
parsers and their accompanying macros are unified into a single
`doWhile` parser whose macro delegates to the existing `doIf`
desugaring.
This PR allows tactic macros and elaborators to opt out of automatic
fallback to previous macros/elabs on failure. `throwUnsupportedSyntax`
is unaffected.
This PR replaces the transparency bump from `.reducible` to `.instances`
in `whnfMatcher` with an explicit allowlist in `canUnfoldAtMatcher`.
Previously, `whnfMatcher` would unfold all `implicitReducible`
definitions and all `fromClass` projections when reducing match
discriminants. This made it impossible to mark definitions as
`implicit_reducible` without silently affecting match reduction
behavior.
The new `canUnfoldAtMatcher` delegates to `canUnfoldDefault` first
(respecting the ambient transparency), then allows unfolding of
`match_pattern`-attributed definitions, and finally checks an explicit
allowlist:
- `OfNat.ofNat` — numeric literals in match discriminants
- `NatCast.natCast` — `↑m` coercions (pervasive in Int proofs)
- `Zero.zero`, `One.one` — `0`/`1` class projections in match
discriminants
- `Fin.ofNat`, `HMod.hMod`, `Mod.mod` — Fin literal reduction
- `decEq`, `Nat.decEq` — decidable equality
- `Char.ofNat`, `Char.ofNatAux` — character literals
- `String.decEq`, `List.hasDecEq` — string/list equality
- `UInt{8,16,32,64}.{ofNat,decEq}` — unsigned integer literals and
equality
The key change is removing the blanket `implicitReducible` and
`fromClass` checks, so that marking definitions as `implicit_reducible`
no longer silently affects match reduction.
Additionally, `reduceMatcher?` and `reduceRecMatcher?` now call
`consumeMData` on their input to handle mdata-wrapped matcher
expressions.
Mathlib adaptation: the removal of the `fromClass` projection check
means class projections like `CategoryStruct.comp`, `CategoryStruct.id`,
`Min.min` etc. are no longer auto-unfolded in match discriminants.
Affected proofs add these projections explicitly to `simp`/`dsimp`
calls.
---------
Co-authored-by: Claude Opus 4.6 <noreply@anthropic.com>
This PR appends `unreachable!` to the expansion of `break`-less `repeat`
when the expected result type does not unify with `PUnit`. The
continuation then has a polymorphic value, so the enclosing do block's
result type is inferred without a user-written filler, and `ControlInfo`
for break-less `repeat` can report `noFallthrough` honestly — dead-code
warnings on subsequent elements are now actionable.
Co-authored-by: Rob23oba <robin.arnez@web.de>
This PR exposes the `Pure.pure` / `Bind.bind` applications emitted by
the `do` elaborator as pluggable closures, so external surface syntaxes
(e.g. an `ido` notation for indexed monads) can reuse the full `do`
machinery while emitting alternate constants.
`Context` carries a new `DoOps` record (wrapped via an opaque `DoOpsRef`
to break the cycle with `DoElabM`) with `mkPureApp`, `mkBindApp`, and
`isPureApp?` fields. `mkPureApp` and `mkBindApp` become thin
dispatchers; the original bodies move to `DoOps.default`. `isPureApp?`
returns the pure value as an `Expr` rather than a `Bool`, so overrides
aren't locked into `Pure.pure`'s 4-argument layout. A new `elabDoWith`
entry point takes a `DoOps` plus a `doSeq`; `elabDo` is now `elabDoWith
.default` applied to a matched ``(do $doSeq)``.
Control-flow features (`mut`, `return`, `break`, `continue`, `for`) and
the transformer stack (`StateT`, `OptionT`, `ExceptT`, `EarlyReturnT`,
`BreakT`, `ContinueT`) remain hard-coded to `Monad`; generalising them
is deferred to a follow-up. A new
`tests/elab/doNotationPluggableOps.lean` registers an Atkey-style
indexed monad and an `ido` surface syntax that drives `elabDoWith`,
covering the forms of `do` that are supported under the minimal scope.
This PR improves metavariable pretty printing and their hovers in the
InfoView. The hovers in the InfoView now include information about
specific metavariables — it includes information such as the kind of the
metavariable, whether it is a blocked delayed assignment and which
metavariables it is blocked on, and the differences in what variables
exist the metavariable's local context. Additionally, named
metavariables now pretty print with tombstones if they are inaccessible.
Delayed assignment pretty printing now more reliably follows chains of
assignments to find the pending metavariable.
**Example hovers**
Hovering over a natural metavariable:
> `?m.7 : Sort ?u.14`
> A metavariable representing an expression that should be solved for by
unification during the elaboration process. They are created during
elaboration as placeholders for implicit arguments and by `_`
placeholder syntax.
>
> Variables absent from this metavariable's local context: `a`, `b`, `y`
Hovering over `?baz`, a tactic goal:
> `?baz : ∀ (a : ?m.7) (a : ?m.8), True`
> A metavariable representing a tactic goal or an expression whose
elaboration is still pending. They usually act like constants until they
are completely solved for. They can be created using `?_` and `?n`
synthetic placeholder syntax.
>
> Variables absent from this metavariable's local context: `a`, `b`, `y`
Hovering over `?refine_1`, which appears under a binder:
> `?m.4 x : Nat`
> A metavariable representing a tactic goal or an expression whose
elaboration is still pending. They usually act like constants until they
are completely solved for. They can be created using `?_` and `?n`
synthetic placeholder syntax.
>
> This metavariable appears here via a *delayed assignment*.
Substitution is delayed until the metavariable's value contains no
metavariables, since all occurrences of the variables from its local
context will need to be replaced with expressions that are valid in the
current context.
>
> Additional variable in this metavariable's local context: `x`
Hovering over `?m.4`:
> `?m.4 : Nat → Nat`
> Part of the encoding of the *delayed assignment* mechanism. Represents
the metavariable `?refine_1`, which has additional local context
variables. Substitution is delayed until the metavariable's value
contains no metavariables, since all occurrences of the variables from
its local context will need to be replaced with expressions that are
valid in the current context.
>
> Additional variable in this metavariable's local context: `x`
The middle paragraph for `?refine_1` when it has been partially
assigned:
> This metavariable has been assigned, but it is a *delayed assignment*.
Substitution is delayed until the metavariable's value contains no
metavariables, since all occurrences of the variables from its local
context will need to be replaced with expressions that are valid in the
current context. Substitution is awaiting assignment of the following
metavariable: `?foo`
This PR adds builtin environment linting support to Lake, accessible via
`lake lint` flags. It also introduces two builtin linters upstreamed
from Mathlib (`defLemma` and `checkUnivs`) and a `builtinLint` package
configuration option.
Builtin linting is triggered via flags on `lake lint`:
- `--builtin-lint`: run default builtin linters (in addition to the lint
driver if configured)
- `--builtin-only`: run only builtin linters, skip the lint driver
- `--clippy`: run only non-default (clippy) linters
- `--lint-all`: run all builtin linters (default + clippy)
- `--lint-only <name>`: run a specific builtin linter by name
- Using `--clippy`, `--lint-all`, or `--lint-only` implicitly enables
builtin lint mode
The `builtinLint` package option is a tristate (`Option Bool`):
- `true`: always run builtin lints via `lake lint`; when a lint driver
is also configured, builtin lints run first, then the driver, and the
command fails if either reports errors.
- `false`: never run builtin lints automatically; `lake check-lint`
fails unless a lint driver is configured.
- `none` (default): currently equivalent to `false`; in a future
release, `none` will fall back to builtin lints when no lint driver is
configured.
The linter framework introduces a `LintScope` enum (`.default`,
`.clippy`, `.all`) replacing the previous boolean `clippy` parameter in
`getChecks` and `formatLinterResults`. A `@[builtin_nolint]` attribute
(available without imports) allows suppressing specific linters per
declaration.
---------
Co-authored-by: Mac Malone <tydeu@hatpress.net>
Co-authored-by: Thomas R. Murrills <68410468+thorimur@users.noreply.github.com>
This PR fixes the `ControlInfo` inference for a do-block `match`: the
fold over the match arms started from `ControlInfo.pure` (defaults to
`numRegularExits := 1`, `noFallthrough := false`), but `alternative`
sums `numRegularExits` and ANDs `noFallthrough`, so the fold identity is
`{ numRegularExits := 0, noFallthrough := true }`. With the wrong base,
a `match` whose arms all `break`/`continue`/`return` reported
`numRegularExits = 1` and `noFallthrough = false`, suppressing the
dead-code warning on the continuation after the match. The fix corrects
both the inference handler in `InferControlInfo.lean` and the fold in
`elabDoMatchCore`.
This PR splits `ControlInfo`'s dead-code signal in two.
`numRegularExits` is now purely syntactic: how many times the block
wires its continuation into the elaborated expression, consumed by
`withDuplicableCont` as a join-point duplication trigger (`> 1`). The
new `noFallthrough : Bool` asserts that the next doElem in the enclosing
sequence is semantically irrelevant; `false` asserts nothing. Invariant:
`numRegularExits = 0 → noFallthrough`; the converse does not hold.
`sequence` derives `noFallthrough := a.noFallthrough || b.noFallthrough`
(and aggregates syntactic fields unconditionally); `alternative` derives
it as `a.noFallthrough && b.noFallthrough`. The dead-code warning gate
in `withDuplicableCont` and `ControlLifter.ofCont` now reads
`noFallthrough`.
This PR stops the `repeat` inference handler from reporting
`numRegularExits := 0` for break-less bodies. For break-less `repeat`
the loop never terminates normally, so `0` looks more accurate
semantically, but the loop expression still has type `m Unit` and the do
block's continuation after the loop is what carries that type. Reporting
`0` makes the elaborator flag that continuation as dead code, yet there
is no way for the user to remove it that is also type correct — unless
the enclosing do block's monadic result type happens to be `Unit`.
Pinning `numRegularExits` at `1` (matching `for ... in`) eliminates
those spurious warnings.
This PR fixes a bug where the nesting level in Verso Docstrings is
forgotten when there's a doc comment with no headers.
It changes the `terminalNesting` of `VersoModuleDocs` to be recomputed
rather than stored in the structure; we never want it to be anything
besides the default value, and it's easy to accidentally break this
invariant.
Closes#13485
This PR fixes `inferControlInfoSeq` and `ControlInfo.sequence` to keep
aggregating `breaks`/`continues`/`returnsEarly`/`reassigns` past
elements whose `ControlInfo` reports `numRegularExits := 0`. Previously
the analysis short-circuited at such elements, so any trailing
`return`/`break`/`continue` was missing from the inferred info. The
elaboration framework only skips subsequent doElems syntactically for
top-level `return`/`break`/`continue`; for every other `numRegularExits
== 0` case (e.g. a `match`/`if`/`try` whose branches all terminate, or a
`repeat` without `break`) the elaborator keeps visiting the continuation
and the for/match elaborator then tripped its invariant check with
`Early returning ... but the info said there is no early return`. With
this change the inferred info matches what the elaborator actually sees,
which also removes the need for the `numRegularExits := 1` workaround on
`repeat` introduced in #13479.
This PR introduces the Server module, an Async HTTP/1.1 server.
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 ensures that if wrapInstance encounters an instance that cannot
be reduced to a constructor, the wrapping definition is left at
semireducible transparency to avoid leakage.
This PR removes the transitional `macro_rules` for `repeat`, `while`,
and `repeat ... until` from `Init.While`. After the latest stage0
update, the `@[builtin_macro]` and `@[builtin_doElem_elab]` definitions
in `Lean.Elab.BuiltinDo.Repeat` are picked up directly, so the bootstrap
duplicates in `Init.While` are no longer needed. `Init.While` now only
provides the `Loop` type and its `ForIn` instance.
This PR also adjusts `repeat`'s `ControlInfo` to match `for ... in`: its
`numRegularExits` is now unconditionally `1` rather than `if info.breaks
then 1 else 0`. Reporting `0` when the body has no `break` causes
`inferControlInfoSeq` (in any enclosing sequence whose `ControlInfo` is
inferred — e.g. a surrounding `for`/`if`/`match`/`try` body) to stop
aggregating after the `repeat` and miss any `return`/`break`/`continue`
that follows. The corresponding elaborator then sees the actual control
flow disagree with the inferred info and throws errors like `Early
returning ... but the info said there is no early return`. The new test
in `tests/elab/newdo.lean` pins down the regression. See
[#13437](https://github.com/leanprover/lean4/pull/13437) for further
discussion.
This PR refines how the `apply` tactic (and related tactics like
`rewrite`) name and tag the remaining subgoals. Assigned metavariables
are now filtered out *before* computing subgoal tags. As a consequence,
when only one unassigned subgoal remains, it inherits the tag of the
input goal instead of being given a fresh suffixed tag.
User-visible effect: proof states that previously displayed tags like
`case h`, `case a`, or `case upper.h` for a single remaining goal now
display the input goal's tag directly (e.g. no tag at all, or `case
upper`). This removes noise from `funext`, `rfl`-style, and
`induction`-alternative goals when the applied lemma introduces only one
non-assigned metavariable. Multi-goal applications are unaffected —
their subgoals continue to receive distinguishing suffixes.
This may affect users whose proofs rely on the previous tag names (for
example, `case h => ...` after `funext`). Such scripts need to be
updated to use the input goal's tag instead.
---------
Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
This PR fixes a bug in `sym =>` interactive mode where goals whose
metavariable was assigned by `isDefEq` (e.g. via `apply Eq.refl`) were
not pruned. `pruneSolvedGoals` previously only filtered out goals
flagged as inconsistent, so an already-assigned goal would linger as an
unsolved goal. It now also removes goals whose metavariable is already
assigned.
Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
This PR fixes a bug in `sym =>` interactive mode where satellite solvers
(`lia`, `ring`, `linarith`) would throw an internal error if their
automatic `intros + assertAll` preprocessing step already closed the
goal. Previously, `evalCheck` used `liftAction` which discarded the
closure result, so the subsequent `liftGoalM` call failed due to the
absence of a main goal. `liftAction` is now split so the caller can
distinguish the closed and subgoals cases and skip the solver body when
preprocessing already finished the job.
Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
This PR applies two minor tweaks:
- `tests/bench/sym/simp_1.lean`: share-common the proof term before
counting objects in `getProofSize`, so the reported size reflects the
shared representation.
- `tests/elab/sym_simp_3.lean`: use `>>` instead of `.andThen` when
composing `Sym.Simp` methods.
Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
This PR makes the universe level pretty printer instantiate level
metavariables when `pp.instantiateMVars` is true.
Previously level metavariables were not instantiated.
The PR adjusts the tracing in the LevelDefEq module to create the trace
message using the original MetavarContext. It also adds
`Meta.isLevelDefEq.step` traces for when level metavariables are
assigned.
This PR fixes a kernel error in `grind` when propagating a `Nat`
equality to an order structure whose carrier type is not `Int` (e.g.
`Rat`). The auxiliary `Lean.Grind.Order.of_nat_eq` lemma was specialized
to `Int`, so the kernel rejected the application when the cast
destination differed.
We add a polymorphic `of_natCast_eq` lemma over `{α : Type u} [NatCast
α]` and cache the cast destination type in `TermMapEntry`.
`processNewEq` now uses the original `of_nat_eq` when the destination is
`Int` (the common case) and the new lemma otherwise. The symmetric
`nat_eq` propagation (deriving `Nat` equality from a derived cast
equality) is now guarded to fire only when the destination is `Int`,
since the `nat_eq` lemma is still specialized to `Int`.
Closes#13265.
This PR adds a direct regression test for issue #13416. It exercises
`Std.HashMap.getElem_insert`, whose `dom` argument is a lambda closing
over pattern variables, and checks that the discrimination tree lookup
finds the theorem once the target's `dom` lambda is eta-reduced.
The underlying fix landed in #13448; this test pins the specific MWE
from the original issue so a regression would surface immediately.
Closes#13416🤖 Generated with [Claude Code](https://claude.com/claude-code)
Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
This PR fixes a bug in `Sym.introCore.finalize` where the original
metavariable was unconditionally assigned via a delayed assignment, even
when no binders were introduced. As a result, `Sym.intros` would return
`.failed` while the goal metavariable had already been silently
assigned, confusing downstream code that relies on `isAssigned` (e.g. VC
filters in `mvcgen'`).
The test and fix were suggested by Sebastian Graf (@sgraf812).
Co-authored-by: Sebastian Graf <sgraf1337@gmail.com>
Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
This PR removes some cases where `simp` would significantly overrun a
timeout.
This is a little tricky to test cleanly; using mathlib's
`#count_heartbeats` as
```lean4
#count_heartbeats in
set_option maxHeartbeats 200000 in
example (k : Nat) (a : Fin (1 + k + 1) → Nat) :
0 ≤ sumRange (1 + k + 1) (fun i =>
if h : i < 1 + k + 1 then a ⟨i, h⟩ else 0) := by
simp only [Nat.add_comm, sumRange_add]
```
I see 200010 heartbeats with this PR, and 1873870 (9x the requested
limit) without.
This type of failure is wasteful in AI systems which try tactics with a
short timeout.
This PR fixes a regression in `Sym.simp` where rewrite rules whose LHS
contains a lambda over a pattern variable (e.g. `∃ x, a = x`) failed to
match targets with semantically equivalent structure.
`Sym.etaReduceAux` previously refused any eta-reduction whenever the
body had loose bound variables, but patterns produced by stripping outer
foralls always carry such loose bvars. The eta-reduction therefore
skipped patterns while still firing on the target, producing mismatched
discrimination tree keys and no match.
The fix narrows the check to loose bvars in the range `[0, n)` (those
that would actually refer to the peeled binders) and lowers any
remaining loose bvars by `n` so that pattern-variable references stay
consistent in the reduced expression. The discrimination tree now
classifies patterns like `exists_eq_True : (∃ x, a = x) = True` with
their full structure rather than falling back to `.other`.
Includes a regression test (`sym_simp_1.lean`) and Sebastian Graf's MWE
(`sym_eta_mwe.lean`).
🤖 Generated with [Claude Code](https://claude.com/claude-code)
Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
This PR adds two validation checks to `addInstance` that provide early
feedback for common mistakes in instance declarations:
1. **Non-class instance check**: errors when an instance target type is
not a type class. This catches the common mistake of writing `instance`
for a plain structure. Previously handled by the `nonClassInstance`
linter in Batteries (`Batteries.Tactic.Lint.TypeClass`), this is now
checked directly at declaration time.
2. **Impossible argument check**: errors when an instance has arguments
that cannot be inferred by instance synthesis. Specifically, it flags
arguments that are not instance-implicit and do not appear in any
subsequent instance-implicit argument or in the return type. Previously
such instances would be silently accepted but could never be
synthesised.
Supersedes #13237 and #13333.
This PR globally enables `warning.simp.varHead` (added in #13325) and
silences the warning in `Lake.Util.Family.Mathlib` adaptations were
already merged as part of adaptations for #13325. This is a separate PR
from #13325 due to warning appearing when re-bootstrapping, so we needed
`stage0` update before enabling this option.
This PR fixes `processDefDeriving` to propagate the `meta` attribute to
instances derived via delta deriving, so that `deriving BEq` inside a
`public meta section` produces a meta instance. Previously the derived
`instBEqFoo` was not marked meta, and the LCNF visibility checker
rejected meta definitions that used `==` on the alias — this came up
while bumping verso to v4.30.0-rc1.
`processDefDeriving` now computes `isMeta` from two sources:
1. `(← read).isMetaSection` — true inside a `public meta section`,
covering the original issue #13313.
2. `isMarkedMeta (← getEnv) declName` — true when the type being derived
for was individually marked `meta` (e.g. `meta def Foo := Nat`), via
`elabMutualDef` in `src/Lean/Elab/MutualDef.lean`.
This value is passed to `wrapInstance` for aux declarations and to the
new `addAndCompile (markMeta := ...)` parameter from #13311, matching
how the regular command elaboration pipeline handles meta definitions.
Existing regression tests `tests/elab/13043.lean` and
`tests/elab/12897.lean` already cover meta-section + `wrapInstance` aux
def interaction. The new `tests/elab/13313.lean` specifically covers the
delta-derived `BEq` + LCNF-use case (the original issue) and an explicit
`meta def ... deriving BEq` outside a meta section (motivating the
second disjunct).
- [ ] depends on: #13311Closes#13313🤖 Prepared with Claude Code
---------
Co-authored-by: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
This PR fixes#12846, where the new do elaborator produced confusing
errors when a do element's continuation had a mismatched monadic result
type. The errors were misleading both in location (e.g., pointing at the
value of `let x ← value` rather than the `let` keyword) and in content
(e.g., mentioning `PUnit.unit` which the user never wrote).
The fix introduces `DoElemCont.ensureUnitAt`/`ensureHasTypeAt`, which
check the continuation result type early and report mismatches with a
clear message ("The `do` element has monadic result type ... but the
rest of the `do` block has monadic result type ..."). Each do-element
elaborator (`let`, `have`, `let rec`, `for`, `unless`, `dbg_trace`,
`assert!`, `idbg`, etc.) now captures its keyword token via `%$tk` and
passes it to `ensureUnitAt` so that the error points at the do element
rather than at an internal elaboration artifact. The old ad-hoc type
check in `for` and the confusing `ensureHasType` call in
`continueWithUnit` are replaced by this uniform mechanism. Additionally,
`extractMonadInfo` now calls `instantiateMVars` on the expected type,
and `While.lean`/`If.lean` macros propagate token info through their
expansions.
Closes#12846
---------
Co-authored-by: Rob23oba <robin.arnez@web.de>
This PR fixes an issue in the expand reset reuse pass that causes
segfaults in very rare situations.
This bug occurs in situations where two projections from the same field
happen right before a reset,
for example:
```
let x.2 := oproj[0] _x.1;
inc x.2;
let x.3 := oproj[0] _x.1;
inc x.3;
let _x.4 := reset[1] _x.1;
```
when expand reset reuse we optimize situations like this to only `inc`
on the cold path as on the
hot path we are going to keep the projectees alive until at least
`reuse` by just not `dec`-ing the
resetee. However, the algorithm for this assumed that we do not project
more than once from each
field and thus removed both `inc x.2` and `inc x.3` which is too much.
The bug was masked compared to the original #13407 that was reproducible
in 4.29, because the
presented code relied on semantics of global constants which were
changed in 4.30. The PR contains a
modified (and more consistent) reproducer.
Closes: #13407
Co investigated with @Rob23oba
This PR fixes a panic when `coinductive` predicates are defined inside
macro scopes where constructor names carry macro scopes. The existing
guard only checked the declaration name for macro scopes, missing the
case where constructor identifiers are generated inside a macro
quotation and thus carry macro scopes. This caused
`removeFunctorPostfixInCtor` to panic on `Name.num` components from
macro scope encoding.
Closes#13415
This PR adds a basic support for `lake builtin-lint` command that is
used to run environment linters and in the future will be extend to deal
with the core syntax linters.
This PR adds level instantiation and normalization in `getDecLevel` and
`getDecLevel?` before calling `decLevel`.
`getLevel` can return levels with uninstantiated metavariables or
un-normalized structure, such as `max ?u ?v` where the metavariables
have already been assigned. After instantiation and normalization (via
`normalizeLevel`), a level like `max ?u ?v` (with `?u := 1, ?v := 0`)
simplifies to `1 = succ 0`, which `decLevel` can decrement. Without this
step, `decLevel` sees `max ?u ?v`, tries to decrement both arms, fails
on a zero-valued arm, and reports "invalid universe level".
Concretely, this fixes `for` loops with `mut` variables of
sort-polymorphic type (e.g. `PProd Nat True`) where the state tuple's
universe level ends up as an uninstantiated `max`.
The expected-output change in `doNotation1.lean` is because the `for`
loop's unit type now resolves to `Unit` instead of `PUnit` due to the
improved level handling.
This PR makes the `deriving Inhabited` handler for `structure`s be able
to inherit `Inhabited` instances from structure parents, using the same
mechanism as for class parents. This fixes a regression introduced by
#9815, which lost the ability to apply `Inhabited` instances for parents
represented as subobject fields. With this PR, now it works for all
parents in the hierarchy.
Implementation detail: adds `struct_inst_default%` for synthesizing a
structure default value using `Inhabited` instances for parents and
fields.
Closes#13372
This PR improves error reporting when the `do` elaborator produces an
ill-formed expression that fails `checkedAssign` in
`withDuplicableCont`. Previously the failure was silently discarded,
making it hard to diagnose bugs in the `do` elaborator. Now a
descriptive error is thrown showing the join point RHS and the
metavariable it failed to assign to.
Closes#12826
This PR fixes#12768, where the new `do` elaborator produced a
"declaration has free variables" kernel error when the bind
continuation's result type was definitionally but not syntactically
independent of the bound variable. The fix moves creation of the result
type metavariable before `withLocalDecl`, so the unifier must reduce
away the dependency.
For example, given `def Quoted (x : Nat) := Nat`, the expression `do let
val ← pure 3; withStuff val do return 3` would fail because `β` was
assigned `Quoted val` rather than `Nat`.
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 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>
