This PR adds an opt-in linter (`set_option simp.rfl.checkTransparency
true`) that warns when a `rfl` simp theorem's LHS and RHS are not
definitionally equal at `.instances` transparency. Bad rfl-simp theorems
— those that only hold at higher transparency — create problems
throughout the system because `simp` and `dsimp` operate at restricted
transparency. The linter suggests two fixes: use `id rfl` as the proof
(to remove the `rfl` status), or mark relevant constants as
`[implicit_reducible]`.
This is part of a broader effort to ensure `isDefEq` respects
transparency levels. The linter helps systematically identify
problematic rfl-simp theorems so they can be fixed incrementally.
Co-authored-by: Claude Opus 4.6 <noreply@anthropic.com>
This PR marks any exposed (non-private) auxiliary match declaration as
`[implicit_reducible]`. This is essential when the outer declaration is
marked as `instance_reducible` — without it, reduction is blocked at the
match auxiliary. We do not inherit the attribute from the parent
declaration because match auxiliary declarations are reused across
definitions, and the reducibility setting of the parent can change
independently. This change prepares for implementing the TODO at
`ExprDefEq.lean:465`, which would otherwise cause too many failures
requiring manual `[implicit_reducible]` annotations on match
declarations whose names are not necessarily derived from the outer
function.
---------
Co-authored-by: Claude Opus 4.6 <noreply@anthropic.com>
This PR adds a new option `backward.isDefEq.respectTransparency.types`
that controls the transparency used when checking whether the type of a
metavariable matches the type of the term being assigned to it during
`checkTypesAndAssign`. Previously, this check always bumped transparency
to `.default` (via `withInferTypeConfig`), which is overly permissive.
The new option uses `.instances` transparency instead (via
`withImplicitConfig`), matching the behavior already used for implicit
arguments.
The option defaults to `false` (preserving old behavior) until stage0 is
updated and breakage is assessed. If
`backward.isDefEq.respectTransparency` (already in v4.29) is set to
`false`, then `backward.isDefEq.respectTransparency.types` is
automatically treated as `false` too.
When `diagnostics` is enabled, a trace message is emitted if the
stricter transparency fails but `.default` would have succeeded, helping
identify affected code. To investigate failures when enabling
`backward.isDefEq.respectTransparency.types`, use:
```
set_option diagnostics true
set_option trace.diagnostics true
```
Also renames `withInstanceConfig` to `withImplicitConfig` since it now
serves implicit argument and type checking, not just instances.
Registers the `diagnostics` trace class in `CoreM`.
Co-authored-by: Claude Opus 4.6 <noreply@anthropic.com>
This PR adds a `deprecated_syntax` command that marks syntax kinds as
deprecated. When deprecated syntax is elaborated (in terms, tactics, or
commands), a linter warning is emitted. The warning is also emitted
during quotation precheck when a macro definition uses deprecated syntax
in its expansion.
The `deprecated_syntax` command takes a syntax node kind, an optional
message, and a `(since := "...")` clause. Deprecation warnings correctly
attribute the warning to macro call sites when the deprecated syntax is
produced by macro expansion, including through nested macro chains.
---------
Co-authored-by: Sebastian Ullrich <sebasti@nullri.ch>
The stage0 tree hash used by Lake to invalidate stage 1 oleans was
computed via `git ls-tree HEAD`, which fails in jj workspaces (no .git
directory). Fall back to discovering the backing git repo via `jj git
root` and resolving the current workspace's commit via `jj log -r @`
(since git's HEAD points to the root jj workspace, not the current one).
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>
