feat: #grind_lint refinements (#11166)

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

@@ -38,6 +38,7 @@ By default, `#grind_lint` uses the following `grind` configuration:
   instances    := 100
   gen          := 10
 ```
+Consider using `#grind_lint inspect <thm>` 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
 

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

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
 

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}"
 

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.

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