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 wraps the top-level command parser with `withPosition` to
enforce indentation in `by` blocks, combined with an empty-by fallback
for better error messages.
This subsumes #3215 (which introduced `withPosition commandParser` but
without the empty-by fallback). It is also related to #9524, which
explores elaboration with empty tactic sequences — this PR reuses that
idea for the empty-by fallback, so that a `by` not followed by an
indented tactic produces an elaboration error (unsolved goals) rather
than a parse error.
**Changes:**
- `topLevelCommandParserFn` now uses `(withPosition commandParser).fn`,
setting the saved position at the start of each top-level command
- `tacticSeqIndentGt` gains an empty tactic sequence fallback
(`pushNone`) so that missing indentation produces an elaboration error
(unsolved goals) instead of a parse error
- `isEmptyBy` in `goalsAt?` removed: with strict `by` indentation, empty
`by` blocks parse successfully via `pushNone` (producing empty nodes)
rather than producing `.missing` syntax, making the `isEmptyBy` check
dead code. The `isEmpty` helper in `isSyntheticTacticCompletion`
continues to work correctly because it handles both `.missing` and empty
nodes from `pushNone` (via the vacuously-true `args.all isEmpty` on
`#[]`)
- Test files updated to indent `by` blocks and expression continuations
that were previously at column 0
**Behavior:**
- Top-level `by` blocks now require indentation (column > 0 for commands
at column 0)
- Commands indented inside `section` require proofs to be indented past
the command's column
- `#guard_msgs in example : True := by` works because tactic indentation
is checked against the outermost command's column
- Expression continuations (not just `by`) must also be indented past
the command, which is slightly more strict but more consistent
- `have : True := by` followed by a dedent now correctly puts `this` in
scope in the outer tactic block (the `have` is structurally complete
with an unsolved-goal error, rather than a parse error)
**Code changes observed in practice (lean4 test suite + Mathlib):**
- `by` blocks: top-level `theorem ... := by` / `decreasing_by` followed
by tactics at column 0 must be indented
- `variable` continuations: `variable {A : Type*} [Foo A]\n{B : Type*}`
where the second line starts at column 0 must be indented (most common
category in Mathlib)
- Expression continuations: `def f : T :=\nexpr` or `#synth Foo\n[args]`
where the body/arguments start at column 0
- Structure literals: `.symm\n{ toFun := ...` where the struct literal
starts at column 0
🤖 Generated with [Claude Code](https://claude.com/claude-code)
Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
---------
Co-authored-by: Claude Opus 4.6 <noreply@anthropic.com>
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 speeds up some benchmarks when run as tests by lowering their
workload. It also stops testing some of the more expensive benchmarks
that can't be easily made smaller.
This PR adds per-result `contextDependent` tracking to `Sym.Simp.Result`
and splits the simplifier cache into persistent (context-independent)
and transient (context-dependent, cleared on binder entry). This
replaces the coarse `wellBehavedMethods` flag.
Key changes:
- Add `contextDependent : Bool := false` to `Result.rfl` and
`Result.step`
- Split `State.cache` into `persistentCache` and `transientCache`
- Remove `wellBehavedMethods` from `Methods`
- Replace `withoutModifyingCacheIfNotWellBehaved` with
`withFreshTransientCache`
- Change `DischargeResult` to an inductive (`.failed`/`.solved`)
- Add `dischargeAssumption` (context-dependent discharger for testing)
- Add `sym.simp.debug.cache` trace class
- Propagate `contextDependent` through all combinators (congruence,
transitivity, control flow, arrows, rewriting)
- Add `mkRflResult`/`mkRflResultCD` to avoid dynamic allocation of rfl
results
- Fix `isRfl` to ignore `contextDependent` (was silently broken by the
extra field)
Propagation invariant: when combining sub-results, `cd` is the
disjunction of ALL sub-results' flags — including `.rfl` results. If
`simp` returned `.rfl (contextDependent := true)`, it means `simp` might
take a completely different code path in another local context, so all
downstream results must be marked context-dependent.
---------
Co-authored-by: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
The tests need to run with certain environment variables set that only
cmake really knows and that differ between stages. Cmake could just set
the variables directly when running the tests and benchmarks, but that
would leave no good way to manually run a single benchmark. So cmake
generates some stage-specific scripts instead that set the required
environment variables.
Previously, those scripts were sourced directly by the individual
`run_*` scripts, so the env scripts of different stages would overwrite
each other. This PR changes the setup so they can instead be generated
next to each other. This also simplifies the `run_*` scripts themselves
a bit, and makes `tests/bench/build` less of a hack.
This PR adds a benchmark that measures `simp` performance on string
literal equality and inequality for various string lengths and
difference positions.
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 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 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.
