feat: efficient tactic configuration elaborators and configurability

[kmill]

This PR replaces the previous tactic configuration system with a significantly more efficient one that supports custom configuration syntaxes and processing. 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., namedArguments) 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 the ability to set 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 proper (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 handle its functionality.
• The module Lean.Elab.Tactic.Config is deprecated and will be removed. Import Lean.Elab.ConfigEval instead.

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.

---

The #13426 draft PR includes some LSP modifications to support completions for simp user configuration options.

[kmill]

!bench

[leanprover-radar]

Benchmark results for 9873567 against 25ec7e5 are in. There are significant results. @kmill

• 🟥 build//instructions: +3.4G (+0.03%)

Large changes (4✅, 9🟥)

• 🟥 build/module/Lean.Elab.Tactic.Grind.Main//instructions: +12.9G (+86.99%)
• ✅ build/module/Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas.Expr//instructions: -6.9G (-6.40%)
• ✅ elab/mut_rec_wf//instructions: -3.0G (-11.19%)
• ✅ elab/mut_rec_wf//task-clock: -297ms (-13.14%)
• ✅ elab/mut_rec_wf//wall-clock: -296ms (-14.36%)
• 🟥 mvcgen/sym/PurePrecond/400/vcgen//wall-clock: +60ms (+26.67%)
• 🟥 mvcgen/sym/PurePrecond/700/vcgen//wall-clock: +890ms (+268.07%)
• 🟥 size/all/.c//lines: +166.9k (+1.48%)
• 🟥 size/all/.ir//bytes: +5MiB (+1.35%)
• 🟥 size/all/.olean.private//bytes: +9MiB (+0.77%)
• 🟥 size/compile/.out//bytes: +21MiB (+1.05%)
• 🟥 size/install//bytes: +21MiB (+0.71%)
• 🟥 size/libleanshared.so//bytes: +2MiB (+1.07%)

Medium changes (7✅, 5🟥)

• ✅ build/module/Init.Data.Array.Basic//instructions: -1.7G (-13.39%) (reduced significance based on absolute threshold)
• ✅ build/module/Init.Data.List.ToArray//instructions: -1.0G (-4.85%) (reduced significance based on absolute threshold)
• ✅ build/module/Lean.Elab.MutualInductive//instructions: -1.1G (-3.31%) (reduced significance based on absolute threshold)
• 🟥 build/module/Lean.Elab.Tactic.BVDecide.Frontend.Attr//instructions: +1.3G (+55.72%) (reduced significance based on absolute threshold)
• 🟥 build/module/Lean.Elab.Tactic.Lets//instructions: +1.3G (+38.70%) (reduced significance based on absolute threshold)
• 🟥 build/module/Lean.Elab.Tactic.NormCast//instructions: +3.4G (+37.61%) (reduced significance based on absolute threshold)
• ✅ build/module/Lean.Meta.Sym.Pattern//instructions: -1.9G (-7.92%) (reduced significance based on absolute threshold)
• ✅ build/module/Std.Data.DTreeMap.Internal.Queries//instructions: -1.3G (-6.50%) (reduced significance based on absolute threshold)
• ✅ build/module/Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Expr//instructions: -2.6G (-3.87%) (reduced significance based on absolute threshold)
• ✅ build/module/Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.Mul//instructions: -1.3G (-5.71%) (reduced significance based on absolute threshold)
• 🟥 build/stat/imported bytes//bytes: +2GiB (+1.20%)
• 🟥 build/stat/imported modules//amount: +13.3k (+1.22%)

Small changes (233✅, 30🟥)

Too many entries to display here. View the full report on radar instead.

[mathlib-lean-pr-testing]

Mathlib CI status (docs):

• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 25ec7e5b0f6fb481f19d51843a2beaec92e06a8b --onto dae325700c89e23c453b1d6d5ed5432d87880062. You can force Mathlib CI using the force-mathlib-ci label. (2026-05-05 19:56:25)
• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 25ec7e5b0f6fb481f19d51843a2beaec92e06a8b --onto 8ebd294673e9e0397c5ccf2ab9a65b0f3e937918. You can force Mathlib CI using the force-mathlib-ci label. (2026-05-06 09:47:46)
• 💥 Mathlib branch lean-pr-testing-13651 build failed against this PR. (2026-05-06 16:29:35) View Log
• 💥 Mathlib branch lean-pr-testing-13651 build failed against this PR. (2026-05-06 21:00:05) View Log
• 💥 Mathlib branch lean-pr-testing-13651 build failed against this PR. (2026-05-09 02:26:16) View Log
• 💥 Mathlib branch lean-pr-testing-13651 build failed against this PR. (2026-05-11 18:29:11) View Log

[leanprover-bot]

Reference manual CI status:

• ❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase 25ec7e5b0f6fb481f19d51843a2beaec92e06a8b --onto 3fc99eef102549c743c6c63547983319bfae6f01. You can force reference manual CI using the force-manual-ci label. (2026-05-05 19:56:27)
• ❗ Reference manual CI can not be attempted yet, as the nightly-testing-2026-05-06 tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto nightly-with-manual, reference manual CI should run now. You can force reference manual CI using the force-manual-ci label. (2026-05-06 16:14:46)
• 💥 Reference manual branch lean-pr-testing-13651 build failed against this PR. (2026-05-09 02:26:45) View Log
• 🟡 Reference manual branch lean-pr-testing-13651 build against this PR didn't complete normally. (2026-05-09 02:26:57) View Log