This PR adds `namespace Lake` to `Lake.Util.Opaque`, which was missing
it. This is technically a breaking change for any code which used
`Opaque` without `open Lake`, but hopefully no one was doing that.
This PR changes `whnfAux` in the equation-theorem generation machinery
to use
reducible transparency (`whnfR`) instead of instances transparency
(`whnfI`).
Previously, the loop in `Eqns.go` would unfold instances on the LHS,
which
interacts badly with users that mark `dite`/`ite` as
`implicit_reducible`:
equation generation would reduce past the `dite` and get stuck instead
of
committing to a branch. The original motivation for `whnfI` (reducing
`Nat.rec ... (OfNat.ofNat 0)` residuals from `match` on numeric
literals) is
already covered by the surrounding
`simpMatch?`/`simpIf?`/`simpTargetStar`
steps in `Eqns.go`, so the full test suite continues to pass.
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Co-authored-by: Claude Opus 4.7 (1M context) <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 adds a check for empty `lake build` invocations (as an empty
build usually indicates a misconfiguration). Builds with no jobs will
now print "Nothing to build." and invocations of `lake build` with no
default targets configured will produce a warning. This will be promoted
to an error in the future. The warning (and future error) can be
suppressed with the new `--allow-empty` CLI option.
---------
Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
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 adds server-side support for incremental diagnostics via a new
`isIncremental` field on `PublishDiagnosticsParams` that is only used by
the language server when clients set `incrementalDiagnosticSupport` in
`LeanClientCapabilities`.
### Context
The goal of this new feature is to avoid quadratic reporting of
diagnostics.
LSP has two means of reporting diagnostics; pull diagnostics (where the
client decides when to fetch the diagnostics of a project) and push
diagnostics (where the server decides when to update the set of
diagnostics of a file in the client).
Pull diagnostics have the inherent problem that clients need to
heuristically decide when the set of diagnostics should be updated, and
that diagnostics can only be incrementally reported per file, so the
Lean language server has always stuck with push diagnostics instead.
In principle, push diagnostics were also intended to only be reported
once for a full file, but all major language clients also support
replacing the old set of diagnostics for a file when a new set of
diagnostics is reported for the same version of the file, so we have
always reported diagnostics incrementally while the file is being
processed in this way.
However, this approach has a major limitation: all notifications must be
a full set of diagnostics, which means that we have to report a
quadratic amount of diagnostics while processing a file to the end.
### Semantics
When `LeanClientCapabilities.incrementalDiagnosticSupport` is set, the
language server will set `PublishDiagnosticsParams.isIncremental` when
it is reporting a set of diagnostics that should simply be appended to
the previously reported set of diagnostics instead of replacing it.
Specifically, clients implementing this new feature should implement the
following behaviour:
- If `PublishDiagnosticsParams.isIncremental` is `false` or the field is
missing, the current diagnostic report for a specific document should
replace the previous diagnostic report for that document instead of
appending to it. This is identical to the current behavior before this
PR.
- If `PublishDiagnosticsParams.isIncremental` is `true`, the current
diagnostic report for a specific document should append to the previous
diagnostic report for that document instead of replacing it.
- Versions should be ignored when deciding whether to replace or append
to a previous set of diagnostics. The language server ensures that the
`isIncremental` flag is set correctly.
### Client-side implementation
A client-side implementation for the VS Code extension can be found at
[vscode-lean4#752](https://github.com/leanprover/vscode-lean4/pull/752).
---------
Co-authored-by: Claude Opus 4.6 <noreply@anthropic.com>
Co-authored-by: Wojciech Nawrocki <13901751+Vtec234@users.noreply.github.com>
This PR fixes an issue with `Workspace.setDepPkgs` (introduced in
#13445) where it did not properly update the workspace `packageMap`. In
addition, this PR further verifies aspects of the workspace construction
during dependency resolution.
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 fixes a benchmark regression introduced in #13475:
`eqnOptionsExt`
was using `.async .asyncEnv` asyncMode, which accumulates state in the
`checked` environment and can block. Switching to `.local` — consistent
with the neighbouring `eqnsExt` and the other declaration caches in
`src/Lean/Meta` — restores performance (the
`build/profile/blocked (unaccounted) wall-clock` bench moves from +33%
back to baseline). `.local` is safe here because
`saveEqnAffectingOptions`
is only called during top-level `def` elaboration and downstream readers
see the imported state; modifications on non-main branches are merged
into the main branch on completion.
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
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 replaces the eager equation realization that was triggered by
non-default values of equation-affecting options (like
`backward.eqns.nonrecursive`) with a `MapDeclarationExtension` that
stores non-default option values at definition time. These values are
then restored when equations are lazily realized, so the same equations
are produced regardless of when generation occurs.
Restoring the options is done via a new `withEqnOptions` helper in
`Lean.Meta.Eqns`. Because `realizeConst` overrides the caller's options
with the options saved in its `RealizationContext` — which are empty
for imported constants — the helper must also be applied inside the
`realizeConst` callbacks in `mkSimpleEqThm`, `mkEqns` (in
`Elab/PreDefinition/Eqns.lean`), `getConstUnfoldEqnFor?`, and
`Structural.mkUnfoldEq`. Without that, equation generation code that
reads eqn-affecting options inside the realize callback would see the
caller-independent defaults rather than the values stored in
`eqnOptionsExt` — so the store-at-definition-time behavior would not
carry across module boundaries.
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
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 adds a type abbreviation `GitRev` to Lake, which is used for
`String` values that signify Git revisions. Such revisions may be a SHA1
commit hash, a branch name, or one of Git's more complex specifiers.
The PR also adds a number of additional Git primitives which are useful
for #11662.
This PR adds `Pakcage.depPkgs` for internal use (namely in #11662). This
field contains the list of the package's direct dependencies (as package
objects). This is much more efficient than going through the old package
`deps` facet.
As part of this refactor, the Workspace `root` is now derived from
`packages` instead of being is own independent field.
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 `JobAction.reuse` and `JobAction.unpack` which provide more
information captions for what a job is doing for the build monitor.
`reuse` is set when using an artifact from the Lake cache, `unpack` is
set when unpacking module `.ltar` archives and release (Reservoir or
GitHub) archives.
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 removes the transitional `syntax` declarations for `repeat`,
`while`, and `repeat ... until` from `Init.While` and promotes the
corresponding `@[builtin_doElem_parser]` defs in `Lean.Parser.Do` from
`low` to default priority, making them the canonical parsers.
The `macro_rules` in `Init.While` are kept as a bootstrap: they expand
`repeat`/`while`/`until` directly to `for _ in Loop.mk do ...`, which is
what any `prelude` Init file needs. The `@[builtin_macro]` /
`@[builtin_doElem_elab]` in `Lean.Elab.BuiltinDo.Repeat` are only
visible once `Lean.Elab.*` is transitively imported, so they cannot
serve Init bootstrap. The duplication will be removed in a follow-up
after the next stage0 update.
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 promotes the `repeat`, `while`, and `repeat ... until` parsers
from `syntax` declarations in `Init.While` to `@[builtin_doElem_parser]`
definitions in `Lean.Parser.Do`, alongside the other do-element parsers.
The `while` variants and `repeat ... until` get `@[builtin_macro]`
expansions; `repeat` itself gets a `@[builtin_doElem_elab]` so a
follow-up can extend it with an option-driven choice between `Loop.mk`
and a well-founded `Repeat.mk`.
The new builtin parsers are registered at `low` priority so that the
bootstrapping `syntax` declarations in `Init.While` (still needed for
stage0 compatibility) take precedence during the transition. After the
next stage0 update, the `Init.While` syntax and macros can be removed.
This PR fixes a bug in EmitC that can be caused by working with the
string literal `"\x01abc"` in
Lean and causes a C compiler error.
The error is as follows:
```
run.c:29:189: error: hex escape sequence out of range
29 | static const lean_string_object l_badString___closed__0_value = {.m_header = {.m_rc = 0, .m_cs_sz = 0, .m_other = 0, .m_tag = 249}, .m_size = 5, .m_capacity = 5, .m_length = 4, .m_data = "\x01abc"};
| ^~~~~~~
1 error generated.
```
This happens as hex escape sequences can be arbitrarily long while lean
expects them to cut off
after two chars. Thus, the C compiler parses the string as one large hex
escape sequence `01abc` and
subsequently notices this is too large.
Discovered by @datokrat
This PR names the `repeat` syntax (`doRepeat`) and installs dedicated
elaborators for it in both the legacy and new do-elaborators. Both
currently expand to `for _ in Loop.mk do ...`, identical to the existing
fallback macro in `Init.While`.
The elaborators are dead code today because that fallback macro fires
first. A follow-up PR will drop the macro (after this PR's stage0 update
lands) and extend `elabDoRepeat` to choose between `Loop.mk` and a
well-founded `Repeat.mk` based on a `backward.do.while` option.
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 two minor bugs in `io.cpp`:
1. A resource leak in a Windows error path of
`Std.Time.Database.Windows.getNextTransition`
2. A buffer overrun in `IO.appPath` on linux when the executable is a
symlink at max path length.
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 an internal `skip` syntax for do blocks, intended for use
by the `if` and `unless` elaborators to replace `pure PUnit.unit` in
implicit else branches. This gives the elaborator a dedicated syntax
node to attach better error messages and location info to, rather than
synthesizing `pure PUnit.unit` which leaks internal details into
user-facing errors.
Includes a stage0 trigger comment so that the new parser is available
during bootstrapping.
Co-authored-by: Rob23oba <robin.arnez@web.de>
This PR fixes a bug where tactic auto-completion would produce tactic
completion items in the entire trailing whitespace of an empty tactic
block. Since #13229 further restricted top-level `by` blocks to be
indentation- sensitive, this PR adjusts the logic to only display
completion items at a "proper" indentation level.
Co-authored-by: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
