chore(AtLocation): clean up backtick handling

Make errors in AtLocation surround the tactic name with backticks by default.
This fixes a few error messages to comply with mathlib's style guide.

Extracted from leanprover-community#37899.

Author: grunweg

Mathlib/Tactic/Abel.lean

@@ -506,7 +506,7 @@ elab (name := abelNF) "abel_nf" tk:"!"? cfg:optConfig loc:(location)? : tactic =
   let loc := (loc.map expandLocation).getD (.targets #[] true)
   let s ← IO.mkRef {}
   let m := AtomM.recurse s cfg.toConfig (wellBehavedDischarge := true) evalExpr (cleanup cfg)
-  transformAtLocation (m ·) "`abel_nf`" loc (failIfUnchanged := true) false
+  transformAtLocation (m ·) "abel_nf" loc (failIfUnchanged := true) false
 
 @[tactic_alt abel]
 macro "abel_nf!" cfg:optConfig loc:(location)? : tactic =>

Mathlib/Tactic/FieldSimp.lean

@@ -711,8 +711,7 @@ elab (name := fieldSimp) "field_simp" d:(discharger)? args:(simpArgs)? loc:(loca
   let m := AtomM.recurse s { contextual := true } (wellBehavedDischarge := false)
     (fun e ↦ reduceProp disch e <|> reduceExpr disch e) cleanup
   let loc := (loc.map expandLocation).getD (.targets #[] true)
-  transformAtLocation
-    (m ·) "`field_simp`" (failIfUnchanged := true) (mayCloseGoalFromHyp := true) loc
+  transformAtLocation (m ·) "field_simp" (failIfUnchanged := true) (mayCloseGoalFromHyp := true) loc
 
 /--
 `field_simp` normalizes an expression in a (semi-)field by rewriting it to a common denominator,

Mathlib/Tactic/Push.lean

@@ -211,7 +211,7 @@ def elabDischarger (stx : TSyntax ``discharger) : TacticM Simp.Discharge :=
 def push (cfg : Config) (disch? : Option Simp.Discharge) (head : Head) (loc : Location)
     (failIfUnchanged : Bool := true) : TacticM Unit := do
   let cfg := { distrib := cfg.distrib || (← getBoolOption `push_neg.use_distrib) }
-  transformAtLocation (pushCore head cfg disch? ·) "`push`" loc failIfUnchanged
+  transformAtLocation (pushCore head cfg disch? ·) "push" loc failIfUnchanged
 
 /--
 `push c` rewrites the goal by pushing the constant `c` deeper into an expression.
@@ -318,7 +318,7 @@ elab (name := pull) "pull" disch?:(discharger)? head:(ppSpace colGt term) loc:(l
   let disch? ← disch?.mapM elabDischarger
   let head ← elabHead head
   let loc := (loc.map expandLocation).getD (.targets #[] true)
-  transformAtLocation (pullCore head · disch?) "`pull`" loc (failIfUnchanged := true) false
+  transformAtLocation (pullCore head · disch?) "pull" loc (failIfUnchanged := true) false
 
 /-- A simproc variant of `push fun _ ↦ _`, to be used as `simp [↓pushFun]`. -/
 simproc_decl _root_.pushFun (fun _ ↦ ?_) := pushStep .lambda {}

Mathlib/Tactic/Ring/RingNF.lean

@@ -138,7 +138,7 @@ elab (name := ringNF) "ring_nf" tk:"!"? cfg:optConfig loc:(location)? : tactic =
   let loc := (loc.map expandLocation).getD (.targets #[] true)
   let s ← IO.mkRef {}
   let m := AtomM.recurse s cfg.toConfig (wellBehavedDischarge := true) evalExpr (cleanup cfg)
-  transformAtLocation (m ·) "`ring_nf`" loc cfg.failIfUnchanged false
+  transformAtLocation (m ·) "ring_nf" loc cfg.failIfUnchanged false
 
 @[tactic_alt ringNF] macro "ring_nf!" cfg:optConfig loc:(location)? : tactic =>
   `(tactic| ring_nf ! $cfg:optConfig $(loc)?)

Mathlib/Util/AtLocation.lean

@@ -48,6 +48,7 @@ namespace Mathlib.Tactic
 open Lean Meta Elab.Tactic
 
 /-- Use the procedure `m` to rewrite the provided goal. -/
+-- Assumes `proc` is not surrounded by backticks itself.
 def transformAtTarget (m : Expr → ReaderT Simp.Context MetaM Simp.Result) (proc : String)
     (failIfUnchanged : Bool) (goal : MVarId) :
     ReaderT Simp.Context MetaM (Option MVarId) := do
@@ -56,7 +57,7 @@ def transformAtTarget (m : Expr → ReaderT Simp.Context MetaM Simp.Result) (pro
   -- we use expression equality here (rather than defeq) to be consistent with, e.g.,
   -- `applySimpResultToTarget`
   let unchanged := tgt.cleanupAnnotations == r.expr.cleanupAnnotations
-  if failIfUnchanged && unchanged then throwError "{proc} made no progress on the goal"
+  if failIfUnchanged && unchanged then throwError "`{proc}` made no progress on the goal"
   if r.expr.isTrue then
     goal.assign (← mkOfEqTrue (← r.getProof))
     pure none
@@ -71,23 +72,25 @@ def transformAtTarget (m : Expr → ReaderT Simp.Context MetaM Simp.Result) (pro
 The `simpTheorems` of the simp-context carried with `m` will be modified to remove `fvarId`;
 this ensures that if the procedure `m` involves rewriting by this `SimpTheoremsArray`, then, e.g.,
 `h : x = y` is not transformed (by rewriting `h`) to `True`. -/
+-- Assumes `proc` is not surrounded by backticks itself.
 def transformAtLocalDecl (m : Expr → ReaderT Simp.Context MetaM Simp.Result) (proc : String)
     (failIfUnchanged : Bool) (mayCloseGoal : Bool) (fvarId : FVarId) (goal : MVarId) :
     ReaderT Simp.Context MetaM (Option MVarId) := do
   let ldecl ← fvarId.getDecl
   if ldecl.isImplementationDetail then
-    throwError "Cannot run {proc} at {ldecl.userName}, it is an implementation detail"
+    throwError "Cannot run `{proc}` at `{ldecl.userName}`, it is an implementation detail"
   let tgt ← instantiateMVars (← fvarId.getType)
   let eraseFVarId (ctx : Simp.Context) :=
     ctx.setSimpTheorems <| ctx.simpTheorems.eraseTheorem (.fvar fvarId)
   let r ← withReader eraseFVarId <| m tgt
   -- we use expression equality here (rather than defeq) to be consistent with, e.g.,
   -- `applySimpResultToLocalDeclCore`
   if failIfUnchanged && tgt.cleanupAnnotations == r.expr.cleanupAnnotations then
-    throwError "{proc} made no progress at {ldecl.userName}"
+    throwError "`{proc}` made no progress at `{ldecl.userName}`"
   return (← applySimpResultToLocalDecl goal fvarId r mayCloseGoal).map Prod.snd
 
 /-- Use the procedure `m` to transform at specified locations (hypotheses and/or goal). -/
+-- Assumes `proc` is not surrounded by backticks itself.
 def transformAtLocation (m : Expr → ReaderT Simp.Context MetaM Simp.Result) (proc : String)
     (loc : Location) (failIfUnchanged : Bool := true) (mayCloseGoalFromHyp : Bool := false)
     -- streamline the most common use case, in which the procedure `m`'s implementation is not
@@ -97,11 +100,12 @@ def transformAtLocation (m : Expr → ReaderT Simp.Context MetaM Simp.Result) (p
   withLocation loc
     (liftMetaTactic1 ∘ (transformAtLocalDecl m proc failIfUnchanged mayCloseGoalFromHyp · · ctx))
     (liftMetaTactic1 (transformAtTarget m proc failIfUnchanged · ctx))
-    fun _ ↦ throwError "{proc} made no progress anywhere"
+    fun _ ↦ throwError "`{proc}` made no progress anywhere"
 
 /-- Use the procedure `m` to transform at specified locations (hypotheses and/or goal).
 
 In the wildcard case (`*`), filter out all dependent and/or non-Prop hypotheses. -/
+-- Assumes `proc` is not surrounded by backticks itself.
 def transformAtNondepPropLocation (m : Expr → ReaderT Simp.Context MetaM Simp.Result)
     (proc : String) (loc : Location) (failIfUnchanged : Bool := true)
     (mayCloseGoalFromHyp : Bool := false)
@@ -112,6 +116,6 @@ def transformAtNondepPropLocation (m : Expr → ReaderT Simp.Context MetaM Simp.
   withNondepPropLocation loc
     (liftMetaTactic1 ∘ (transformAtLocalDecl m proc failIfUnchanged mayCloseGoalFromHyp · · ctx))
     (liftMetaTactic1 (transformAtTarget m proc failIfUnchanged · ctx))
-    fun _ ↦ throwError "{proc} made no progress anywhere"
+    fun _ ↦ throwError "`{proc}` made no progress anywhere"
 
 end Mathlib.Tactic