chore: profile grind satellite solvers (#9246)

src/Lean/Meta/Tactic/Grind/Arith/CommRing/EqCnstr.lean

@@ -500,7 +500,7 @@ def checkRing : RingM Bool := do
   modifyRing fun s => { s with recheck := false }
   return true
 
-def check : GoalM Bool := do
+def check : GoalM Bool := do profileitM Exception "grind ring" (← getOptions) do
   if (← checkMaxSteps) then return false
   let mut progress := false
   checkInvariants

src/Lean/Meta/Tactic/Grind/Arith/Cutsat/Search.lean

@@ -578,7 +578,7 @@ There are two kinds of progress:
 
 The result is `false` if module already has a satisfying assignment.
 -/
-def check : GoalM Bool := do
+def check : GoalM Bool := do profileitM Exception "grind cutsat" (← getOptions) do
   if (← hasAssignment) then
     return false
   else

src/Lean/Meta/Tactic/Grind/Arith/Linear/Search.lean

@@ -264,7 +264,7 @@ There are two kinds of progress:
 
 The result is `false` if module for every structure already has an assignment.
 -/
-def check : GoalM Bool := do
+def check : GoalM Bool := do profileitM Exception "grind linarith" (← getOptions) do
   let mut progress := false
   for structId in *...(← get').structs.size do
     let r ← LinearM.run structId do

src/Lean/Meta/Tactic/Grind/EMatch.lean

@@ -553,7 +553,7 @@ end EMatch
 open EMatch
 
 /-- Performs one round of E-matching, and returns new instances. -/
-private def ematchCore : GoalM Unit := do
+private def ematchCore : GoalM Unit := do profileitM Exception "grind ematch" (← getOptions) do
   let go (thms newThms : PArray EMatchTheorem) : EMatch.M Unit := do
     withReader (fun ctx => { ctx with useMT := true }) <| ematchTheorems thms
     withReader (fun ctx => { ctx with useMT := false }) <| ematchTheorems newThms