This PR renames `goalDotAlt` to `invariantDotAlt` and `goalCaseAlt` to
`invariantCaseAlt` to better reflect that these syntax nodes are
specific
to invariant alternatives in `mvcgen`, not general goal alternatives.
Part 2 of #13137, which made `elabInvariants` resilient to this rename
by using positional dispatch instead of quotation pattern matching.
---------
Co-authored-by: Claude Opus 4.6 <noreply@anthropic.com>
This PR replaces quotation pattern matches on `goalDotAlt`/`goalCaseAlt`
in `elabInvariants` with positional/structural dispatch based on
`getNumArgs`. This is part 1 of renaming `goalDotAlt` to
`invariantDotAlt` and `goalCaseAlt` to `invariantCaseAlt`; the
elaborator change lands first so that the subsequent rename does not
require a stage0 update.
---------
Co-authored-by: Claude Opus 4.6 <noreply@anthropic.com>
This PR switches all usages from `@[mvcgen_invariant_type]` to
`@[spec_invariant_type]` and removes the old attribute registration.
Concludes the work of #13153.
Co-authored-by: Claude Opus 4.6 <noreply@anthropic.com>
This PR registers the new `spec_invariant_type` attribute alongside the
old
`mvcgen_invariant_type`, renames internal identifiers, and replaces the
hardcoded `Invariant` check in `Spec.lean` with `isSpecInvariantType`.
A follow-up PR will switch all usages to `spec_invariant_type` and
remove
the old attribute after stage0 is updated.
Co-authored-by: Claude Opus 4.6 <noreply@anthropic.com>
This PR re-enables `#print axioms` under the module system by computing
axiom dependencies at olean serialization time. It reverts #8174 and
replaces it with a proper fix.
Depends on #13142, which refactors `exportEntriesFnEx` to return all
three olean levels at once via a new `OLeanEntries` structure, allowing
extensions to share expensive computation.
The axiom extension uses `exportEntriesFnEx` to walk bodies of all
public declarations in the current module, collecting axiom dependencies
in a single batch with a shared cache across declarations. The results
are stored sorted for binary search and exported uniformly to all olean
levels. Downstream modules look up pre-computed axiom data from imported
oleans, so axiom collection never crosses module boundaries. During
elaboration of the current module, `collectAxioms` walks bodies directly
since they are always available locally.
---------
Co-authored-by: Claude Opus 4.6 <noreply@anthropic.com>
This PR fixes theoretical leaks in the handling of `Array.get!Internal`
in the code generator.
Currently, the code generator assumes that the value returned by
`get!Internal` is derived from the
`Array` argument. However, this does not generally hold up as we might
also return the `Inhabited`
value in case of an out of bounds access (recall that we continue
execution after panics by
default). This means that we sometimes convert an `Array.get!Internal`
to
`Array.get!InternalBorrowed` when we are not allowed to do so because in
the panic case the
`Inhabited` instance can be returned and if it is an owned value it is
going to leak.
The fix consists of adapting several components to this change:
1. `PropagateBorrow` will only mark the derived value as forcibly
borrowed if both the `Inhabited`
and `Array` argument are forcibly borrowed.
2. `InferBorrow` will do the same for its data flow analysis
3. The derived value analysis of `ExplicitRC` is extended from a derived
value tree to a derived
value graph where a value may have more than one parent. We only
consider a value borrowed if all
of its parents are still accessible. Then `get!Internal` is equipped
with both its `Inhabited`
and its `Array` parent.
These changes are sufficient for correctness on their own. However, they
are going to break
`get!Internal` to `get!InternalBorrowed` conversion in most places. This
happens because almost all
`Inhabited` instances are going to be constants. Currently reads from
constants yield semantically
owned values and thus block the `get!InternalBorrowed` conversion. We
would thus prefer for these
constants to be treated as borrows instead.
The owned return is implemented in two ways at the moment:
1. In the C code emitter we do not need to do anything as constants are
marked persistent to begin
with
2. In the interpreter whenever a constant is pulled from the constant
cache it is `inc`-ed and then
later `dec`-ed somewhere (potentially using a `dec[persistent]` which is
a no-op in C)
This PR changes the semantics of constant reads to instead be borrows
from the constant (they can be
cutely interpreted as "being borrowed from the world"). This enables
many `get!Internal` to have
both their arguments be marked as borrowed and thus still converted to
`get!InternalBorrowed`. Note
that this PR does not yet change the semantics of the interpreter to
account for this
(it will be done in a part 2) and thus introduces (very minor) leaks
temporarily.
Furthermore, we observed code with signatures such as the following:
```lean
@[specialize]
def foo {a : Type} [inst : Inhabited a] (xs : Array a) (f : a -> a -> Bool) ... :=
...
let x := Array.get!Internal inst xs i
...
```
being instantiated with `a := UInt32`. This poses a challenge because
`Inhabited` is currently
marked as `nospecialize`, meaning that we are sometimes going to end up
with code such as:
```
def foo._spec (inst : UInt32) (xs : @&Array UInt32) ... :=
...
let inst := box inst
let x := Array.get!Internal inst xs i
dec inst
...
```
Here `xs` itself was inferred as borrowed, however, the `UInt32`
`Inhabited` instance was not
specialized for (as `Inhabited` is marked `nospecialize`) and thus needs
to be boxed. This causes
the `inst` parameter to `get!Internal` to be owned and thus
`get!InternalBorrowed` conversion fails.
This PR marks `Inhabited` as `weak_specialize` which will make it get
specialized for in this case,
yielding code such as:
```
def foo._spec (xs : @&Array UInt32) ... :=
...
let inst := instInhabitedUInt32
let inst := box inst
let x := Array.get!Internal inst xs i
dec inst
...
```
Fortunately the closed term extractor has support for precisely this
feature and thus produces:
```
def inst.boxed_const :=
let inst := instInhabitedUInt32
let inst := box inst
return inst
def foo._spec (xs : @&Array UInt32) ... :=
...
let inst := inst.boxed_const
let x := Array.get!Internal inst xs i
...
```
As described above reads from constants are now interpreted as borrows
and thus the conversion to
`get!InternalBorrowed` becomes legal again.
This PR introduces the `weak_specialize` attribute. Unlike the
`nospecialize` attribute it does not
block specialization for parameters marked with this type completely.
Instead, `weak_specialize`
parameters are only specialized for if another parameter provokes
specialization. If no such
parameter exists, they are treated like `nospecialize`.
This PR reverts #12882 which added the `@[mvcgen_witness_type]` tag
attribute and `witnesses` section to `mvcgen`. Théophile Wallez
confirmed he doesn't need this feature and can get by with `invariants`,
so there is no use in having it.
The actual `mvcgen` syntax needs to be adjusted after a stage0 update in
order for `elabMVCGen` to cope with both old and new syntax.
Co-authored-by: Claude Opus 4.6 <noreply@anthropic.com>
This PR marks the `Inhabited` arguments of all functions in core marked
as `extern` as borrowed
(panicking array accessors and `panic!` itself). This in turn causes a
transitive effect throughout
the codebase and promotes most, if not all, `Inhabited` arguments to
functions to borrowed.
This PR marks the context argument of `ReaderT` as borrowed, causing a
wide spread of useful borrow annotations throughout the entire meta
stack which reduces RC pressure. This introduces a crucial new behavior:
When modifying `ReaderT` context, e.g. through `withReader` this will
almost always cause an allocation. Given that the `ReaderT` context is
frequently used in a non-linear fashion anyways we think this is an
acceptable behavior.
This PR extracts the functional (lambda) passed to `brecOn` in
structural
recursion into a named `_f` helper definition (e.g. `foo._f`), similar
to
how well-founded recursion uses `._unary`. This way the functional shows
up
with a helpful name in kernel diagnostics rather than as an anonymous
lambda.
The `_f` definition is added with `.abbrev` kernel reducibility hints
and
the `@[reducible]` elaborator attribute, so the kernel unfolds it
eagerly
after `brecOn` iota-reduces. For inductive predicates, the previous
inline
lambda behavior is kept.
To ensure that parent definitions still get the correct reducibility
height
(since `getMaxHeight` ignores `.abbrev` definitions), each `_f`'s body
height is registered via a new `defHeightOverrideExt` environment
extension.
`getMaxHeight` checks this extension for all definitions, making the
height
computation transparent to the extraction.
This change improves code size (a bit). It may regress kernel reduction
times,
especially if a function defined by structural recursion is used in
kernel reduction
proofs on the hot path. Functions defined by structural recursion are
not particularly
fast to reduce anyways (due to the `.brecOn` construction), so already
now it may be
worth writing a kernel-reduction-friendly function manually (using the
recursor directly,
avoiding overloaded operations). This change will guide you in knowing
which function to
optimize.
🤖 Generated with [Claude Code](https://claude.com/claude-code)
---------
Co-authored-by: Claude Opus 4.6 <noreply@anthropic.com>
This PR adds the infrastructure for simproc and discharger DSLs used to
specify `pre`/`post` simproc chains and conditional rewrite dischargers
in `Sym.simp` variants.
**Syntax categories** (`src/Init/Sym/Simp/SimprocDSL.lean`):
- `sym_simproc` with primitives (`ground`, `telescope`, `rewrite`,
`self`, `none`) and combinators (`>>`, `<|>`)
- `sym_discharger` with primitives (`self`, `none`) for the `with`
clause of `rewrite`
**Elaboration attributes**
(`src/Lean/Elab/Tactic/Grind/SimprocDSL.lean`):
- `builtin_sym_simproc` / `sym_simproc` mapping syntax to `Syntax →
GrindTacticM Simproc`
- `builtin_sym_discharger` / `sym_discharger` mapping syntax to `Syntax
→ GrindTacticM Discharger`
- `elabSymSimproc`, `elabSymDischarger`, and `elabWithClause`
dispatchers
Built-in elaborators for each primitive/combinator will follow in a
subsequent PR after the stage0 update.
Co-authored-by: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
This PR adds an `@[mvcgen_invariant_type]` tag attribute so that users
can mark
custom types as invariant types for the `mvcgen` tactic. Goals whose
type is an
application of a tagged type are classified as invariants rather than
verification
conditions. The hard-coded check for `Std.Do.Invariant` is kept as a
fallback
until a stage0 update allows applying the attribute directly.
A follow-up PR (after a stage0 update) will apply
`@[mvcgen_invariant_type]` to
`Std.Do.Invariant` and remove the hard-coded fallback.
---------
Co-authored-by: Claude Opus 4.6 <noreply@anthropic.com>
This PR adds a `cbv_simproc` system for the `cbv` tactic, mirroring
simp's `simproc` infrastructure but tailored to cbv's three-phase
pipeline (`↓` pre, `cbv_eval` eval, `↑` post). User-defined
simplification procedures are indexed by discrimination tree patterns
and dispatched during cbv normalization.
New syntax:
- `cbv_simproc [↓|↑|cbv_eval] name (pattern) := body` — define and
register a cbv simproc
- `cbv_simproc_decl name (pattern) := body` — define without registering
- `attribute [cbv_simproc [↓|↑|cbv_eval]] name` — register an existing
declaration
- `builtin_cbv_simproc` variants for the internal use
New files:
- `src/Init/CbvSimproc.lean` — syntax and macros
- `src/Lean/Meta/Tactic/Cbv/CbvSimproc.lean` — types, env extensions,
registration, dispatch
- `src/Lean/Elab/Tactic/CbvSimproc.lean` — pattern elaboration and
command elaborators
---------
Co-authored-by: Claude Opus 4.6 <noreply@anthropic.com>
This PR adds a warning to any `def` of class type that does not also
declare an appropriate reducibility.
The warning check runs after elaboration (checking the actual
reducibility status via `getReducibilityStatus`) rather than
syntactically checking modifiers before elaboration. This is necessary
to accommodate patterns like `@[to_additive (attr :=
implicit_reducible)]` in Mathlib, where the reducibility attribute is
applied during `.afterCompilation` by another attribute, and would be
missed by a purely syntactic check.
---------
Co-authored-by: Paul Reichert <6992158+datokrat@users.noreply.github.com>
Co-authored-by: Kim Morrison <kim@tqft.net>
Co-authored-by: Claude Opus 4.6 <noreply@anthropic.com>
This PR replaces the `isImplicitReducible` check with `Meta.isInstance`
in the `shouldInline` function within `inlineCandidate?`.
At the base phase, we skip inlining instances tagged with
`[inline]`/`[always_inline]`/`[inline_if_reduce]` because their local
functions will be lambda lifted during the base phase. The goal is to
keep instance code compact so the lambda lifter can extract
cheap-to-inline declarations. Inlining instances prematurely expands the
code and creates extra work for the lambda lifter — producing many
additional lambda-lifted closures.
The previous check used `isImplicitReducible`, which does not capture
the original intent: some `instanceReducible` declarations are not
instances. `Meta.isInstance` correctly targets only actual type class
instances. Although `Meta.isInstance` depends on the scoped extension
state, this is safe because `shouldInline` runs during LCNF compilation
at `addDecl` time — any instance referenced in the code was resolved
during elaboration when the scope was active, and LCNF compilation
occurs before the scope changes.
🤖 Generated with [Claude Code](https://claude.com/claude-code)
Co-authored-by: Claude Opus 4.6 <noreply@anthropic.com>
This PR enables the module system, in cooperation with the linker, to
separate meta and non-meta code in native binaries. In particular, this
ensures tactics merely used in proofs do not make it into the final
binary. A simple example using `meta import Lean` has its binary size
reduced from 130MB to 1.7MB.
# Breaking change
`importModules (loadExts := true)` must now be preceded by
`enableInitializersExecution`. This was always the case for correct
importing but is now enforced and checked eagerly.
