This PR moves the compiled Lake configurations (e.g., `lakefile.olean`)
from the package's `.lake/config` directory to the workspace's
`.lake/config`. This removes a potential source contention between
workspaces sharing a dependency.
This PR adds an experimental tactic `mvcgen'` that will soon replace
`mvcgen`. It has been reimplemented from the ground up using the new
`SymM`-based framework for efficient symbolic evaluation and can
outperform `mvcgen` by a factor of >100x for some synthetic benchmarks.
`mvcgen'` aspires to be feature-complete with `mvcgen`. Known exceptions
currently are join point sharing, introduction of local specs and
smaller bugs.
The implementation of `mvgen'` used to live in the benchmark suite for
rapid prototyping; this commit merely moves it into the Lean toolchain.
Doing so results in an build time instruction count increase in
seemingly unrelated tests such as `elab/delayed_assign//instructions`;
the reason is that the builtin elaborator attribute now pulls in
substantially more import code on startup.
---------
Co-authored-by: Sebastian Graf <sg@lean-fro.org>
This PR adds `whileM`, a counterpart to `Lean.Loop.forIn` that admits a
one-step unfolding lemma `whileM_eq` (impossible to prove for the
original `partial def`). `Lean.Loop.forIn` now expands to `whileM`, so
`repeat`/`while` keep working without source changes, and the
`Spec.whileM`/`Spec.forIn_loop` `@[spec]` theorems let `mvcgen`
discharge their bodies given a Nat variant and an `α ⊕ β` invariant.
`whileM.impl` is still a `partial def`, but returns a `Subtype
(whileM.Pred f a)` whose property pins the value to an `Acc.recOn` term
whenever an `Acc` and a `MonadAttach` witness exist; `whileM_eq`
extracts that property. A `@[implemented_by]` `whileM.erased` keeps the
runtime a tail call after specialization and would be unnecessary if the
compiler were able eta-expand through the trivial `Subtype` structure.
Supporting infrastructure:
`Internal.Ensures`/`MayReturn`/`ErasesTo`/`IsAttach` and `WPAdequate`
for `Id`/`ReaderT`/`StateT`/`ExceptT`/`OptionT`.
The resulting `while` loops take more work to optimize, hence a modest
increase in build time instructions.
This PR ensures that one can hover over the function name in
fun_induction. Fixes#13673
---------
Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
This PR adds support for blockquotes to Verso docstrings, which had been
missing before. It also substantially improves the robustness of
Verso->Markdown rendering of docstrings, especially the handling of
blockquote line prefixes.
This PR fixes the semantics of `mvcgen' with grind`: it now logs an
error per VC that `grind` cannot close and throws at the end, instead of
silently leaving the unsolved VC as a residual. The previous
silent-fallback behaviour is preserved as `mvcgen' with (try grind)`,
which `elabPreTac` recognises and routes to the same efficient `.grind`
path with a `silent` flag.
Co-authored-by: Sebastian Graf <sg@lean-fro.org>
This PR adds a `+debug` config option to `mvcgen'` and a
`BackwardRule.applyChecked` wrapper around `BackwardRule.apply`. On
apply failure with `+debug` set, the wrapper retries on the
`unfoldReducible`-normalized goal type; if the retry succeeds, an
earlier step missed a normalization and `mvcgen'` raises a hard error
naming the rule (auto-derived from `rule.expr.getAppFn` when available)
and showing the original vs. normalized types.
---------
Co-authored-by: Sebastian Graf <sg@lean-fro.org>
This PR replaces the `check_cancel` two-way coordination protocol used
by
`tests/server_interactive/cancellation_par.lean` with a single tactic
`block_until_cancelled "<label>"`. The first invocation for a label
registers
a promise, prints `<label>: blocked`, and loops on
`Core.checkInterrupted`
until the cancel token fires (then `finally` resolves the promise). Any
later
invocation for the same label waits on that promise — so the test only
terminates if the first invocation actually exited the loop. If
cancellation
fails to propagate, the second invocation's `IO.wait` blocks forever and
the
test hangs (timeout = failure), with no false-success path.
The test was disabled in `tests/CMakeLists.txt` due to flakiness in the
old
two-way protocol; this PR re-enables it. Verified that reverting #13428
makes the test deadlock as expected.
Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
---------
Co-authored-by: Claude Opus 4.7 <noreply@anthropic.com>
This PR cleans up `tests/bench/mvcgen/sym/lib/VCGen/Util.lean`.
- Drops the four `mkApp{Rev,RevRange,Range,N}S` helpers that were
vendored locally; they are now public in `Lean.Meta.Sym.Internal`
(`Lean.Meta.Sym.AlphaShareBuilder`).
- Moves `Std.HashMap.getDM` out of the root `Std.HashMap` namespace into
`namespace VCGen` and relocates it to `RuleCache.lean`, where its only
call sites live.
---------
Co-authored-by: Sebastian Graf <sg@lean-fro.org>
This PR fixes an issue in the `mvcgen'` prototype where user-provided
invariant values were elaborated against a goal type containing
reducible abbreviations like `PostShape.args ps`, baking
`(PostShape.args PostShape.pure)` into the assignment instead of `[]`.
After `tryInlineInvariant` confirms the user tactic assigned the
invariant metavariable, reduce its assignment with `unfoldReducible`.
Fixes the `mvcgen'` migration path for several `tests/elab/*` proofs
that had been blocked on the entailment-phase apply failure.
Co-authored-by: Sebastian Graf <sg@lean-fro.org>
This PR fixes an "Unknown constant" error when `set_option diagnostics
true` is enabled in module mode under a `public section`. Diagnostic
output may reference private declarations such as `_match_*` and
`_sparseCasesOn_*` that are recorded in unfold counters; constructing
the message previously failed because the environment was in exporting
mode and could not resolve those names. The diagnostic-printing paths in
`Lean.Meta.Diagnostics.reportDiag` and
`Lean.Meta.Tactic.Simp.Diagnostics.reportDiag` now run under
`withoutExporting`.
Closes https://github.com/leanprover/lean4/issues/13581.
🤖 Prepared with Claude Code
Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
This PR makes the elaborator reject `@[foo]` when the module that
registers `foo` is not visibly imported into the current file but merely
loaded as IR. Previously such uses silently elaborated but led to
divergence of cmdline and server behavior and caused `lake shake --fix`
to flip-flop on successive runs (#13599).
This PR renames the `lake lint --clippy` flag to `--extra` and broadens
its scope so that it runs the default builtin linters together with the
non-default ones, instead of only the non-default ones. Use `--lint-all`
to additionally enable any other off-by-default linters.
The matching internal names follow: the namespace `Lean.Linter.Clippy`
becomes `Lean.Linter.Extra`, the option `linter.clippy` becomes
`linter.extra`, and the env-linter attribute form `@[builtin_env_linter
clippy]` becomes `@[builtin_env_linter extra]`.
Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
This PR adds the ability to specify a name for the initialization
function of a Lean plugin on load.
* The `Lean.loadPlugin` API has gained a `initFn?` argument that
defaults to `none`. When `none`, the initialization function name will
be inferred from the shared library's name (as before).
* The CLI `--plugin` option can now have a initialization function
specified via `--plugin=path:initFn`.
* The `--setup` JSON configuration now also accepts`{"path": ...,
"initFn": ...}` for plugins.
This PR fixes the termination checker reporting errors at the wrong
recursive call site when a function contains structurally-identical
recursive calls at different source locations.
The `_recApp` `MData` attached to recursive applications carried the
attached `Syntax`, but two structurally-equal `MData` wrappers could be
merged by hashconsing/simplification, so the syntax of the first call
ended up associated with both call sites. We now also store the source
byte position as `_recAppPos`, which keeps the wrappers distinct.
Closes#13444.
This PR makes radar use the LLVM that we actually ship to users (stored
at https://github.com/leanprover/lean-llvm). In doing so it also makes
the lake build compatible with lean-llvm, allowing us to do potential
release builds with lake in the future.
This PR brings the Sym-based `mvcgen'` to feature parity with `mvcgen`;
the only remaining gap is `+jp` (join-point handling).
The slight benchmark regressions are due to simplifying VCs out of
`SPred` form, hitting hardest on cases with linearly many VCs like
`PurePreCond`. The ~10% vcgen slowdown is worth it for the cleaner
user-visible VCs.
---------
Co-authored-by: Claude Opus 4.6 <noreply@anthropic.com>
This PR adds a trace event emitted whenever a `dsimp` (or rfl-only
`simp`) rewrite fires
because of a `[backward_defeq]`-tagged theorem (i.e., one that would not
have applied without `set_option backward.defeqAttrib.useBackward
true`).
Useful for finding where downstream code is silently relying on the
backwards escape hatch — a precursor to either re-tagging the lemma as
`[defeq]` or restructuring the proof so it works under the strict
defeq rules.
This PR fixes a `Sym.simp` panic ("unexpected kernel projection term
during simplification") that triggered when matcher iota-reduction
exposed kernel `Expr.proj` terms via struct-eta. For example, a `do`
block with a `for` loop whose state is a tuple, where `Sym.simp`
unfolds the equational lemma and then descends into a destructuring
match.
This PR fixes a Lake issue where the IR for a `meta import`'s transitive
imports was not included in the import artifacts Lake provided to Lean
(e.g., via `--setup`). When using the Lake artifact cache, this could
produce "missing data file" errors due to absent IR.
Closes#13419
---------
Co-authored-by: Claude Code <noreply@anthropic.com>
This PR fixes a `grind` congruence-table invariant violation that could
panic
when an `ite` branch was internalized lazily (after the condition became
`True`
or `False`) and that branch's equivalence class was later merged with
another.
`Internalize.lean` has a special case for `ite` that internalizes only
the
condition; the `then`/`else` branches are skipped and only internalized
later
on demand by `propagateIte`. The on-demand path (`applyCongrFun`) called
`internalize` for the branch but never called `registerParent` to add
the
parent `ite` to the branch's parent set in the e-graph. Subsequent
merges of
the branch's equivalence class then skipped re-hashing the `ite` in the
congruence table, leaving an orphan entry whose `congr` chain no longer
matched
the table's representative.
The fix adds the explicit `registerParent e rhs` that the standard
`for arg in args` loop in `Internalize.lean` would have made for an
ordinary
application argument; we are simply mirroring that pattern lazily. The
same
helper is reused by `propagateDIte`, but with parent registration
disabled
(controlled by a new `ite : Bool` parameter): for `dite` the `rhs`
propagated
upwards is a *constructed* reduction (built via `mkApp` from `e`'s
children,
possibly post-`preprocess`), not a structural argument of `e`, so
registering
`e` as its parent would be incorrect. The lambda branches of a `dite`
are
already eagerly internalized as parents of `e` by `Internalize.lean`, so
this
case does not need the fix.
---------
Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
This PR fixes a `grind` internal error triggered when `cast` (or
`Eq.rec`, `Eq.ndrec`, `Eq.recOn`) is applied to an argument that has not
yet been internalized. `pushCastHEqs` was emitting `e ≍ a` before
internalizing the args of `e`, so the `rhs` of the heq had no enode and
the debug sanity check tripped. The call now runs after the args are
internalized.
This PR adds infrastructure to help diagnose cases where tactics like
`unfold`
leave the goal in a state that is type-correct only at `.default`
transparency,
causing `rw`/`simp` to fail at `.instances` transparency.
Changes:
- Add a `transparency` parameter to `Meta.check` (defaults to `.all`)
- Add `withInstancesTypeCheckNote` which appends a
lazy note to tactic errors when the target is not type-correct at
`.instances`
- Wrap `rw`, `simp`, `dsimp`, and `simp_all` at the Elab level
- Add opt-in `linter.tacticCheckInstances` that proactively checks every
tactic goal and reports semireducible defs that should be marked
`@[implicit_reducible]`, using diagnostic counter diffing between
`.default`
and `.instances` checks
This PR extends the procedure behind `inferInstanceAs`/`def ...
deriving` to continue recursion through the class graph even when a
(local) instance to wrap was found in order to re-use already-wrapped
instance of subclasses.
This PR ensures consistent metavariable behavior between Verso
docstrings and Verso moduledocs by sharing more code between their
elaborators. It also improves the error message when a metavariable leak
is prevented.
This PR disables model-based theory combination (`mbtc`) in `grind`'s
`NoopConfig`, which is the base configuration used by the derived
tactics `lia`, `linarith`, `cutsat`, `order`, and `ring`. Without this
fix, these tactics could engage in wasteful reasoning via theory
combination, causing them to run for a long time (or hit the
deterministic timeout) on problems they are not designed to solve. With
this fix, these tactics fail quickly on out-of-scope problems, as
expected.
Closes#13573.
This PR makes `lia` (and `grind`'s arithmetic case-split heuristic)
recognize
implications whose antecedent is an `And` or `Or` of arithmetic
predicates as
relevant case-split candidates. Previously, `Arith.isRelevantPred` only
matched
`Not`, `LE`, `LT`, `Eq`, and `Dvd`. With `splitImp := false` (the
default),
implications `p → q` are added as split candidates only when `p` is
arith-relevant, so a hypothesis like `(b ≤ e ∧ e < b + c → a ≤ e ∧ e < a
+ d)`
was never registered as a candidate. cutsat/lia would then find a
satisfying
assignment for the constraints it had been told about, but that
assignment
would not necessarily satisfy the original implication, yielding the bad
counterexample reported in #13575.
After this change, `isRelevantPred` recurses through `And` and `Or`
(returning
`true` if either operand is relevant), so the implication is split,
modus
ponens fires in the True branch, and cutsat/lia closes the False branch
via the
disjunction over negated atoms.
Closes#13575.
This PR adds a `ringMaxDegree` configuration option (default `1024`)
that bounds the maximum degree of polynomials processed by the `grind`
ring solver. Equality constraints whose polynomial exceeds this
threshold are discarded (with an issue reported once per goal),
preventing pathological degree explosion on inputs such as `r ^ (2 ^ 250
- 1)`.
This PR also introduces `Poly.simpM?`, a monadic version of `Poly.simp?`
built on the existing safe arithmetic primitives (`mulMonM`, `combineM`,
`mulConstM`) in `Grind.Arith.CommRing.SafePoly`. The previous
reflection-oriented `Poly.simp?` in `Sym.Arith.Poly` lacked the abort
mechanisms needed during proof search, so the simplification path used
by `EqCnstr` now goes through the safe variant. A regression test
`tests/elab/grind_ring_degree_explosion.lean` ensures `grind` fails
quickly on high-degree problems.
This PR gives the `specialize` tactic the ability to instantiate
universal quantifiers other than the first using `specialize h (y := v)`
syntax. It also fixes an issue where `MVarId.assertAfter` did not record
variable alias information, and an issue where `MVarId.replace` and
`MVarId.replaceLocalDecl` did not take metavariables into account when
calculating dependencies. Additionally it fixes some uninstantiated
metavariables bugs, including one in the Infoview tactic state
hypothesis diff.
The `specialize` tactic now uses `Lean.MVarId.replace` to simplify the
implementation, and as a consequence it tries to keep the specialized
hypothesis close to its original spot in the local context.
Additional metaprogramming API:
- `Lean.Expr.getLambdaBody` to accompany `Lean.Expr.getNumHeadLambdas`
- `Lean.LocalContext.setType`, `Lean.MetavarContext.setFVarType`,
`Lean.MVarId.setFVarType`
- `Lean.MVarId.assertAfter'` to assert a new hypothesis as early as
possibly in the context where it is well-formed, as a frontend to
`Lean.MVarId.assertAfter`, which assumes the new hypothesis is
well-formed
Breaking change: metaprograms cannot assume that `MVarId`s change if
metavariables are assigned. For example, the `change` tactic will no
longer change `MVarId`s if the only effect is incidental metavariable
assignments.
Mathlib impact: this revealed many `dsimp`s that did nothing and could
be deleted.
Closes#9893
This PR fixes parallel tactic combinators (`attempt_all_par`,
`first_par`) leaking their subtasks when the server cancels elaboration
on re-elaboration. Subtasks spawned via `CoreM.asTask` (and its
`MetaM`/`TermElabM`/`TacticM` variants) get a fresh `IO.CancelToken`,
which previously had no link to the parent token; `cancelRec` would set
the command-level token but the children kept running.
The fix is one line in `CoreM.asTask`: when a parent token is in scope,
register `cancelToken.set` as an `onSet` callback on the parent.
Server-level cancellation now flows down to every parallel subtask, and
`Core.checkInterrupted` inside the child sees the token set as expected.
Fixes#13300.
Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
---------
Co-authored-by: Claude Opus 4.6 <noreply@anthropic.com>
This PR upstreams `unnecessarySeqFocus` linter from batteries to core
lean as a "clippy" linter - i.e. one that is disabled by default and
executed by `lake lint --clippy`.
---------
Co-authored-by: Mac Malone <tydeu@hatpress.net>
Co-authored-by: Thomas R. Murrills <68410468+thorimur@users.noreply.github.com>
This PR adds regression tests for `do`-notation issues that the new
elaborator fixes:
* `tests/elab/doNotation7.lean` collects reproducers for #2663, #2676,
#3126, #5607, #6426, and #8119.
* `tests/elab/12229.lean` covers the `logInfo` and `Std.TreeMap`
reproducers from #12229.
This PR upstreams `dupNamespace` linter from batteries to work with new
core environment linting framework, as a "clippy" linter - i.e. one that
is not enabled by default.
Stacked on top of #13513.
---------
Co-authored-by: Mac Malone <tydeu@hatpress.net>
Co-authored-by: Thomas R. Murrills <68410468+thorimur@users.noreply.github.com>
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>
