047f6aaf89
This PR replaces the previous tactic configuration system with a
significantly more efficient one that supports custom configuration
syntaxes and processing. On a simple benchmark, configuration evaluation
takes 6.2% of the time it used to. The `declare_config_elab` command
generates a configuration elaborator that now directly constructs
configuration objects; previously it relied on `Meta.evalExpr'`, which
involved running a configuration through the full term elaboration,
compilation, and evaluation processes. The generated configuration
elaborators now also have the capability to do direct `Syntax`
evaluation in common cases, skipping term elaboration. Furthermore, the
elaborator accepts configurations more liberally: any user-defined
syntax that has the form of an `optConfig`-style configuration or
configuration item (including, e.g., `namedArgument`s) is accepted.
Import `Lean.Elab.ConfigEval` to use the system; see this module for
some documentation in addition to the docstrings in
`Lean.Elab.ConfigEval.Commands`. Furthermore, the `simp` tactic now also
has `(user.optionName := ...)` user configuration options, which can be
declared using a global `tactic.simp.user.optionName` option; use
`getUserConfigOption` and `withUserConfig` to access and set these in
metaprograms.
Other features:
- `declare_config_elab` creates a function that exposes an `init`
parameter for the configuration that will be modified. It also now has a
`where` clause, enabling defining custom handlers for specific keys.
- Elaborators can be given additional binders, to make parameterized
elaborators. This is used by `simp` and `grind ` to support multiple
default configurations with the correct expected type for `(config :=
...)` elaboration.
- The `EvalTerm` class supports direct evaluation of `Syntax`, skipping
term elaboration. The system will attempt to automatically derive this
class when generating the elaborator.
- In case `EvalTerm` does not recognize the term, then the syntax is
elaborated to an expression and an `EvalExpr` instance is applied to
evaluate the expression. The system will similarly automatically derive
these instances if possible.
- Automatic derivation is *transitive*. It is able to seek instances
through other instances; e.g. if it needs an `EvalTerm (List T)`
instance it will be able to reduce this to seeking an `EvalTerm T`
instance.
- The system is designed to be flexible, and the various components can
be combined to construct a configuration elaborator. There are also now
`declare_core_config_elab` and `declare_term_config_elab` for
conveniently generating elaborators for `CoreM` and `TermElabM`. The
difference is that the first takes an explicit flag for whether to log
exceptions, and the second uses the current `errToSorry` state.
**Warning:** if you use the `TermElabM` one from `TacticM`, it will be
unaware of the current `recover` state. The only differences between
these macros are the ways error recovery is handled per monad.
Other changes:
- `#reduce` tactic configuration now makes use of this system and has
more options
- The module `Lean.Elab.Tactic.ConfigSetter` is removed; the
`declare_config_elab`-family macros subsume its functionality.
- The module `Lean.Elab.Tactic.Config` is deprecated and will be
removed; migration notes appear in the module docs there. Import
`Lean.Elab.ConfigEval` instead.
- One of the mvcgen benchmarks got significantly slower, but it turned
out to be caused by the new tactic configuration elaboration no longer
resetting the MetaM caches. Adding an explicit `resetCache` into the
test driver fixed the benchmark.
### Notes for metaprogram authors
If you are using the module system, you just need a `meta import
Lean.Elab.ConfigEval` to use the macros, and it should serve as a
drop-in replacement to the previous system so long as
1. your configuration type is a `structure` with no parameters, indices,
or universes (only `Type` is supported);
2. default values are self-contained and not dependent on other fields;
and
3. all fields have types that are composed from `Option`, `List`,
`Array`, `String`, `DataValue`, and inductive types in `Type` with no
parameters or indices, whose fields are similarly composed.
The macros synthesize a self-contained configuration elaboration
procedure, analyzing the `EvalTerm` and `EvalExpr` instances that are
currently available or can be automatically derived. These are the
components of the system:
- `EvalTerm` instances provide `Term → TermElabM α` functions for
evaluation of raw syntax; these handle the common cases where an option
value is a identifier, application, or other simple expression. They are
responsible for adding TermInfo when info is enabled, to support hovers.
One can invoke derivation of a `EvalTerm T` instance with the
`ensure_eval_term_instance T` command (after `open scoped
Lean.Elab.ConfigEval`).
- `EvalExpr` instances provide `Expr → TermElabM α` functions for
evaluation of elaborated expressions; these handle cases where an option
value may require reduction to evaluate. Similarly, one can invoke
derivation of an `EvalExpr T` instance with the
`ensure_eval_expr_instance T` command. If needed, there's also
`derive_eval_expr_instance_using_meta_eval T` for creating a
`Meta.evalExpr'`-based evaluator.
- Functions like `ConfigEval.evalExprWithElab` compose `EvalTerm` and
`EvalExpr` instances into a single procedure that first attempts
`EvalTerm`, and, if that fails, applies the standard term elaborator and
then attempts `EvalExpr`. This way term elaboration can be skipped in
all but uncommon cases.
- Configuration item interpretation is through `ConfigEval.foldConfigM`,
which is a procedure with a lax specification for what counts as a
configuration item, calling the provided function on each recognized
configuration item. The idea is:
- Null nodes are lists of configurations
- One-argument nodes are considered to be wrappers like `optConfig` or
`configItem`
- Two-argument nodes of the form `("+"<|>"-") (atom<|>ident)` are
considered to be boolean options
- Five-argument nodes of the form `"(" (atom<|>ident) ":=" syntax ")"`
are considered to be general configuration items. (It only checks for
the presence of `(` and that there are two-to-five arguments.)
- Bare atoms are considered to be positive boolean options
- Configuration evaluation then uses `EvalConfigItem.set` on each item
produced by the fold, for an `EvalConfigItem` structure defined for the
given configuration type. The `def_eval_config_item` command can be used
to generate this structure. It analyzes which `EvalTerm` and `EvalExpr`
instances exist and derives missing ones, then builds an efficient
procedure to process configuration items and apply evaluators.
- Lastly, there are the `declare_core_config_elab`,
`declare_term_config_elab`, `declare_config_elab`, and
`declare_command_config_elab` macros for conveniently running the
`def_eval_config_item` command and constructing a self-contained
elaboration function.
The derivation procedures analyze which `EvalTerm`/`EvalExpr` instances
already exist and only derive the "leaf" instances that are necessary to
construct `EvalTerm` and `EvalExpr` instances. The derived instances are
made `private local` — since configuration elaborators are meant to be
self-contained, we decided not to let the additional instances be a side
effect of the macros. The instances can be globally added by manually
using the `ensure_*` commands.
The macros support making parameterized elaborators with arbitrary
additional binders. See `make_elab_grind_config` and
`make_elab_simp_config` in core Lean for examples of generating a single
elaborator that's used with multiple default value configurations.
To see how to create a key handler that matches all configuration keys
with a given prefix, see `make_elab_simp_config`.
There is a todo item at `Lean.Elab.ConfigEval.ReflectConfigItems` for
reflecting configurations back to syntax, which is not yet supported.
### Performance evaluation
A legacy configuration parser was temporarily added to
`Lean.Elab.Tactic.Grind.Config` using `declare_term_config_elab_legacy
elabGrindConfigLegacy Grind.Config`, and then this file was used for
measuring elaboration time:
```lean
import Lean
open Lean Elab Meta Tactic Parser
def cfgs : Array Syntax := Unhygienic.run do
return #[
← `(Tactic.optConfig| ),
← `(Tactic.optConfig| +clean),
← `(Tactic.optConfig| +trace +markInstances -lookahead -useSorry),
← `(Tactic.optConfig| (trace := true) (markInstances := true) (lookahead := false) (useSorry := false)),
← `(Tactic.optConfig| -trace (splits := 20) +revert (maxSuggestions := some 3) (ematch := 2)),
← `(Tactic.optConfig| (gen := 5) -reducible +splitImp -funCC),
← `(Tactic.optConfig| (config := { trace := true, lookahead := false, maxSuggestions := some 3 })),
]
def testGrindElab (cfgs : Array Syntax) (n : Nat) : TacticM Unit := do
profileitM Exception "test grind elab" (← getOptions) do
let mut ematch := 0
for _ in [0:n] do
for cfg in cfgs do
let c ← Tactic.elabGrindConfig cfg
ematch := ematch + c.ematch
logInfo m!"sum = {ematch}"
def testGrindElabLegacy (cfgs : Array Syntax) (n : Nat) : TacticM Unit := do
profileitM Exception "test grind elab legacy" (← getOptions) do
let mut ematch := 0
for _ in [0:n] do
for cfg in cfgs do
let c ← Tactic.elabGrindConfigLegacy cfg
ematch := ematch + c.ematch
logInfo m!"sum = {ematch}"
def runTest (info : Bool) (test : TacticM Unit) : TermElabM Unit := do
withEnableInfoTree info do
let mvar ← mkFreshExprMVar none
discard <| Tactic.run mvar.mvarId! test
set_option maxHeartbeats 0
set_option profiler true
set_option profiler.threshold 1
def iters : Nat := 1000
#eval runTest false <| testGrindElab cfgs iters
#eval runTest true <| testGrindElab cfgs iters
#eval runTest false <| testGrindElabLegacy cfgs iters
#eval runTest true <| testGrindElabLegacy cfgs iters
```
A representative output is
```
test grind elab took 315ms
test grind elab took 333ms
test grind elab legacy took 5.22s
test grind elab legacy took 5.33s
```
Computing `(315.0 + 333.0) / (5220 + 5330)` and rounding up to the
nearest tenth gives the 6.2% figure.
---
The #13426 draft PR includes some LSP modifications to support
completions for `simp` user configuration options.
86 lines
3.9 KiB
Text
86 lines
3.9 KiB
Text
/-
|
||
Copyright (c) 2026 Lean FRO LLC. All rights reserved.
|
||
Released under Apache 2.0 license as described in the file LICENSE.
|
||
Authors: Sebastian Graf
|
||
-/
|
||
module
|
||
public import Lean.Meta
|
||
import Lean.Elab
|
||
import Lean.Meta.Sym.Simp.Theorems
|
||
|
||
open Lean Parser Meta Elab Tactic Sym
|
||
|
||
def timeItMs (k : MetaM α) : MetaM (α × UInt64) := do
|
||
let startTime ← IO.monoNanosNow
|
||
let a ← k
|
||
let endTime ← IO.monoNanosNow
|
||
let ms := (endTime - startTime).toFloat / 1000000.0
|
||
return (a, ms.toUInt64)
|
||
|
||
/-- Helper function for executing a tactic `k` for solving `$(goal) n`. -/
|
||
def driver (goal : Name) (unfold : List Name) (n : Nat) (discharge : MetaM (TSyntax `tactic)) (k : MVarId → MetaM (List MVarId)) : MetaM Unit := do
|
||
let mvar ← mkFreshExprMVar (mkApp (mkConst goal) (mkNatLit n))
|
||
let (mvarId, _unfoldMs) ← timeItMs do SymM.run do
|
||
let mvarId ← preprocessMVar mvar.mvarId!
|
||
let eqnss ← unfold.toArray
|
||
|>.push goal
|
||
|>.mapM fun n => getEqnsFor? n
|
||
let thms := eqnss.flatMap (fun o => o.getD #[])
|
||
match (← Sym.simpGoal mvarId (← Sym.mkMethods thms)) with
|
||
| .goal mvarId => return mvarId
|
||
| .noProgress => throwError "No progress when simping {mvarId}!"
|
||
| .closed => throwError "Simp closed goal {mvarId}"
|
||
-- IO.println s!"time spent unfolding: {_unfoldMs} ms"
|
||
let (mvarIds, ms) ← timeItMs do k mvarId
|
||
let discharge ← discharge
|
||
let dischargePp ← PrettyPrinter.ppTactic discharge
|
||
let dischargeMs? ← OptionT.run <| do
|
||
guard !mvarIds.isEmpty
|
||
Prod.snd <$> timeItMs do
|
||
for mvarId in mvarIds do
|
||
let ([], _) ← Lean.Elab.runTactic mvarId discharge.raw {} {}
|
||
| throwError "{dischargePp} failed to solve {mvarId}"
|
||
let (expr, instMs) ← timeItMs (instantiateMVars mvar)
|
||
-- Emulate the shareCommonPreDefs step before sending the term to the kernel.
|
||
-- If we don't do this, kernel checking time balloons.
|
||
let expr ← SymM.run (shareCommon expr)
|
||
let (_, kernelMs) ← timeItMs (checkWithKernel expr)
|
||
let label := s!"{goal.getPrefix}({n}):"
|
||
let pad := "".pushn ' ' (24 - min label.length 24)
|
||
let mut msg := s!"{label}{pad}{ms} ms"
|
||
if let some dischargeMs := dischargeMs? then
|
||
msg := msg ++ s!", {mvarIds.length} VCs by {dischargePp}: {dischargeMs} ms"
|
||
else
|
||
msg := msg ++ s!", {mvarIds.length} VCs"
|
||
if instMs > 1000 then
|
||
msg := msg ++ s!", instantiate > 1000ms: {instMs} ms"
|
||
msg := msg ++ s!", kernel: {kernelMs} ms"
|
||
IO.println msg
|
||
|
||
def solveUsingTactic (goal : Name) (unfold : List Name) (n : Nat) (solve : MetaM (TSyntax `tactic)) (discharge : MetaM (TSyntax `tactic)) : MetaM Unit := do
|
||
driver goal unfold n discharge fun mvarId => do
|
||
let (mvarIds, _) ← Lean.Elab.runTactic mvarId (← solve).raw {} {}
|
||
return mvarIds
|
||
|
||
/--
|
||
Solves a goal of the form `goal n` using the given tactic, where `n` ranges over `sizes`.
|
||
`unfold` is a list of `simp` lemmas to apply in order to unfold `goal n`.
|
||
For many benchmarks, this is `[step, loop]`.
|
||
-/
|
||
public def runBenchUsingTactic (goal : Name) (unfold : List Name) (solve : MetaM (TSyntax `tactic)) (discharge : MetaM (TSyntax `tactic)) (sizes : List Nat) : MetaM Unit := do
|
||
for n in sizes do
|
||
resetCache
|
||
solveUsingTactic goal unfold n solve discharge
|
||
|
||
def solveUsingSym (goal : Name) (unfold : List Name) (n : Nat) (solve : MVarId → SymM (List MVarId)) (discharge : MetaM (TSyntax `tactic)) : MetaM Unit := do
|
||
driver goal unfold n discharge fun mvarId => SymM.run do solve mvarId
|
||
|
||
/--
|
||
Solves a goal of the form `goal n` using a `SymM` procedure, where `n` ranges over `sizes`.
|
||
`unfold` is a list of `simp` lemmas to apply in order to unfold `goal n`.
|
||
For many benchmarks, this is `[step, loop]`.
|
||
-/
|
||
public def runBenchUsingSym (goal : Name) (unfold : List Name) (solve : MVarId → SymM (List MVarId)) (discharge : MetaM (TSyntax `tactic)) (sizes : List Nat) : MetaM Unit := do
|
||
for n in sizes do
|
||
resetCache
|
||
solveUsingSym goal unfold n solve discharge
|