max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2
lean4-htt/tests/elab/extraModUses.lean
Kyle Miller 047f6aaf89
feat: efficient tactic configuration elaborators and configurability (#13651) 
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.
2026-05-14 17:20:57 +00:00

341 lines
7 KiB
Text
Raw Permalink Blame History

module
import all Lean.ExtraModUses
public meta import Lean.Elab.Tactic.Basic
/-!
# Test for module dependencies described by ExtraModUses
-/
meta def resetExtraModUses : Lean.CoreM Unit := do
Lean.modifyEnv (Lean.PersistentEnvExtension.setState Lean.extraModUses · ⟨[], ∅⟩)
Lean.modifyEnv (Lean.PersistentEnvExtension.setState Lean.isExtraRevModUseExt · ⟨[], ()⟩)
meta def Lean.ExtraModUse.toImport (e : ExtraModUse) : Import :=
{ e with }
meta def showExtraModUses : Lean.CoreM Unit := do
Lean.logInfo m!"Entries: {toString <| (Lean.extraModUses.getEntries (← Lean.getEnv)).map (·.toImport)}\n\
Is rev mod use: {!(Lean.isExtraRevModUseExt.getEntries (← Lean.getEnv)).isEmpty}"
/-!
Test that the `resetExtraModUses` + `showExtraModUses` pair is working.
-/
#eval resetExtraModUses
/--
info: Entries: []
Is rev mod use: false
-/
#guard_msgs in #eval showExtraModUses
/-!
Notation being used in a command is recorded (here `«term_+_»` from Init.Notation)
-/
#eval resetExtraModUses
example := 3 + 3
/--
info: Entries: [import Init.Notation]
Is rev mod use: false
-/
#guard_msgs in #eval showExtraModUses
/-!
Declarations referenced using double-quoted names are recorded.
-/
#eval resetExtraModUses
def test1 := ``List.sum
/--
info: Entries: [import Init.Data.List.Basic]
Is rev mod use: false
-/
#guard_msgs in #eval showExtraModUses
/-!
`recommended_spelling` records a dependency.
-/
#eval resetExtraModUses
recommended_spelling "id" for "id" in [id]
/--
info: Entries: [import Init.Core, import Init.Prelude]
Is rev mod use: false
-/
#guard_msgs in #eval showExtraModUses
/-!
`syntax` records a dependency for the syntax category
(here Lean.Parser.Category.Term from Init.Notation).
-/
#eval resetExtraModUses
syntax "hi" : term
/--
info: Entries: [public import Init.Notation]
Is rev mod use: false
-/
#guard_msgs in #eval showExtraModUses
/-!
Term macro expansions are tracked (here `«term_+_»` from Init.Notation)
-/
macro "macro1" : term => `(3 + 3)
#eval resetExtraModUses
def test2 := macro1
/--
info: Entries: [import Init.Notation]
Is rev mod use: false
-/
#guard_msgs in #eval showExtraModUses
/-!
Tactic macro expansions are tracked (here `Lean.Parser.Tactic.tacticTrivial` from Init.Tactics)
-/
macro "macro2" : tactic => `(tactic| trivial)
#eval resetExtraModUses
public meta def test3 : True := by macro2
/--
info: Entries: [import Init.Tactics]
Is rev mod use: false
-/
#guard_msgs in #eval showExtraModUses
/-!
Tactic configuration structures are recorded.
-/
#eval resetExtraModUses
public def test4 : True := by simp +contextual
/--
info: Entries: [import Init.Tactics]
Is rev mod use: false
-/
#guard_msgs in #eval showExtraModUses
/-!
`omega` introduces a dependency on `Init.Omega`.
-/
#eval resetExtraModUses
public def test5 : Eq 1 1 := by omega
/--
info: Entries: [import Init.Tactics, import Init.Omega]
Is rev mod use: false
-/
#guard_msgs in #eval showExtraModUses
/-!
References from `@[deprecated]` are tracked (here `Nat.add` from Init.Prelude)
-/
#eval resetExtraModUses
@[deprecated Nat.add "we decided to shorten the name" (since := "1010-10-10")]
def NaturalNumber.additionOperator := Nat.add
/--
info: Entries: [import Init.Notation, import Init.Prelude]
Is rev mod use: false
-/
#guard_msgs in #eval showExtraModUses
/-!
References from `@[grind]` are tracked (here `List.append` from Init.Prelude)
-/
#eval resetExtraModUses
attribute [grind =] List.append
/--
info: Entries: [import Init.Grind.Attr, public import Init.Prelude]
Is rev mod use: false
-/
#guard_msgs in #eval showExtraModUses
/-!
Local attribute applications are tracked as private.
-/
#eval resetExtraModUses
attribute [local grind =] List.append
/--
info: Entries: [import Init.Grind.Attr, import Init.Prelude]
Is rev mod use: false
-/
#guard_msgs in #eval showExtraModUses
/-!
Coercion instances are recorded as dependencies.
-/
#eval resetExtraModUses
public def test6 : Option Bool := false
/--
info: Entries: [import Init.Data.Option.Coe, import Init.Coe]
Is rev mod use: false
-/
#guard_msgs in #eval showExtraModUses
/-!
Simp theorems (especially defeq ones) are tracked (here `Nat.pow_succ` from Init.Data.Nat.Basic)
-/
#eval resetExtraModUses
def test7 : 2 ^ 8 = 256 := by simp [Nat.pow_succ]
/--
info: Entries: [import Init.Tactics, import Init.Data.Nat.Lemmas, import Init.Data.Nat.Basic, import Init.SimpLemmas, import Init.Notation]
Is rev mod use: false
-/
#guard_msgs in #eval showExtraModUses
/-!
`register_error_explanation` creates a dependency on `Lean.ErrorExplanation`.
-/
#eval resetExtraModUses
/-- This error never occurs. If you still get it, something went wrong, sorry -/
register_error_explanation lean.never {
summary := "Not an error"
sinceVersion := "never"
}
/--
info: Entries: [meta import Lean.ErrorExplanation]
Is rev mod use: false
-/
#guard_msgs in #eval showExtraModUses
/-!
The syntax node kind in `syntax` declarations get recorded as a `meta` dependency.
-/
#eval resetExtraModUses
syntax "test_me " Lean.Parser.Term.ident : term
/--
info: Entries: [public meta import Lean.Parser.Term, public import Init.Notation]
Is rev mod use: false
-/
#guard_msgs in #eval showExtraModUses
/-!
The categories in `syntax` declarations get recorded as a `meta` dependency.
-/
#eval resetExtraModUses
syntax "test_me " rcasesPat : term
/--
info: Entries: [public import Init.RCases, public import Init.Notation]
Is rev mod use: false
-/
#guard_msgs in #eval showExtraModUses
/-!
The quotation parser gets recorded as a `meta` dependency.
-/
#eval resetExtraModUses
def test8 : Lean.MacroM Lean.Syntax := `(Lean.Parser.Command.declaration| def a := 5)
/--
info: Entries: [import Init.Notation, import Init.Coe, meta import Lean.Parser.Command]
Is rev mod use: false
-/
#guard_msgs in #eval showExtraModUses
/-!
Elaboration attributes add dependency on the syntax node kind
(here `Lean.Parser.Tactic.done` from Init.Tactics).
-/
public meta def myElab : Lean.Elab.Tactic.Tactic := fun _ => pure ()
#eval resetExtraModUses
attribute [tactic Lean.Parser.Tactic.done] myElab
/--
info: Entries: [public import Init.Tactics]
Is rev mod use: false
-/
#guard_msgs in #eval showExtraModUses
/-!
Similarly with formatters...
-/
public meta def myFormatter : Lean.PrettyPrinter.Formatter := fun _ => pure ()
#eval resetExtraModUses
attribute [formatter Lean.Parser.Tactic.done] myFormatter
/--
info: Entries: [public import Init.Tactics]
Is rev mod use: false
-/
#guard_msgs in #eval showExtraModUses
/-!
... and parenthesizers
-/
public meta def myParenthesizer : Lean.PrettyPrinter.Parenthesizer := fun _ => pure ()
#eval resetExtraModUses
attribute [parenthesizer Lean.Parser.Tactic.done] myParenthesizer
/--
info: Entries: [public import Init.Tactics]
Is rev mod use: false
-/
#guard_msgs in #eval showExtraModUses
/-! `inferInstanceAs` inputs not included in output. -/
#eval resetExtraModUses
def MyNat := Nat
instance : Max MyNat := inferInstanceAs (Max Nat)
/--
info: Entries: [import Init.Data.Nat.Basic]
Is rev mod use: false
-/
#guard_msgs in #eval showExtraModUses
Reference in a new issue View git blame Copy permalink