This PR adds support for simp/equational spec theorems in the SymM-based
`mvcgen'` tactic,
catching up with a feature that the original `mvcgen` has supported for
a long time.
Users can write `@[spec] theorem : get (m := StateT σ m) = fun s => pure
(s, s) := rfl`
instead of manually specifying equivalent Hoare triples. The equational
form is more
concise and natural for specs that simply unfold definitions.
The universe level normalization (`normalizeLevelsExpr`) applied in
`work` and the backward
rule constructors is a workaround; ideally this should be integrated
into
`preprocessMVar`/`preprocessExpr` in the SymM framework so all users
benefit.
Changes:
- Add `SpecTheoremKind` to distinguish triple vs simp specs in
`SpecTheoremNew`
- Add `mkSpecTheoremNewFromSimpDecl?` to create spec entries from
equational lemmas, filtering no-op equations
- Add `mkBackwardRuleFromSimpSpec` to build backward rules via
`Eq.mpr`/`congrArg`, with instance synthesis, projection reduction, and
`unfoldReducible` on the RHS
- Migrate simp theorems from `SimpTheorems` database during
`migrateSpecTheoremsDatabase`
- Normalize universe levels so structural matching in
`BackwardRule.apply` succeeds when `max u v` vs `max v u` arise from
different code paths
- Simplify `mkSpecContext` by removing the mock `simp` context
construction
- Use `mkBackwardRuleFromExpr` instead of `mkAuxLemma` for triple specs,
since the proof may contain free variables from the goal context
- Add `AddSubCancelSimp` benchmark case and test exercising the simp
spec code path
- Change `AddSubCancel` spec proofs from `mvcgen` to `mvcgen'`
(dogfooding)
🤖 Generated with [Claude Code](https://claude.com/claude-code)
Co-authored-by: Claude Opus 4.6 <noreply@anthropic.com>
This PR extracts the example programs from the sym mvcgen benchmarks
into
shared `Cases.*` modules so that both benchmarks and a new fast test
suite
can reuse them. It also renames `vcgen_deep_add_sub_cancel` to
`vcgen_add_sub_cancel_deep` for consistency.
The test suite (`test_vcgen.lean`) runs all cases at n=10, completing in
~2s vs minutes for the full benchmarks. It is wired up as a `lake test`
driver and integrated with the lean4 test/bench infrastructure via
`run_test`/`run_bench` scripts registered in `CMakeLists.txt`.
Benchmark output now uses aligned `CaseName(n):` labels. The `run_bench`
script extracts per-case vcgen and kernel timings into
`measurements.jsonl`.
Benchmarks run single-threaded (`LEAN_NUM_THREADS=1`) for
reproducibility.
`vcgen_get_throw_set` is excluded from benchmarks due to pathological
`instantiateMVars` behavior.
🤖 Generated with [Claude Code](https://claude.com/claude-code)
---------
Co-authored-by: Claude Opus 4.6 <noreply@anthropic.com>
This PR adds `optType` support to the `doPatDecl` parser, allowing
`let ⟨width, height⟩ : Nat × Nat ← action` in do-notation. Previously,
only
the less ergonomic `let ⟨width, height⟩ : Nat × Nat := ← action`
workaround
was available. The type annotation is propagated to the monadic action
as an
expected type, matching `doIdDecl`'s existing behavior.
Both the legacy and new (BuiltinDo) elaborators are updated.
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 add support for erasing `@[cbv_eval]` annotations using
`attribute [-cbv_eval]`, mirroring the existing `@[-simp]` mechanism for
simp lemmas.
The `CbvEvalEntry` now tracks the original declaration name (`origin`)
so that inverted theorems (`@[cbv_eval ←]`) can be erased by their
original name. The `CbvEvalState` stores individual entries alongside
the composed `Theorems` discrimination tree, allowing the tree to be
rebuilt from remaining entries after erasure. Erasure is properly scoped
via `modifyState`, so `attribute [-cbv_eval]` inside a `section` is
reverted when the section ends.
🤖 Generated with [Claude Code](https://claude.com/claude-code)
This PR adds a `lake-ci` label that enables the full Lake test suite in
CI,
avoiding the need to temporarily commit and revert changes to
`tests/CMakeLists.txt`. The `lake-ci` label implies `release-ci` (check
level
3), so all release platforms are also tested.
Motivated by
https://github.com/leanprover/lean4/pull/12540#issuecomment-4000081071
where @tydeu requested running `release-ci` with Lake tests enabled,
which
previously required temporarily uncommenting a line in
`tests/CMakeLists.txt`.
Users can add it via a PR comment containing `lake-ci` on its own line,
or by
adding the label manually. CI automatically restarts when the label is
added.
Implementation:
- `ci.yml`: detect `lake-ci` label, set check level 3, pass
`-DLAKE_CI=ON` to cmake
- `tests/CMakeLists.txt`: `option(LAKE_CI ...)` conditionally enables
full `tests/lake/tests/` glob
- `restart-on-label.yml`: restart CI on `lake-ci` label
- `labels-from-comments.yml`: support `lake-ci` comment
🤖 Prepared with Claude Code
---------
Co-authored-by: Claude Opus 4.6 <noreply@anthropic.com>
This PR adds a `set_option grind.unusedLemmaThreshold` that, when set to
N > 0
and `grind` succeeds, reports E-matching lemmas that were activated at
least N
times but do not appear in the final proof term. This helps identify
`@[grind]`
annotations that fire frequently without contributing to proofs.
🤖 Prepared with Claude Code
---------
Co-authored-by: Claude Opus 4.6 <noreply@anthropic.com>
This PR adds a `result? : Option TraceResult` field to `TraceData` and
populates it in `withTraceNode` and `withTraceNodeBefore`, so that
metaprograms walking trace trees can determine success/failure
structurally instead of string-matching on emoji.
`TraceResult` has three cases: `.success` (checkEmoji), `.failure`
(crossEmoji), and `.error` (bombEmoji, exception thrown). An
`ExceptToTraceResult` typeclass converts `Except` results to
`TraceResult` directly, with instances for `Bool` and `Option`.
`TraceResult.toEmoji` converts back to emoji for display. This replaces
the previous `ExceptToEmoji` typeclass — `TraceResult` is now the
primary representation rather than being derived from emoji strings.
`withTraceNodeBefore` (used by `isDefEq`) uses
`ExceptToTraceResult.toTraceResult` directly, correctly handling `Bool`
(`.ok false` = failure) and `Option` (`.ok none` = failure), with
`Except.error` mapping to `.error`.
For `withTraceNode`, `result?` defaults to `none`. Callers can pass
`mkResult?` to provide structured results; when set, the corresponding
emoji is auto-prepended to the message.
Motivated by mathlib's `#defeq_abuse` diagnostic tactic
(https://github.com/leanprover-community/mathlib4/pull/35750) which
currently string-matches on emoji to determine trace node outcomes. 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 makes notations such as `∨`, `∧`, `≤`, and `≥` pretty print
using ASCII versions when `pp.unicode` is false.
Continuation of #10373. Closes#1056.
This will require followup with a stage0 update and removal of the
ASCII-only `<=` and `>=` syntaxes from `Init.Notation`, for cleanup.
This PR optimizes the handling of `match_same_ctor.het` to make it emit
nice match trees as opposed to unoptimized CPS style code.
`match_same_ctor.het` is essentially a specialized kind of matcher where
we know that two objects are built from the same constructor and we wish
to call a continuation on their data. This means for every constructor
that contains data `het` takes one closure as an argument. Then after
matching on one of the objects every closure but the one relevant for
the match is released in every match arm, causing quadratic code
generation. This PR ensures that the `het` declarations get inlined and
then further processed by ordinary matcher and casesOn compilation,
thereby removing all of the continuations from the compiled code.
This PR replaces the default `instantiateMVars` implementation with a
two-pass variant that fuses fvar substitution into the traversal,
avoiding separate `replace_fvars` calls for delayed-assigned MVars and
preserving sharing. The old single-pass implementation is removed
entirely.
The previous implementation had quadratic complexity when instantiating
expressions with long chains of nested delayed-assigned MVars. Such
chains arise naturally from repeated `intro`/`apply` tactic sequences,
where each step creates a new delayed assignment wrapping the previous
one. The new two-pass approach resolves the entire chain in a single
traversal with a fused fvar substitution, reducing this to linear
complexity.
### Terminology (used in this PR and in the source)
* **Direct MVar**: an MVar that is not delayed-assigned.
* **Pending MVar**: the direct MVar stored in a
`DelayedMetavarAssignment`.
* **Assigned MVar**: a direct MVar with an assignment, or a
delayed-assigned MVar with an assigned pending MVar.
* **MVar DAG**: the directed acyclic graph of MVars reachable from the
expression.
* **Resolvable MVar**: an MVar where all MVars reachable from it
(including itself) are assigned.
* **Updateable MVar**: an assigned direct MVar, or a delayed-assigned
MVar that is resolvable but not reachable from any other resolvable
delayed-assigned MVar.
In the MVar DAG, the updateable delayed-assigned MVars form a cut (the
**updateable-MVar cut**) with only assigned MVars behind it and no
resolvable delayed-assigned MVars before it.
### Two-pass architecture
**Pass 1** (`instantiate_direct_fn`): Traverses all MVars and
expressions reachable from the initial expression and instantiates all
updateable direct MVars (updating their assignment with the result),
instantiates all level MVars, and determines if there are any updateable
delayed-assigned MVars.
**Pass 2** (`instantiate_delayed_fn`): Only run if pass 1 found
updateable delayed-assigned MVars. Has an **outer** and an **inner**
mode, depending on whether it has crossed the updateable-MVar cut.
In outer mode (empty fvar substitution), all MVars are either unassigned
direct MVars (left alone), non-updateable delayed-assigned MVars
(pending MVar traversed in outer mode and updated with the result), or
updateable delayed-assigned MVars. When a delayed-assigned MVar is
encountered, its MVar DAG is explored (via `is_resolvable_pending`) to
determine if it is resolvable (and thus updateable). Results are cached
across invocations.
If it is updateable, the substitution is initialized from its arguments
and traversal continues with the value of its pending MVar in inner
mode. In inner mode (non-empty substitution), all encountered
delayed-assigned MVars are, by construction, resolvable but not
updateable. The substitution is carried along and extended as we cross
such MVars. Pending MVars of these delayed-assigned MVars are NOT
updated with the result (as the result is valid only for this
substitution, not in general).
Applying the substitution in one go, rather than instantiating each
delayed-assigned MVar on its own from inside out, avoids the quadratic
overhead of that approach when there are long chains of delayed-assigned
MVars.
**Write-back behavior**: Pass 2 writes back the normalized pending MVar
values of delayed-assigned MVars above the updateable-MVar cut (the
non-resolvable ones whose children may have been resolved). This is
exactly the right set: these MVars are visited in outer mode, so their
normalized values are suitable for storing in the mctx. MVars below the
cut are visited in inner mode, so their intermediate values cannot be
written back.
### Pass 2 scope-tracked caching
A `scope_cache` data structure ensures that sharing is preserved even
across different delayed-assigned MVars (and hence with different
substitutions), when possible. Each `visit_delayed` call pushes a new
scope with fresh fvar bindings. The cache correctly handles cross-scope
reuse, fvar shadowing, and late-binding via generation counters and
scope-level tracking.
The `scope_cache` has been formally verified:
`tests/elab/scopeCacheProofs.lean` contains a complete Lean proof that
the lazy generation-based implementation refines the eager
specification, covering all operations (push, pop, lookup, insert)
including the rewind lazy cleanup with scope re-entry and degradation.
The key correctness invariant is inter-entry gen list consistency
(GensConsistent), which, unlike per-entry alignment with `currentGens`,
survives pop+push cycles.
### Behavioral differences from original `instantiateMVars`
The implementation matches the original single-pass `instantiateMVars`
behavior with one cosmetic difference: the new implementation
substitutes fvars inline during traversal rather than constructing
intermediate beta-redexes, producing more beta-reduced terms in some
edge cases. This changes the pretty-printed output for two elab tests
(`1179b`, `depElim1`) but all terms remain definitionally equal.
### Tests
Correctness and performance tests for the new implementation were added
in #12808.
### Files
- `src/library/instantiate_mvars.cpp` — C++ implementation of both
passes (replaces `src/kernel/instantiate_mvars.cpp`)
- `src/library/scope_cache.h` — scope-aware cache data structure
- `src/Lean/MetavarContext.lean` — exported accessors for
`DelayedMetavarAssignment` fields
- `tests/elab/scopeCacheProofs.lean` — formal verification of
`scope_cache` correctness
- `tests/elab/1179b.lean.out.expected`,
`tests/elab/depElim1.lean.out.expected` — updated expected output
Co-authored-by: Claude <noreply@anthropic.com>
---------
Co-authored-by: Claude Opus 4.6 <noreply@anthropic.com>
This PR changes the way the linting for `linter.unusedSimpArgs` gets the
value from the environment. This is achieved by using the appropriate
helper functions defined in `Lean.Linter.Basic`.
The following now compiles without warning
```lean4
set_option linter.all false in
example : True := by simp [False]
```
Fixes#12559
This PR makes the `omit`, `unusedSectionVars` and `loopingSimpArgs`
linters respect the `linter.all` option:
when `linter.all` is set to false (and the respective linter option is
unset), the linter should not report errors.
Similarly to #12559, these linters should honour the linter.all flag
being set to false. These are all remaining occurrences of this pattern.
This fixes an issue analogous to #12559.
This PR and #12560 fix all occurrences of this pattern. (The only
question is around `RCases.linter.unusedRCasesPattern`: should this also
respect this? I have left this alone for now.)
Co-authored-by: fiforeach <249703130+fiforeach@users.noreply.github.com>
This PR modifies `#eval e` to elaborate `e` with section variables in
scope. While evaluating expressions with free variables is not possible,
this lets `#eval` give a better error message than "unknown identifier."
Example:
```lean
section
variable (n : Nat)
/-- error: Cannot evaluate, contains free variable `n` -/
#guard_msgs in #eval n
end
```
The error is localized to `#eval`. It would be more friendly if the
error were to be placed on uses of free variables.
[Zulip
discussion](https://leanprover.zulipchat.com/#narrow/channel/270676-lean4/topic/Unknown.20identifier.20error.20messages.20for.20.60.23eval.60/near/560864544)
This PR changes the elaboration of the `structure`/`class` commands so
that default values have later fields in context as well. This allows
field defaults to depend on fields that come both before and after them.
While this was already the case for inherited fields to some degree, it
now applies uniformly to all fields. Additionally, when elaborating the
default value for a field, all fields that depend on it are cleared from
the context to avoid situations where the default value depends on
itself.
This addresses an issue reported by Aaron Liu [on
Zulip](https://leanprover.zulipchat.com/#narrow/channel/270676-lean4/topic/default.20structure.20values.20can.20depend.20on.20themselves/near/578014370).
This PR changes "structure-like" terminology to "non-recursive
structure" across internal documentation, error messages, the
metaprogramming API, and the kernel, to clarify Lean's type theory. A
*structure* is a one-constructor inductive type with no indices — these
can be created by either the `structure` or `inductive` commands — and
are supported by the primitive `Expr.proj` projections. Only
*non-recursive* structures have an eta conversion rule. The PR
description contains the APIs that were renamed.
Addresses RFC #5891, which proposed this rename. The change is motivated
by the need to distinguish between `structure`-defined structures,
structures, and non-recursive structures. Especially since #5783, which
enabled the `structure` command to define recursive structures,
"structure-like" has been easy to misunderstand.
Changes:
- Kernel: `is_structure_like()` -> `is_non_rec_structure()`
- `Lean.isStructureLike` -> `Lean.isNonRecStructure`
- `Lean.matchConstStructLike` -> `Lean.matchConstNonRecStructure`
- `Lean.getStructureLikeCtor?` -> `Lean.getNonRecStructureCtor?`
- `Lean.getStructureLikeNumFields` -> `Lean.getNonRecStructureNumFields`
- `Lean.Expr.proj`: extended and corrected documentation (note: despite
the fact that not every projection can be written as a recursor
application, I left in this claim since it seems good to document a
more-restrictive specification, and some users have requested the kernel
be more restrictive in this way)
Closes#5891
This PR changes Lake to only emit `.nobuild` traces (introduced in
#12076) if the normal trace file already exists. This fixes an issue
where a `lake build --no-build` would create the build directory and
thereby prevent a cloud release fetch in a future build.
This PR migrates most remaining tests to the new test suite. It also
completes the migration of directories like `tests/lean/run`, meaning
that PRs trying to add tests to those old directories will now fail.
This PR solves three distinct issues with the handling of
`ite`/`dite`,`decide`.
1) We prevent the simprocs from picking up `noncomputable`, `Classical`
instances, such as `Classical.propDecidable`, when simplifying the
proposition in `ite`/`dite`/`decide`.
2) We fix a type mismatch occurring when the condition/proposition is
unchanged but the `Decidable` instance is simplified.
3) If we rewrite the proposition from `c` to `c'` and the evaluation of
the original instance `Decidable c` gets stuck we try fallback path of
of obtaining `Decidable c'` instance and evaluating it. This matters
when the instance is evaluated via `cbv_eval` lemmas.
---------
Co-authored-by: Claude Opus 4.6 <noreply@anthropic.com>
This PR implements a merge sort algorithm on arrays. It has been
measured to be about twice as fast as `List.mergeSort` for large arrays
with random elements, but for small or almost sorted ones, the list
implementation is faster. Compared to `Array.qsort`, it is stable and
has O(n log n) worst-case cost. Note: There is still a lot of potential
for optimization. The current implementation allocates O(n log n)
arrays, one per recursive call.
---------
Co-authored-by: Claude Opus 4.6 <noreply@anthropic.com>
This PR adjusts the module parser to set the leading whitespace of the
first token to the whitespace up to that token. If there are no actual
tokens in the file, the leading whitespace is set on the final (empty)
EOI token. This ensures that we do not lose the initial whitespace (e.g.
comments) of a file in `Syntax`.
(Tests generated/adjusted by Claude)
Co-authored-by: Claude Sonnet 4.6 <noreply@anthropic.com>
This PR replaces three independent name demangling implementations
(Lean, C++, Python) with a single source of truth in
`Lean.Compiler.NameDemangling`. The new module handles the full
pipeline: prefix parsing (`l_`, `lp_`, `_init_`, `initialize_`,
`lean_apply_N`, `_lean_main`), postprocessing (suffix flags, private
name stripping, hygienic suffix stripping, specialization contexts),
backtrace line parsing, and C exports via `@[export]`.
The C++ runtime backtrace handler now calls the Lean-exported functions
instead of its own 792-line reimplementation. This is safe because
`print_backtrace` is only called from `lean_panic_impl` (soft panics),
not `lean_internal_panic`.
The Python profiler demangler (`script/profiler/lean_demangle.py`) is
replaced with a thin subprocess wrapper around a Lean CLI tool,
preserving the `demangle_lean_name` API so downstream scripts work
unchanged.
**New files:**
- `src/Lean/Compiler/NameDemangling.lean` — single source of truth (483
lines)
- `tests/lean/run/demangling.lean` — comprehensive tests (281 lines)
- `script/profiler/lean_demangle_cli.lean` — `c++filt`-style CLI tool
**Deleted files:**
- `src/runtime/demangle.cpp` (792 lines)
- `src/runtime/demangle.h` (26 lines)
- `script/profiler/test_demangle.py` (670 lines)
Net: −1,381 lines of duplicated C++/Python code.
🤖 Prepared with Claude Code
---------
Co-authored-by: Claude Opus 4.6 <noreply@anthropic.com>
This PR adds tests and a benchmark exercising `instantiateMVars` on
metavariable assignment graphs with nested delayed assignments, in
preparation for optimizing the delayed mvar resolution path.
- `tests/elab/instantiateMVarsShadow.lean`: Two test cases for
correctness when the same fvar is bound to different values at different
scope levels (fvar shadowing and late-bind patterns). A buggy cache
could return a stale result from one scope level in another.
- `tests/elab/instantiateMVarsSharing.lean`: Verifies correct resolution
and object sharing on a graph with nested delayed mvars producing `∀ s,
(s = s → (s = s) ∧ (s = s)) ∧ (s = s)`.
- `tests/elab_bench/delayed_assign.lean`: Constructs an O(n²) delayed
mvar graph (n=700) and measures `instantiateMVars` resolution time,
calibrated to ~1s total elaboration.
🤖 Generated with [Claude Code](https://claude.com/claude-code)
---------
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 moves the universe-level-count check from
`unfold_definition_core` into `is_delta`, establishing the invariant
that if `is_delta` succeeds then `unfold_definition` also succeeds. This
prevents a crash (SIGSEGV or garbled error) that occurred when call
sites in `lazy_delta_reduction_step` unconditionally dereferenced the
result of `unfold_definition` even on a level-parameter-count mismatch.
Additionally, moves the `is_prop` check for theorem types in
`add_theorem` to occur after `check_constant_val`, so the type is
verified to be well-formed before `is_prop` evaluates it. This prevents
`is_prop` from being called on an ill-typed term when a malformed
theorem declaration is supplied.
Fixes#10577.
---------
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 a `set_option cbv.maxSteps N` option that controls the
maximum
number of simplification steps the `cbv` tactic performs. Previously the
limit
was hardcoded to the `Sym.Simp.Config` default of 100,000 with no way
for
users to override it. The option is threaded through `cbvCore`,
`cbvEntry`,
`cbvGoal`, and `cbvDecideGoal`.
🤖 Generated with [Claude Code](https://claude.com/claude-code)
---------
Co-authored-by: Claude Opus 4.6 <noreply@anthropic.com>
This PR moves cbv tests to the correct test directories. `cbv4.lean` is
a
straightforward elaboration test and is moved to `tests/elab/`. The AES
and ARM
load/store tests are performance-oriented stress tests and are moved to
`tests/elab_bench/`.
Co-authored-by: Claude Opus 4.6 <noreply@anthropic.com>
This PR makes the compiler removes arguments to join points that are
void, avoiding a bunch of dead
stores in the bytecode and the initial C (though LLVM was surely able to
optimize these away further
down the line already).
This PR introduces the core HTTP data types: `Request`, `Response`,
`Status`, `Version`, and `Method`. Currently, URIs are represented as
`String` and headers as `HashMap String (Array String)`. These are
placeholders, future PRs will replace them with strict implementations.
This contains the same code as #10478, divided into separate pieces to
facilitate easier review.
The pieces of this feature are:
- Core data structures: #12126
- Headers: #12127
- URI: #12128
- Body: #12144
- H1: #12146
- Server: #12151
- Client:
---------
Co-authored-by: Rob23oba <152706811+Rob23oba@users.noreply.github.com>
This PR skips the noncomputable pre-check in `processDefDeriving` when
the instance type is `Prop`. Since proofs are erased by the compiler,
computability is irrelevant for `Prop`-valued instances.
Previously (since https://github.com/leanprover/lean4/pull/12756),
`deriving instance` would reject instances that transitively depend on
noncomputable definitions, even when the class extends `Prop`. This came
up in mathlib where `Precoverage.IsStableUnderBaseChange` (a `Prop`
class) needs `deriving noncomputable instance` unnecessarily.
🤖 Prepared with Claude Code
Co-authored-by: Claude Opus 4.6 <noreply@anthropic.com>
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>
