This PR drops `LEAN_NUM_THREADS=1` from the `run_test.sh` of
`bench/mvcgen/sym`. The single-threaded restriction was originally there
to get reproducible benchmark timings, but `run_test.sh` runs as a test
rather than a benchmark, and we do not care about timing reproducibility
for tests. Allowing the default thread count cuts the wall time of what
was the slowest ctest entry from ~30s to ~20s.
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 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 adds an `AGENTS.md` symlink to `.claude/CLAUDE.md` so
Codex-style repository instructions can resolve to the same checked-in
guidance Claude Code already uses.
This keeps the repository's agent-facing instructions in one place
instead of maintaining separate copies for different tools. Previous
Codex runs did not automatically pick up the existing
`.claude/CLAUDE.md` guidance, which caused avoidable drift in PR
formatting and workflow behavior.
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 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 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 updates two Sym benchmarks (`add_sub_cancel.lean` and
`meta_simp_1.lean`) to use the current `SymM.run` API. Both files still
referenced `run'`, which no longer exists, so they failed to elaborate.
Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
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>
