From 46ff76aabdf6b3fb3b0187bdd2767463b7ecbc75 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 13 Nov 2025 12:36:01 -0800 Subject: [PATCH] feat: `#grind_lint` refinements (#11166) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit This PR implements the following improvements to the `#grind_lint` command: 1. More informative messages when the number of instances exceeds the minimum threshold. 2. A code action for `#grind_lint inspect` that inserts `set_option trace.grind.ematch.instance true` whenever the number of instances exceeds the minimum threshold. 3. Displaying doc strings for `grind` configuration options in `#grind_lint`. 4. Improve doc strings for `#grind_lint inspect` and `#grind_lint check`. Example: ```lean /-- info: instantiating `Array.filterMap_some` triggers more than 100 additional `grind` theorem instantiations --- info: Array.filterMap_some [thm] instances [thm] Array.filterMap_filterMap ↦ 94 [thm] Array.size_filterMap_le ↦ 5 [thm] Array.filterMap_some ↦ 1 --- info: Try this to display the actual theorem instances: [apply] set_option trace.grind.ematch.instance true in #grind_lint inspect Array.filterMap_some -/ #guard_msgs in #grind_lint inspect Array.filterMap_some ``` --- src/Init/Grind/Lint.lean | 3 ++ src/Lean/Elab/Tactic/ConfigSetter.lean | 13 ++++--- src/Lean/Elab/Tactic/Grind/Config.lean | 8 ++--- src/Lean/Elab/Tactic/Grind/Lint.lean | 25 ++++++++++--- src/Lean/Parser/Command.lean | 2 +- tests/lean/run/grind_lint_1.lean | 50 +++++++++++++++++++++----- 6 files changed, 77 insertions(+), 24 deletions(-) diff --git a/src/Init/Grind/Lint.lean b/src/Init/Grind/Lint.lean index 16d398b82d..52fd9b8cc4 100644 --- a/src/Init/Grind/Lint.lean +++ b/src/Init/Grind/Lint.lean @@ -38,6 +38,7 @@ By default, `#grind_lint` uses the following `grind` configuration: instances := 100 gen := 10 ``` +Consider using `#grind_lint inspect ` to focus on specific theorems. -/ syntax (name := grindLintCheck) "#grind_lint" ppSpace &"check" (ppSpace configItem)* (ppSpace "in" ident+)? : command @@ -51,6 +52,8 @@ Examples: ``` #grind_lint inspect Array.zip_map ``` +You can use `set_option trace.grind.ematch.instance true` to instruct `grind` to display the +actual instances it produces. -/ syntax (name := grindLintInspect) "#grind_lint" ppSpace &"inspect" (ppSpace configItem)* ident+ : command diff --git a/src/Lean/Elab/Tactic/ConfigSetter.lean b/src/Lean/Elab/Tactic/ConfigSetter.lean index dc0bbdbf86..e0b3bb82b4 100644 --- a/src/Lean/Elab/Tactic/ConfigSetter.lean +++ b/src/Lean/Elab/Tactic/ConfigSetter.lean @@ -6,6 +6,7 @@ Authors: Leonardo de Moura module prelude public import Lean.Elab.Command +public import Lean.Elab.Term meta import Lean.Elab.Command public import Lean.Data.KVMap public section @@ -38,21 +39,23 @@ meta def mkConfigSetter (doc? : Option (TSyntax ``Parser.Command.docComment)) -- **Note**: We only support `Nat` and `Bool` fields let fieldIdent : Ident := mkCIdent fieldInfo.fieldName if fieldType.isConstOf ``Nat then - code ← `(if fieldName == $(quote fieldInfo.fieldName) then + code ← `(if fieldName == $(quote fieldInfo.fieldName) then do + Term.addTermInfo' (← getRef) (← mkConstWithLevelParams $(quote fieldInfo.projFn)) return { s with $fieldIdent:ident := (← getNatField) } else $code) else if fieldType.isConstOf ``Bool then - code ← `(if fieldName == $(quote fieldInfo.fieldName) then + code ← `(if fieldName == $(quote fieldInfo.fieldName) then do + Term.addTermInfo' (← getRef) (← mkConstWithLevelParams $(quote fieldInfo.projFn)) return { s with $fieldIdent:ident := (← getBoolField) } else $code) return code let cmd ← `(command| $[$doc?:docComment]? - def $setterName (s : $struct) (fieldName : Name) (val : DataValue) : CoreM $struct := - let getBoolField : CoreM Bool := do + def $setterName (s : $struct) (fieldName : Name) (val : DataValue) : TermElabM $struct := + let getBoolField : TermElabM Bool := do let .ofBool b := val | throwError "`{fieldName}` is a Boolean" return b - let getNatField : CoreM Nat := do + let getNatField : TermElabM Nat := do let .ofNat n := val | throwError "`{fieldName}` is a natural number" return n $code diff --git a/src/Lean/Elab/Tactic/Grind/Config.lean b/src/Lean/Elab/Tactic/Grind/Config.lean index b9419f8d6c..8a4ee90a5b 100644 --- a/src/Lean/Elab/Tactic/Grind/Config.lean +++ b/src/Lean/Elab/Tactic/Grind/Config.lean @@ -14,18 +14,18 @@ namespace Lean.Elab.Tactic.Grind declare_config_getter setConfigField Grind.Config def elabConfigItems (init : Grind.Config) (items : Array (TSyntax `Lean.Parser.Tactic.configItem)) - : CoreM Grind.Config := do + : TermElabM Grind.Config := do let mut config := init for item in items do match item with | `(Lean.Parser.Tactic.configItem| ($fieldName:ident := true)) | `(Lean.Parser.Tactic.configItem| +$fieldName:ident) => - config ← setConfigField config fieldName.getId true + config ← withRef fieldName <| setConfigField config fieldName.getId true | `(Lean.Parser.Tactic.configItem| ($fieldName:ident := false)) | `(Lean.Parser.Tactic.configItem| -$fieldName:ident) => - config ← setConfigField config fieldName.getId false + config ← withRef fieldName <| setConfigField config fieldName.getId false | `(Lean.Parser.Tactic.configItem| ($fieldName:ident := $val:num)) => - config ← setConfigField config fieldName.getId (.ofNat val.getNat) + config ← withRef fieldName <| setConfigField config fieldName.getId (.ofNat val.getNat) | _ => throwErrorAt item "unexpected configuration option" return config diff --git a/src/Lean/Elab/Tactic/Grind/Lint.lean b/src/Lean/Elab/Tactic/Grind/Lint.lean index 3058789aee..729b207740 100644 --- a/src/Lean/Elab/Tactic/Grind/Lint.lean +++ b/src/Lean/Elab/Tactic/Grind/Lint.lean @@ -10,6 +10,7 @@ import Init.Grind.Lint import Lean.Meta.Tactic.Grind.EMatchTheorem import Lean.EnvExtension import Lean.Elab.Tactic.Grind.Config +import Lean.Meta.Tactic.TryThis namespace Lean.Elab.Tactic.Grind builtin_initialize skipExt : SimplePersistentEnvExtension Name NameSet ← @@ -66,7 +67,7 @@ def defaultConfig : Grind.Config := { detailed := 50 } -def mkConfig (items : Array (TSyntax `Lean.Parser.Tactic.configItem)) : CoreM Grind.Config := do +def mkConfig (items : Array (TSyntax `Lean.Parser.Tactic.configItem)) : TermElabM Grind.Config := do elabConfigItems defaultConfig items def mkParams (config : Grind.Config) : MetaM Params := do @@ -100,8 +101,9 @@ def thmsToMessageData (thms : PHashMap Grind.Origin Nat) : MetaM MessageData := /-- Analyzes theorem `declName`. That is, creates the artificial goal based on `declName` type, and invokes `grind` on it. +Returns `true` if the number of instances is above the minimal threshold. -/ -def analyzeEMatchTheorem (declName : Name) (params : Params) : MetaM Unit := do +def analyzeEMatchTheorem (declName : Name) (params : Params) : MetaM Bool := do let info ← getConstInfo declName let mvarId ← forallTelescope info.type fun _ type => do withLocalDeclD `h type fun _ => do @@ -110,18 +112,31 @@ def analyzeEMatchTheorem (declName : Name) (params : Params) : MetaM Unit := do let thms := result.counters.thm let s := sum thms if s > params.config.min then - logInfo m!"{declName} : {s}" + if s >= params.config.instances then + logInfo m!"instantiating `{declName}` triggers more than {s} additional `grind` theorem instantiations" + else + logInfo m!"instantiating `{declName}` triggers {s} additional `grind` theorem instantiations" if s > params.config.detailed then logInfo m!"{declName}\n{← thmsToMessageData thms}" + return s > params.config.min +set_option hygiene false in -- **Note**: to avoid inaccessible name in code-action option name. @[builtin_command_elab Lean.Grind.grindLintInspect] def elabGrindLintInspect : CommandElab := fun stx => liftTermElabM <| withTheReader Core.Context (fun c => { c with maxHeartbeats := 0 }) do let `(#grind_lint inspect $[$items:configItem]* $ids:ident*) := stx | throwUnsupportedSyntax let config ← mkConfig items let params ← mkParams config + let mut addCodeAction := false for id in ids do let declName ← realizeGlobalConstNoOverloadWithInfo id - analyzeEMatchTheorem declName params + if (← analyzeEMatchTheorem declName params) then + addCodeAction := true + if addCodeAction then + unless (← getOptions).getBool `trace.grind.ematch.instance do + let s ← `(command| + set_option trace.grind.ematch.instance true in + $(⟨stx⟩):command) + Tactic.TryThis.addSuggestion (header := "Try this to display the actual theorem instances:") stx { suggestion := .tsyntax s } def getTheorems (prefixes? : Option (Array Name)) : CoreM (List Name) := do let skip := skipExt.getState (← getEnv) @@ -154,7 +169,7 @@ def elabGrindLintCheck : CommandElab := fun stx => liftTermElabM <| withTheReade let decls := decls.toArray.qsort Name.lt for declName in decls do try - analyzeEMatchTheorem declName params + discard <| analyzeEMatchTheorem declName params catch e => logError m!"{declName} failed with {e.toMessageData}" diff --git a/src/Lean/Parser/Command.lean b/src/Lean/Parser/Command.lean index 57abbf5eee..96d61e6732 100644 --- a/src/Lean/Parser/Command.lean +++ b/src/Lean/Parser/Command.lean @@ -781,7 +781,7 @@ def initializeKeyword := leading_parser optional (atomic (ident >> Term.typeSpec >> ppSpace >> Term.leftArrow)) >> Term.doSeq @[builtin_command_parser] def «in» := trailing_parser - withOpen (ppDedent (" in " >> commandParser)) + withOpen (ppDedent (" in" >> ppLine >> commandParser)) /-- Adds a docstring to an existing declaration, replacing any existing docstring. diff --git a/tests/lean/run/grind_lint_1.lean b/tests/lean/run/grind_lint_1.lean index c5307a21b0..43fd8f7703 100644 --- a/tests/lean/run/grind_lint_1.lean +++ b/tests/lean/run/grind_lint_1.lean @@ -22,7 +22,13 @@ error: `Array.swap_swap` is not marked with the `@[grind]` attribute for theorem #guard_msgs in #grind_lint skip Array.getElem_swap -/-- info: Array.range_succ : 47 -/ +/-- +info: instantiating `Array.range_succ` triggers 47 additional `grind` theorem instantiations +--- +info: Try this to display the actual theorem instances: + [apply] set_option trace.grind.ematch.instance true in + #grind_lint inspect Array.range_succ +-/ #guard_msgs in #grind_lint inspect Array.range_succ @@ -30,24 +36,34 @@ error: `Array.swap_swap` is not marked with the `@[grind]` attribute for theorem #grind_lint mute Array.append_assoc -- It is not used during E-matching by `#grind_lint check` and `#grind_lint inspect` -/-- info: Array.range_succ : 22 -/ +/-- +info: instantiating `Array.range_succ` triggers 22 additional `grind` theorem instantiations +--- +info: Try this to display the actual theorem instances: + [apply] set_option trace.grind.ematch.instance true in + #grind_lint inspect Array.range_succ +-/ #guard_msgs in #grind_lint inspect Array.range_succ /-- -info: Array.range_succ : 22 +info: instantiating `Array.range_succ` triggers 22 additional `grind` theorem instantiations --- -info: Array.range'_succ : 17 +info: instantiating `Array.range'_succ` triggers 17 additional `grind` theorem instantiations +--- +info: Try this to display the actual theorem instances: + [apply] set_option trace.grind.ematch.instance true in + #grind_lint inspect Array.range_succ Array.range'_succ -/ #guard_msgs in #grind_lint inspect Array.range_succ Array.range'_succ /-- -info: Array.extract_empty : 100 +info: instantiating `Array.extract_empty` triggers more than 100 additional `grind` theorem instantiations --- -info: Array.filterMap_some : 100 +info: instantiating `Array.filterMap_some` triggers more than 100 additional `grind` theorem instantiations --- -info: Array.range_succ : 22 +info: instantiating `Array.range_succ` triggers 22 additional `grind` theorem instantiations -/ #guard_msgs in #grind_lint check (min := 20) (detailed := 200) in Array @@ -55,9 +71,25 @@ info: Array.range_succ : 22 #grind_lint skip Array.extract_empty -- `#grind_lint check` skips it from now on /-- -info: Array.filterMap_some : 100 +info: instantiating `Array.filterMap_some` triggers more than 100 additional `grind` theorem instantiations --- -info: Array.range_succ : 22 +info: instantiating `Array.range_succ` triggers 22 additional `grind` theorem instantiations -/ #guard_msgs in #grind_lint check (min := 20) (detailed := 200) in Array + +/-- +info: instantiating `Array.filterMap_some` triggers more than 100 additional `grind` theorem instantiations +--- +info: Array.filterMap_some +[thm] instances + [thm] Array.filterMap_filterMap ↦ 94 + [thm] Array.size_filterMap_le ↦ 5 + [thm] Array.filterMap_some ↦ 1 +--- +info: Try this to display the actual theorem instances: + [apply] set_option trace.grind.ematch.instance true in + #grind_lint inspect Array.filterMap_some +-/ +#guard_msgs in +#grind_lint inspect Array.filterMap_some