chore(AtLocation): clean up backtick handling (#37999)

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 #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

@@ -47,7 +47,9 @@ def Lean.Elab.Tactic.withNondepPropLocation (loc : Location) (atLocal : FVarId 
 namespace Mathlib.Tactic
 open Lean Meta Elab.Tactic
 
-/-- Use the procedure `m` to rewrite the provided goal. -/
+/-- Use the procedure `m` to rewrite the provided goal.
+
+Assumes `proc` is not surrounded by backticks. -/
 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 +58,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
@@ -70,24 +72,28 @@ 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`. -/
+`h : x = y` is not transformed (by rewriting `h`) to `True`. 
+
+Assumes `proc` is not surrounded by backticks. -/
 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). -/
+/-- Use the procedure `m` to transform at specified locations (hypotheses and/or goal).
+
+Assumes `proc` is not surrounded by backticks. -/
 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 +103,13 @@ 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. -/
+In the wildcard case (`*`), filter out all dependent and/or non-`Prop` hypotheses.
+
+Assumes `proc` is not surrounded by backticks. -/
 def transformAtNondepPropLocation (m : Expr → ReaderT Simp.Context MetaM Simp.Result)
     (proc : String) (loc : Location) (failIfUnchanged : Bool := true)
     (mayCloseGoalFromHyp : Bool := false)
@@ -112,6 +120,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

MathlibTest/abel.lean

@@ -99,9 +99,7 @@ error: `abel_nf` made no progress on the goal
 #guard_msgs in
 example : False := by abel_nf
 
-/--
-error: `abel_nf` made no progress at w
--/
+/-- error: `abel_nf` made no progress at `w` -/
 #guard_msgs in
 example [AddCommGroup α] (x y z : α) (w : x = y + z) : False := by
   abel_nf at w
@@ -141,9 +139,7 @@ example [AddCommGroup α] (x y z : α) (_w : x = y + z) : False := by
 example [AddCommGroup α] (x y z : α) (_w : x = y + z) : x - x = 0 := by
   abel_nf at *
 
-/--
-error: `abel_nf` made no progress at w
--/
+/-- error: `abel_nf` made no progress at `w` -/
 #guard_msgs in
 example [AddCommGroup α] (x y z : α) (w : x = y + z) : x - x = 0 := by
   abel_nf at w ⊢

MathlibTest/push_neg.lean

@@ -151,14 +151,14 @@ example {P : Prop} (h : P) : P := by push Not at *
 
 -- new behaviour as of https://github.com/leanprover-community/mathlib4/issues/27562
 -- (Previously, because of a metavariable instantiation issue, the tactic succeeded as a no-op.)
-/-- error: `push` made no progress at h -/
+/-- error: `push` made no progress at `h` -/
 #guard_msgs in
 example {x y : ℕ} : True := by
   have h : x ≤ y := test_sorry
   push Not at h
 
 -- new behaviour as of https://github.com/leanprover-community/mathlib4/issues/27562 (previously the tactic succeeded as a no-op)
-/-- error: Cannot run `push` at inductive_proof, it is an implementation detail -/
+/-- error: Cannot run `push` at `inductive_proof`, it is an implementation detail -/
 #guard_msgs in
 def inductive_proof : True := by
   push Not at inductive_proof

MathlibTest/ring.lean

@@ -243,7 +243,7 @@ example (n : ℤ) (r : ℝ) : n • r = n * r := by
 
 -- new behaviour as of https://github.com/leanprover-community/mathlib4/issues/27562
 -- (Previously, because of a metavariable instantiation issue, the tactic succeeded as a no-op.)
-/-- error: `ring_nf` made no progress at h -/
+/-- error: `ring_nf` made no progress at `h` -/
 #guard_msgs in
 example {R : Type*} [CommSemiring R] {x y : R} : True := by
   have h : x + y = 3 := test_sorry