This PR adds high priority to instances for `OfSemiring.Q` in the grind
ring envelope. When Mathlib is imported, instance synthesis for types
like `OfSemiring.Q Nat` becomes very expensive because the solver
explores many irrelevant paths before finding the correct instances. By
marking these instances as high priority and adding shortcut instances
for basic operations (`Add`, `Sub`, `Mul`, `Neg`, `OfNat`, `NatCast`,
`IntCast`, `HPow`), instance synthesis resolves quickly.
🤖 Generated with [Claude Code](https://claude.com/claude-code)
---------
Co-authored-by: Claude Opus 4.6 <noreply@anthropic.com>
Co-authored-by: Kim Morrison <kim@tqft.net>
This PR deprecates `levelZero` in favor of `Level.zero` and `levelOne`
in favor of the new `Level.one`, and updates all usages throughout the
codebase. The `levelZero` alias was previously required for computed
field `data` to work, but this is no longer needed.
🤖 Prepared with Claude Code
MacOS uses a very old version of bash where `"${FOO[@]}"` fails if `set
-u` is enabled and `FOO` is undefined. Newer versions of bash expand
this to zero arguments instead.
Also, `lint.py` used the shebang `#!/usr/bin/env python` instead of
`python3`, which fails on some systems.
In CI, all macos tests run on nscloud runners. Presumably, they have
installed newer versions of various software, hence this didn't break in
CI.
This PR fixes `@[implicit_reducible]` on well-founded recursive
definitions.
`addPreDefAttributes` sets WF-recursive definitions as `@[irreducible]`
by default, skipping this only when the user explicitly wrote
`@[reducible]` or `@[semireducible]`. It was missing
`@[instance_reducible]` and `@[implicit_reducible]`, causing those
attributes to be silently overridden.
Add `instance_reducible` and `implicit_reducible` to the check in
`src/Lean/Elab/PreDefinition/Mutual.lean` that guards against overriding
user-specified reducibility attributes, and add regression tests in
`tests/elab/wfirred.lean`.
## Example
```lean
-- Before fix: printed @[irreducible] def f : List Nat → Nat
-- After fix: printed @[implicit_reducible] def f : List Nat → Nat
@[instance_reducible] def f : ∀ _l : List Nat, Nat
| [] => 0
| [_x] => 1
| x :: y :: l => if h : x = y then f (x :: l) else f l + 2
termination_by l => sizeOf l
#print sig f
```
Fixes#12775
---------
Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
Co-authored-by: nomeata <148037+nomeata@users.noreply.github.com>
This PR adds `at` location syntax to the `cbv` tactic, matching the
interface of `simp at`. Previously `cbv` could only reduce the goal
target; now it supports `cbv at h`, `cbv at h |-`, and `cbv at *`.
`cbvGoal` is rewritten to use `Sym.preprocessMVar` followed by `cbvCore`
within a single `SymM` context, sharing the term table across all
hypotheses and the target. The old `cbvGoalCore` (which reduced one side
of an equation goal at a time) is replaced by a general approach that
reduces arbitrary goal types and hypothesis types, with special handling
for `True` targets and `False` hypotheses. `cbvDecideGoal` is updated to
use the extracted `cbvCore` as well.
🤖 Generated with [Claude Code](https://claude.com/claude-code)
---------
Co-authored-by: Claude Opus 4.6 <noreply@anthropic.com>
This PR adds a dedicated cbv simproc for `Decidable.decide` that
directly matches on `isTrue`/`isFalse` instances, producing simpler
proof terms and avoiding unnecessary unfolding through `Decidable.rec`.
---------
Co-authored-by: Claude Opus 4.6 <noreply@anthropic.com>
This PR adds `deriving noncomputable instance Foo for Bar` syntax so
that delta-derived instances can be marked noncomputable. Previously,
when the underlying instance was noncomputable, `deriving instance`
would fail with an opaque async compilation error.
Now:
- `deriving noncomputable instance Foo for Bar` marks the generated
instance as noncomputable (using `addDecl` + `addNoncomputable` instead
of `addAndCompile`)
- `deriving instance Foo for Bar` pre-checks for noncomputable
dependencies and gives an actionable error with a "Try this:" suggestion
pointing to the noncomputable variant
- For handler-based deriving (inductives/structures), `noncomputable`
sets `isNoncomputable` on the scope
The `optDefDeriving` and `optDeriving` trailing parsers are updated with
`notSymbol "noncomputable"` to prevent them from stealing the parse of
`deriving noncomputable instance ...`.
🤖 Prepared with Claude Code
---------
Co-authored-by: Claude Opus 4.6 <noreply@anthropic.com>
This PR enables Lake to download artifacts from a remote cache service
on demand as part of a `lake build`. It also refactors much of the cache
API to be more type safe.
The newly documented `lake cache add` command loads input-to-output
mappings from a file and stores them in the cache with optional
information about which cache service and what scope they come from.
With this information, Lake can now download artifacts on demand during
a `lake build`.
The `lake cache get` command has also changed its default behavior to
download just the input-to-outputs mapping and then lazily fetch
artifacts from Reservoir as part of a `lake build`. The original eager
behavior can be forced via the new `--download-arts` option.
This PR ensures `linter.all` disables `constructorNameAsVariable`.
The issue was discovered by @eric-wieser while investigating a quote4
issue.
This seems like an easy mistake to make when setting up a new linter,
and perhaps we need a better structure to make it easy to do the right
thing.
---------
Co-authored-by: Claude Opus 4.6 <noreply@anthropic.com>
This PR changes the approach in `simpIteCbv` and `simpDIteCbv`, by
replacing call to `Decidable.decide`
with reducing and direct pattern matching on the `Decidable` instance
for `isTrue`/`isFalse`. This produces simpler proof terms.
---------
Co-authored-by: Claude Opus 4.6 <noreply@anthropic.com>
This PR adds pre-pass simprocs `simpOr` and `simpAnd` to the `cbv`
tactic that evaluate only the left argument of `Or`/`And` first,
short-circuiting when the result is determined without evaluating the
right side. Previously, `cbv` processed `Or`/`And` via congruence, which
always evaluated both arguments. For expressions like `decide (m < n ∨
expensive)`, when `m < n` is true, the expensive right side is now
skipped entirely.
🤖 Generated with [Claude Code](https://claude.com/claude-code)
Co-authored-by: Claude Opus 4.6 <noreply@anthropic.com>
This PR adds a bitblasting circuit for `BitVec.cpop` with a
divide-and-conquer for a parallel-prefix-sum.
This is the [most efficient circuit we could
fine](https://docs.google.com/spreadsheets/d/1dJ5uUY4-eWIQmMjIui3H4U-wBxBxy-qYuqJZFZD1xvA/edit?usp=sharing),
after comparing with Kernighan's algorithm and with the intuitive
addition circuit.
---------
Co-authored-by: Henrik Böving <hargonix@gmail.com>
This PR fixes `pp.fvars.anonymous` to display loose free variables as
`_fvar._` instead of `_` when the option is set to `false`. This was the
intended behavior in https://github.com/leanprover/lean4/pull/12688 but
the fix was committed locally and not pushed before that PR was merged.
🤖 Prepared with Claude Code
Co-authored-by: Claude Opus 4.6 <noreply@anthropic.com>
This PR gives the `generate` function's "apply @Foo to Goal" trace nodes
their own trace sub-class `Meta.synthInstance.apply` instead of sharing
the parent `Meta.synthInstance` class.
This allows metaprograms that walk synthesis traces to distinguish
instance application attempts from other synthesis nodes by checking
`td.cls` rather than string-matching on the header text.
The new class is registered with `inherited := true`, so `set_option
trace.Meta.synthInstance true` continues to show these nodes.
Motivated by mathlib's `#defeq_abuse` diagnostic tactic
(https://github.com/leanprover-community/mathlib4/pull/35750) which
currently checks `headerStr.contains "apply"` to identify these nodes.
See
https://leanprover.zulipchat.com/#narrow/channel/113488-general/topic/backward.2EisDefEq.2ErespectTransparency🤖 Prepared with Claude Code
---------
Co-authored-by: Claude Opus 4.6 <noreply@anthropic.com>
This PR adds a `pp.fvars.anonymous` option (default `true`) that
controls the display of loose free variables (fvars not in the local
context).
- When `true` (default), loose fvars display their internal name like
`_fvar.42`
- When `false`, they display as `_fvar._`
This is analogous to `pp.mvars.anonymous` for metavariables. It's useful
for stabilizing output in `#guard_msgs` when messages contain fvar IDs
that vary between runs — for example, in diagnostic tools that report
`isDefEq` failures from trace output where the local context is not
available.
🤖 Prepared with Claude Code
Co-authored-by: Claude Opus 4.6 <noreply@anthropic.com>
This PR fixes a gap in how `@[implicit_reducible]` is assigned to parent
projections during structure elaboration.
When `class C extends P₁, P₂` has diamond inheritance, some ancestor
structures become constructor subobject fields even though they aren't
direct parents. For example, in `Monoid extends Semigroup, MulOneClass`,
`One` becomes a constructor subobject of `Monoid` — its field `one`
doesn't overlap with `Semigroup`'s fields, and `inSubobject?` is `none`
during `MulOneClass` flattening.
`mkProjections` creates the projection `Monoid.toOne` but defers
reducibility to `addParentInstances` (guarded by `if !instImplicit`).
However, `addParentInstances` only processes direct parents from the
`extends` clause. Grandparent subobject projections fall through the gap
and stay `semireducible`.
This causes defeq failures when `backward.isDefEq.respectTransparency`
is enabled (#12179): at `.instances` transparency, the semireducible
grandparent projection can't unfold, so two paths to the same ancestor
structure aren't recognized as definitionally equal.
Fix: before `addParentInstances`, iterate over all `.subobject` fields
and set `implicitReducible` on those whose parent is a class.
🤖 Prepared with Claude Code
---------
Co-authored-by: Claude Opus 4.6 <noreply@anthropic.com>
The linter was running in parallel with other tests, which were creating
and deleting files. Since the linter was iterating over some files and
directories at the time, it crashed.
This PR ensures the compiler extracts `Array`/`ByteArray`/`FloatArray`
literals as one big closed term to avoid quadratic overhead at closed
term initialization time.
This PR changes the spec lookup procedure in Sym-based mvcgen so that
1. Spec candidates are sorted first before being filtered
2. Instead of filtering the whole set of candidates using
`spec.pattern.match?`, we take the first match with the highest
priority.
The second point means we will do a lot fewer matches when the highest
priority spec matches immediately. In this case, the one match is still
partially redundant with the final application of the backward rule
application. It would be great if could somehow specialize the backward
rule after it has been created. Still, this yields some welcome
speedups. Before and after for each.
```
vcgen_add_sub_cancel:
goal_1000: 865 ms, 1 VCs by grind: 228 ms, kernel: 435 ms
goal_1000: 540 ms, 1 VCs by grind: 229 ms, kernel: 426 ms
vcgen_ping_pong:
goal_1000: 458 ms, 0 VCs, kernel: 431 ms
goal_1000: 454 ms, 0 VCs, kernel: 443 ms (unchanged, because there is only ever one candidate spec)
vcgen_deep_add_sub_cancel:
goal_1000: 986 ms, 1 VCs by grind: 234 ms, kernel: 735 ms
goal_1000: 728 ms, 1 VCs by grind: 231 ms, kernel: 708 ms
vcgen_reader_state:
goal_1000: 746 ms, 1 VCs by sorry: 1 ms, kernel: 803 ms
goal_1000: 525 ms, 1 VCs by sorry: 1 ms, kernel: 840 ms
```
This PR fixes a bug in `Meta.zetaReduce` where `have` expressions were
not being zeta reduced. It also adds a feature where applications of
local functions are beta reduced, and another where zeta-delta reduction
can be disabled. These are all controllable by flags:
- `zetaDelta` (default: true) enables unfolding local definitions
- `zetaHave` (default: true) enables zeta reducing `have` expressions
- `beta` (default: true) enables beta reducing applications of local
definitions
Closes#10850
This PR adds support for generating and discharging postcondition VCs in
Sym-based `mvcgen`. It also adds a new benchmark case
`vcgen_ping_pong.lean` that tests this functionality. This benchmark
required a more diligent approach to maintain maximal sharing in goal
preprocessing. Goal preprocessing was subsequently merged into the main
VC generation function.
This PR changes the order of implicit parameters `α` and `ps` such that
`α` consistently comes before `ps` in `PostCond.noThrow`,
`PostCond.mayThrow`, `PostCond.entails`, `PostCond.and`, `PostCond.imp`
and theorems.
This PR ports the simple ground expression extraction pass from IR to
LCNF.
I locally confirmed that this produces no diff between stage1/stage2 at
the C level (apart from the
changed compiler files) so this should essentially be binary equivalent.
This PR ports the expand reset/reuse pass from IR to LCNF. In addition
it prevents exponential code generation unlike the old one. This results
in a ~15% decrease in binary size and slight speedups across the board.
The change also removes the "is this reset actually used" syntactic
approximation as the previous passes guarantee (at the moment) that all
uses are in the continuation and will thus be caught by this.
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.
This PR adds two `decide_cbv` stress tests extracted from LNSym (ARMv8
symbolic
simulator, Apache 2.0). `cbv_aes.lean` tests a full AES-128 encryption
on large
bitvector computations. `cbv_arm_ldst.lean` tests ARMv8 load/store
instruction
decoding and execution with nested pattern matching over bitvectors.
Co-authored-by: Claude Opus 4.6 <noreply@anthropic.com>
This PR adds a `cbv` tactic test based on a minimized example extracted
from verifying the Collatz conjecture for small numbers, suggested by
Bhavik Mehta (@b-mehta).
---------
Co-authored-by: Claude Opus 4.6 <noreply@anthropic.com>
Co-authored-by: Bhavik Mehta <bhavikmehta8@gmail.com>
This PR reverts commit 9b7a8eb7c8. After
some more contemplation on
the implications of these changes I think this is not the direction we
want to move into.
This PR sets up the new integrated test/bench suite. It then migrates
all benchmarks and some related tests to the new suite. There's also
some documentation and some linting.
For now, a lot of the old tests are left alone so this PR doesn't become
even larger than it already is. Eventually, all tests should be migrated
to the new suite though so there isn't a confusing mix of two systems.
This PR fixes an issue where `mutual public structure` would have a
private constructor. The fix copies the fix from #11940.
Closes#10067. Also recloses duplicate issue #11116 (its test case is
added to the test suite).
This PR adds several useful lemmas for `List`, `Array` and `Vector`
whenever they were missing, improving API coverage and consistency among
these types.
- `size_singleton`/`sum_singleton`/`sum_push`
-
`foldlM_toArray`/`foldlM_toList`/`foldl_toArray`/`foldl_toList`/`foldrM_toArray`/`foldrM_toList`/`foldr_toList`
- `toArray_toList`
- `foldl_eq_apply_foldr`/`foldr_eq_apply_foldl`, `foldr_eq_foldl`:
relates `foldl` and `foldr` for associative operations with identity
- `sum_eq_foldl`: relates sum to `foldl` for associative operations with
identity
- `Perm.pairwise_iff`/`Perm.pairwise`: pairwise properties are preserved
under permutations of arrays
This PR changes all `lean-toolchain` to use relative toolchain paths
instead of `lean4` and `lean4-stage0` identifiers, which removes the
need for manually linking toolchains via Elan.
After this PR, at least Elan 4.2.0 and 0.0.224 of the Lean VS Code
extension will be needed to edit core.
Co-authored-by: Claude Sonnet 4.6 <noreply@anthropic.com>
This PR marks `List.flatten`, `List.flatMap`, `List.intercalate` as
noncomputable to ensure that their `csimp` variants are used everywhere.
We also mark `List.flatMapM` as noncomputable and provide a
tail-recursive implementation, and mark `List.utf8Encode` as
noncomputable, which only exists for specification purposes anyway (at
this point).
Closes#12676.
This PR adds a feature where `inductive` constructors can override the
binder kinds of the type's parameters, like in #9480 for `structure`.
For example, it's possible to make `x` explicit in the constructor
`Eq.refl`, rather than implicit:
```lean
inductive Eq {α : Type u} (x : α) : α → Prop where
| refl (x) : Eq x x
```
In the Prelude, this is currently accomplished by taking advantage of
auto-promotion of indices to parameters.
**Breaking change.** Inductive types with a constructor that starts with
typeless binders may need to be rewritten, e.g. changing `(x)` to `(x :
_)` if there is a `variable` with that name or if it is meant to shadow
one of the inductive type's parameters.
This PR fixes an issue where `withLocation` wasn't saving the info
context, which meant that tactics that use `at *` location syntax and do
term elaboration would save infotrees but revert the metacontext,
leading to Infoview messages like "Error updating: Error fetching goals:
Rpc error: InternalError: unknown metavariable" if the tactic failed at
some locations but succeeded at others.
Closes#10898
This PR fixes two aspects of pretty printing of private names.
1. Name unresolution. Now private names are not special cased: the
private prefix is stripped off and the `_root_` prefix is added, then it
tries resolving all suffixes of the result. This is sufficient to handle
imported private names in the new module system. (Additionally,
unresolution takes macro scopes into account now.)
2. Delaboration. Inaccessible private names use a deterministic
algorithm to convert private prefixes into macro scopes. The effect is
that the same private name appearing in multiple times in the same
delaborated expression will now have the same `✝` suffix each time. It
used to use fresh macro scopes per occurrence.
Note: There is currently a small hack to support pretty printing in the
compiler's trace messages, which print constants that do not exist (e.g.
`obj`, `tobj`, and auxiliary definitions being compiled). Even though
these names are inaccessible (for the stronger reason that they don't
exist), we make sure that the pretty printer won't add macro scopes. It
also does some analysis of private names to see if the private names are
for the current module.
Closes#10771, closes#10772, and closes#10773
