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`.
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 Introduces new foundations for reasoning about monadic Lean
code. Eventually we will port `mvcgen` on top of these new foundations,
to make the framework more general and robust.
Key issues, new metatheory is supposed to solve are
- It gives more flexibility over what an assertion language for
pre-/post-conditions of monadic Hoare triples can be. In particular, any
`CompleteLattice` might become a pre-/post-condtions language, not only
`SPred`. It potentially gives an opportunity to reason about
probabilistic monads, where assertion language are distributions. This
also simplifies the metatheory of monadic Hoare triples, as it does not
require defining the notion of `SPred`, and allows users to work in a
fairly common interface of `CompleteLattice`
- It splits the post-conditions of Hoare triples/ WPs into two: (1)
`post` for post-conditions on terminating paths and (2) `epost` for
post-conditions on abrupt paths. Current foundations always bundle them
into a pair, which inevitably leads to constructing and eliminating such
pairs everywhere in the code.
- It relaxes some conditions that the current foundations require for
instantiating `WPMonad` type class. In particular we do not require `wp`
to distribute over `bind` any more. Instead, we require just `wp x (fun
x => wp (f x) post epost) epost ⊑ wp (x >>= f) post epost`, i.e. the
distributed `wp` must only imply the non-distributed one (and not
necessarily vice versa). With this we can define `WPMonad` for
Separation Logic, where `wp` only distributes over `bind` on
local-footprint computations.
- It solves some universe polymorphism issues. As now universe levels of
assertion languages are independent of universe levels in the monad, one
can define `WPMonad Id.{u} Prop EPost⟨⟩`, which means that for arbitrary
level `Id` the language for pre-/post-conditions is going to be just
`Prop` and the language for post-conditions on abrupt exits is idle.
---------
Co-authored-by: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
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 adds source-level comments noting that the constructors of
`Lean.Meta.TransparencyMode` and `Lean.ReducibilityStatus` are not laid
out in the unfolding-amount order suggested by their docstrings, and
that reordering them induces a non-trivial bootstrap problem.
Also rewrites a stale comment in `Lean.Meta.Basic` that listed the
hierarchy in descending order without `.none`.
🤖 Prepared with Claude Code
Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
This PR fixes a race condition in the Lake build monitor's draining of
the job queue.
Previously, the monitor drained the registered-jobs queue before
checking task states. A finished job in that scan may have registered
new jobs in its body just before terminating. Those jobs landed in the
queue after the drain, so when no other unfinished jobs remained the
monitor exited without ever observing them. If one of the missed jobs
errors, this could produce an "uncaught top-level build failure" message
alongside "Build completed successfully".
To fix this, the monitor loop is restructured so the queue is drained
*after* task states are scanned, with an additional drain before the
loop terminates. `drainQueue` and `scanJobs` are split out from `poll`,
and `Monitor.main` performs an initial drain to capture any jobs
registered before the monitor starts iterating. Finishing jobs cannot
register further work once their state transitions, so a single
post-scan drain is sufficient to close the window.
🤖 Prepared with Claude Code
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 prevents memory exhaustion turning into segfaults when using
Lean functions which call into libuv
`malloc` can return `NULL`, in which case this code would previously go
on to dereference a null pointer.
Instead, it now returns a suitable `IO.Error`.
Calling `lean_internal_panic_out_of_memory` would also be an option
here, since the adjacent `lean_promise_new` calls would fail in this
way.
