This PR fixes possible corruption when recovering from memory
exhaustion.
This code threw an `std::bad_alloc` in the case of memory exhaustion,
but left the small allocator in an inconsistent state when doing so.
This would mean any code catching and recovering from the allocation
failure would likely find itself with a corrupt small allocator.
While we could try and make this code exception safe in future, simply
making it panic is better than the status quo, and is consistent with
how we handle most other allocation failures.
changelog-please-rerun-the-changelog-ci
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.
Those action runs don't have access to the READ_RUNNERS_TOKEN secret, so
they should just fall back to the namespace runner.
Also, this PR removes the permission checks again. They are failing for
some non-user authors (e.g. copilot) and could be removed anyways by a
malicious actor in a PR.
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 ensures that the `lean --error=tag` flag actually sets a
non-zero exit code on promoted errors.
Closes#13588, fixing the feature introduced in #6362.
This PR prevents undefined behavior in `readModuleDataParts #[]` on
configurations without `LEAN_MMAP`. Previously this would lead to
out-of-bounds indexing.
This PR ensures that `import` gracefully processes `EINTR` errors from
the filesystem.
`read()` is allowed to return fewer bytes than requested, if it is
interrupted. If it is interrupted before returning any bytes, then it
returns `EINTR`. In either case, Lean should keep reading the file.
This PR makes `readModuleDataParts` report a clearer error if there is
insufficient memory to load a module.
changelog-ignores-my-messages-unless-i-edit-the-description-afterwards
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 renames `UInt8.ofNatTruncate` to `UInt8.ofNatClamp`.
The new name is more consistent with the rest of the library (e.g.,
`Int8.toNatClampNeg`) and also more clear. See also [#lean4 > Name of
UInt32.ofNatTruncate etc may be
wrong](https://leanprover.zulipchat.com/#narrow/channel/270676-lean4/topic/Name.20of.20UInt32.2EofNatTruncate.20etc.20may.20be.20wrong/with/591873604).
Historical note: during prehistoric times (in January 2024),
`UInt32.ofNatTruncate` (only the 32 bit version) was introduced for use
in the `simp` configuration. When I looked at the `UIntX` API more
properly later, I added the missing variants but didn't reconsider the
name.
This PR changes Lake's module import graph processing to await the
completion of any `needs` targets or other extra dependencies (such as
cloud releases). This both enables the `needs` targets to influence
header processing and prevents them from racing with said processing.
**Known Limitation:** This PR currently blocks on the `needs` targets
rather than running the import processing in a callback. This is done to
keep import processing simple and in a single thread. If this proves to
be a performance issue, this can be restructured in a future PR with a
more sophisticated refactor.
Closes#13598
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 script that imports the target modules and reads an
appropriate information from environment extensions about deprecated
modules, options and usage of deprecated syntax.
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 changes `Invariant`, `StringInvariant`, and
`StringSliceInvariant` from `abbrev` to `@[spec_invariant_type, simp,
grind =] def`, so that they remain visible as applications of a named
constant in proof states (where `SymM` does not unfold `def`s) and can
be detected as invariant types by `isSpecInvariantType`. The `@[simp,
grind =]` annotations ensure they still unfold on demand under `simp`
and `grind`.
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 adds several entailment-related lemmas to `Std.Do.SPred` and
`Std.Do.PostCond`, intended for goal-decomposition during program
verification proof automation.
- `SPred.down_pure_nil` and `SPred.apply_pure_cons` (existing `rfl`
lemmas) become `@[simp, grind =]`. Drops the now-redundant `pure_cons`
argument from `simp` in `conjunction_apply`.
- New `SPred.entails_nil_intro` and `SPred.entails_nil_pure_intro`:
introduction forms for `entails` at `SPred []`, mirroring the existing
`entails_cons_intro`.
- New `SPred.down_pure_intro`: derive `(pure φ).down` from `φ`.
- New `SPred.apply_pure_cons_entails_l`/`_r`: peel a state argument from
`pure (σ::σs) φ s` on either side of `⊢ₛ`.
- New `Std.Do.ExceptConds.entails.pure`: closes any `⊢ₑ` goal at
`PostShape.pure`, where `ExceptConds.entails` reduces to `True`.
