Update tests

so that the pretty-printed origin is clickable

src/Lean/Meta/Tactic/Simp/SimpTheorems.lean

@@ -11,6 +11,7 @@ import Lean.Meta.AppBuilder
 import Lean.Meta.Eqns
 import Lean.Meta.Tactic.AuxLemma
 import Lean.DocString
+import Lean.PrettyPrinter
 namespace Lean.Meta
 
 /--
@@ -142,7 +143,7 @@ instance : ToFormat SimpTheorem where
 
 def ppOrigin [Monad m] [MonadEnv m] [MonadError m] : Origin → m MessageData
   | .decl n post inv => do
-    let r ← mkConstWithLevelParams n;
+    let r := MessageData.ofConst (← mkConstWithLevelParams n)
     match post, inv with
     | true,  true  => return m!"← {r}"
     | true,  false => return r

tests/lean/1079.lean.expected.out

@@ -1,8 +1,8 @@
 1079.lean:4:2-6:12: error: alternative 'isFalse' has not been provided
 [Meta.Tactic.simp.rewrite] h:1000, m ==> n
-[Meta.Tactic.simp.rewrite] @eq_self:1000, n = n ==> True
-[Meta.Tactic.simp.unify] @eq_self:1000, failed to unify
+[Meta.Tactic.simp.rewrite] eq_self:1000, n = n ==> True
+[Meta.Tactic.simp.unify] eq_self:1000, failed to unify
       ?a = ?a
     with
       Ordering.eq = Ordering.lt
-[Meta.Tactic.simp.rewrite] @imp_self:10000, False → False ==> True
+[Meta.Tactic.simp.rewrite] imp_self:10000, False → False ==> True

tests/lean/973b.lean.expected.out

@@ -1,5 +1,5 @@
 973b.lean:5:8-5:10: warning: declaration uses 'sorry'
 973b.lean:9:8-9:11: warning: declaration uses 'sorry'
-[Meta.Tactic.simp.discharge] @ex discharge ❌
+[Meta.Tactic.simp.discharge] ex discharge ❌
       ?p x
-[Meta.Tactic.simp.discharge] @ex discharge ❌ ?p (f x)
+[Meta.Tactic.simp.discharge] ex discharge ❌ ?p (f x)

tests/lean/discrTreeIota.lean.expected.out

@@ -1,2 +1,2 @@
 [Meta.Tactic.simp.rewrite] PUnit.default_eq_unit:1000, default ==> PUnit.unit
-[Meta.Tactic.simp.rewrite] @eq_self:1000, PUnit.unit = x ==> True
+[Meta.Tactic.simp.rewrite] eq_self:1000, PUnit.unit = x ==> True

tests/lean/run/1234.lean

@@ -10,12 +10,12 @@ set_option trace.Meta.Tactic.simp true
 warning: declaration uses 'sorry'
 ---
 info: [Meta.Tactic.simp.rewrite] h₁:1000, k ≤ v - 1 ==> True
-[Meta.Tactic.simp.discharge] @succ_pred_eq_of_pos discharge ✅
+[Meta.Tactic.simp.discharge] succ_pred_eq_of_pos discharge ✅
       0 < v
   [Meta.Tactic.simp.rewrite] h₂:1000, 0 < v ==> True
-[Meta.Tactic.simp.rewrite] @succ_pred_eq_of_pos:1000, v - 1 + 1 ==> v
-[Meta.Tactic.simp.rewrite] @ite_true:1000, if True then ⟨v, ⋯⟩ else ⟨v - 1, ⋯⟩ ==> ⟨v, ⋯⟩
-[Meta.Tactic.simp.rewrite] @eq_self:1000, ⟨v, ⋯⟩ = ⟨v, ⋯⟩ ==> True
+[Meta.Tactic.simp.rewrite] succ_pred_eq_of_pos:1000, v - 1 + 1 ==> v
+[Meta.Tactic.simp.rewrite] ite_true:1000, if True then ⟨v, ⋯⟩ else ⟨v - 1, ⋯⟩ ==> ⟨v, ⋯⟩
+[Meta.Tactic.simp.rewrite] eq_self:1000, ⟨v, ⋯⟩ = ⟨v, ⋯⟩ ==> True
 -/
 #guard_msgs in
 example (h₁: k ≤ v - 1) (h₂: 0 < v):
@@ -35,12 +35,12 @@ example (h₁: k ≤ v - 1) (h₂: 0 < v):
 warning: declaration uses 'sorry'
 ---
 info: [Meta.Tactic.simp.rewrite] h₁:1000, k ≤ v - 1 ==> True
-[Meta.Tactic.simp.discharge] @succ_pred_eq_of_pos discharge ✅
+[Meta.Tactic.simp.discharge] succ_pred_eq_of_pos discharge ✅
       0 < v
   [Meta.Tactic.simp.rewrite] h₂:1000, 0 < v ==> True
-[Meta.Tactic.simp.rewrite] @succ_pred_eq_of_pos:1000, v - 1 + 1 ==> v
-[Meta.Tactic.simp.rewrite] @ite_true:1000, if True then ⟨v, ⋯⟩ else ⟨v - 1, ⋯⟩ ==> ⟨v, ⋯⟩
-[Meta.Tactic.simp.rewrite] @eq_self:1000, ⟨v, ⋯⟩ = ⟨v, ⋯⟩ ==> True
+[Meta.Tactic.simp.rewrite] succ_pred_eq_of_pos:1000, v - 1 + 1 ==> v
+[Meta.Tactic.simp.rewrite] ite_true:1000, if True then ⟨v, ⋯⟩ else ⟨v - 1, ⋯⟩ ==> ⟨v, ⋯⟩
+[Meta.Tactic.simp.rewrite] eq_self:1000, ⟨v, ⋯⟩ = ⟨v, ⋯⟩ ==> True
 -/
 #guard_msgs in
 example (h₁: k ≤ v - 1) (h₂: 0 < v):
@@ -58,12 +58,12 @@ example (h₁: k ≤ v - 1) (h₂: 0 < v):
 warning: declaration uses 'sorry'
 ---
 info: [Meta.Tactic.simp.rewrite] h₁:1000, k ≤ v - 1 ==> True
-[Meta.Tactic.simp.discharge] @succ_pred_eq_of_pos discharge ✅
+[Meta.Tactic.simp.discharge] succ_pred_eq_of_pos discharge ✅
       0 < v
   [Meta.Tactic.simp.rewrite] h₂:1000, 0 < v ==> True
-[Meta.Tactic.simp.rewrite] @succ_pred_eq_of_pos:1000, v - 1 + 1 ==> v
-[Meta.Tactic.simp.rewrite] @ite_true:1000, if True then ⟨v, ⋯⟩ else ⟨v - 1, ⋯⟩ ==> ⟨v, ⋯⟩
-[Meta.Tactic.simp.rewrite] @eq_self:1000, ⟨v, ⋯⟩ = ⟨v, ⋯⟩ ==> True
+[Meta.Tactic.simp.rewrite] succ_pred_eq_of_pos:1000, v - 1 + 1 ==> v
+[Meta.Tactic.simp.rewrite] ite_true:1000, if True then ⟨v, ⋯⟩ else ⟨v - 1, ⋯⟩ ==> ⟨v, ⋯⟩
+[Meta.Tactic.simp.rewrite] eq_self:1000, ⟨v, ⋯⟩ = ⟨v, ⋯⟩ ==> True
 -/
 #guard_msgs in
 example (h₁: k ≤ v - 1) (h₂: 0 < v):

tests/lean/run/1380.lean

@@ -3,19 +3,19 @@ variable (n v₁ v₂) (hv₁: v₁ < n + 1) (hv₂: v₂ < n + 1)
 theorem foo (_: ¬ Fin.mk v₂ hv₂ = Fin.mk v₁ hv₁ ): True := trivial
 
 /--
-info: [Meta.Tactic.simp.unify] @eq_self:1000, failed to unify
+info: [Meta.Tactic.simp.unify] eq_self:1000, failed to unify
       ?a = ?a
     with
       ⟨v₂, hv₂⟩ = ⟨v₁, hv₁⟩
-[Meta.Tactic.simp.rewrite] @Fin.mk.injEq:1000, ⟨v₂, hv₂⟩ = ⟨v₁, hv₁⟩ ==> v₂ = v₁
-[Meta.Tactic.simp.unify] @eq_self:1000, failed to unify
+[Meta.Tactic.simp.rewrite] Fin.mk.injEq:1000, ⟨v₂, hv₂⟩ = ⟨v₁, hv₁⟩ ==> v₂ = v₁
+[Meta.Tactic.simp.unify] eq_self:1000, failed to unify
       ?a = ?a
     with
       v₂ = v₁
-[Meta.Tactic.simp.discharge] @Nat.ne_of_gt discharge ✅
+[Meta.Tactic.simp.discharge] Nat.ne_of_gt discharge ✅
       v₁ < v₂
   [Meta.Tactic.simp.rewrite] hv:1000, v₁ < v₂ ==> True
-[Meta.Tactic.simp.rewrite] @Nat.ne_of_gt:1000, v₂ = v₁ ==> False
+[Meta.Tactic.simp.rewrite] Nat.ne_of_gt:1000, v₂ = v₁ ==> False
 -/
 #guard_msgs in
 set_option trace.Meta.Tactic.simp true in

tests/lean/run/1815.lean

@@ -7,10 +7,10 @@ theorem mul_comm (a b : α) : a * b = b * a := sorry
 
 set_option trace.Meta.Tactic.simp true
 /--
-info: [Meta.Tactic.simp.rewrite] @mul_comm:1000:perm, perm rejected Left a ==> default * a
-[Meta.Tactic.simp.rewrite] @mul_comm:1000:perm, Right a ==> a * default
-[Meta.Tactic.simp.rewrite] @mul_comm:1000:perm, perm rejected a * default ==> default * a
-[Meta.Tactic.simp.rewrite] @eq_self:1000, Left a = a * default ==> True
+info: [Meta.Tactic.simp.rewrite] mul_comm:1000:perm, perm rejected Left a ==> default * a
+[Meta.Tactic.simp.rewrite] mul_comm:1000:perm, Right a ==> a * default
+[Meta.Tactic.simp.rewrite] mul_comm:1000:perm, perm rejected a * default ==> default * a
+[Meta.Tactic.simp.rewrite] eq_self:1000, Left a = a * default ==> True
 -/
 #guard_msgs in
 example (a : α) : Left a = Right a := by

tests/lean/run/3257.lean

@@ -14,10 +14,10 @@ example : U := by
   simp [foo, T.mk]
 
 /--
-info: [Meta.Tactic.simp.discharge] @bar discharge ✅
+info: [Meta.Tactic.simp.discharge] bar discharge ✅
       autoParam T _auto✝
-  [Meta.Tactic.simp.rewrite] { }:1000, T ==> True
-[Meta.Tactic.simp.rewrite] @bar:1000, U ==> True
+  [Meta.Tactic.simp.rewrite] T.mk:1000, T ==> True
+[Meta.Tactic.simp.rewrite] bar:1000, U ==> True
 -/
 #guard_msgs in
 example : U := by

tests/lean/run/790.lean

@@ -16,8 +16,8 @@ instance : Vec' Nat := ⟨⟩
 
 set_option trace.Meta.Tactic.simp true
 /--
-info: [Meta.Tactic.simp.rewrite] @differential_of_linear:1000, differential f x dx ==> f dx
-[Meta.Tactic.simp.rewrite] @eq_self:1000, f dx = f dx ==> True
+info: [Meta.Tactic.simp.rewrite] differential_of_linear:1000, differential f x dx ==> f dx
+[Meta.Tactic.simp.rewrite] eq_self:1000, f dx = f dx ==> True
 -/
 #guard_msgs in
 example {Y : Type} [Vec Y] (f : Nat → Y) (x dx : Nat)

tests/lean/simp_trace.lean.expected.out

@@ -1,23 +1,23 @@
 Try this: simp only [f]
 [Meta.Tactic.simp.rewrite] unfold f, f (a :: b = []) ==> a :: b = []
-[Meta.Tactic.simp.rewrite] @eq_self:1000, False = False ==> True
+[Meta.Tactic.simp.rewrite] eq_self:1000, False = False ==> True
 Try this: simp only [length, gt_iff_lt]
 [Meta.Tactic.simp.rewrite] unfold length, length (a :: b :: as) ==> length (b :: as) + 1
 [Meta.Tactic.simp.rewrite] unfold length, length (b :: as) ==> length as + 1
-[Meta.Tactic.simp.rewrite] @gt_iff_lt:1000, length as + 1 + 1 > length as ==> length as < length as + 1 + 1
+[Meta.Tactic.simp.rewrite] gt_iff_lt:1000, length as + 1 + 1 > length as ==> length as < length as + 1 + 1
 Try this: simp only [fact, gt_iff_lt, Nat.zero_lt_succ, Nat.mul_pos_iff_of_pos_left]
 [Meta.Tactic.simp.rewrite] unfold fact, fact (x + 1) ==> (x + 1) * fact x
-[Meta.Tactic.simp.rewrite] @gt_iff_lt:1000, (x + 1) * fact x > 0 ==> 0 < (x + 1) * fact x
+[Meta.Tactic.simp.rewrite] gt_iff_lt:1000, (x + 1) * fact x > 0 ==> 0 < (x + 1) * fact x
 [Meta.Tactic.simp.rewrite] Nat.zero_lt_succ:1000, 0 < x + 1 ==> True
-[Meta.Tactic.simp.rewrite] @Nat.mul_pos_iff_of_pos_left:1000, 0 < (x + 1) * fact x ==> 0 < fact x
+[Meta.Tactic.simp.rewrite] Nat.mul_pos_iff_of_pos_left:1000, 0 < (x + 1) * fact x ==> 0 < fact x
 Try this: simp only [head]
 [Meta.Tactic.simp.rewrite] unfold head, head (a :: as) ==> match a :: as with
     | [] => default
     | a :: tail => a
-[Meta.Tactic.simp.rewrite] @eq_self:1000, a = a ==> True
+[Meta.Tactic.simp.rewrite] eq_self:1000, a = a ==> True
 Try this: simp only [foo]
 [Meta.Tactic.simp.rewrite] unfold foo, foo ==> 10
-[Meta.Tactic.simp.rewrite] @eq_self:1000, 10 + x = 10 + x ==> True
+[Meta.Tactic.simp.rewrite] eq_self:1000, 10 + x = 10 + x ==> True
 Try this: simp only [g, pure]
 [Meta.Tactic.simp.rewrite] unfold g, g x ==> (let x := x;
       pure x).run
@@ -37,33 +37,33 @@ Try this: simp (config := { unfoldPartialApp := true }) only [f1, modify, modify
 [Meta.Tactic.simp.rewrite] unfold getThe, getThe Nat s ==> MonadStateOf.get s
 [Meta.Tactic.simp.rewrite] unfold StateT.get, StateT.get s ==> pure (s, s)
 [Meta.Tactic.simp.rewrite] unfold StateT.set, StateT.set (g s) s ==> pure (PUnit.unit, g s)
-[Meta.Tactic.simp.rewrite] @eq_self:1000, (fun s => (PUnit.unit, g s)) = fun s => (PUnit.unit, g s) ==> True
+[Meta.Tactic.simp.rewrite] eq_self:1000, (fun s => (PUnit.unit, g s)) = fun s => (PUnit.unit, g s) ==> True
 Try this: simp only [bla, h]
 [Meta.Tactic.simp.rewrite] unfold bla, bla x ==> match h x with
     | Sum.inl (y, z) => y + z
     | Sum.inr val => 0
 [Meta.Tactic.simp.rewrite] unfold h, h x ==> Sum.inl (x, x)
-[Meta.Tactic.simp.rewrite] @eq_self:1000, x + x = x + x ==> True
+[Meta.Tactic.simp.rewrite] eq_self:1000, x + x = x + x ==> True
 Try this: simp only [h, Nat.sub_add_cancel]
 [Meta.Tactic.simp.rewrite] h:1000, 1 ≤ x ==> True
-[Meta.Tactic.simp.rewrite] @Nat.sub_add_cancel:1000, x - 1 + 1 ==> x
-[Meta.Tactic.simp.rewrite] @eq_self:1000, x + 2 = x + 2 ==> True
+[Meta.Tactic.simp.rewrite] Nat.sub_add_cancel:1000, x - 1 + 1 ==> x
+[Meta.Tactic.simp.rewrite] eq_self:1000, x + 2 = x + 2 ==> True
 Try this: simp (config := { contextual := true }) only [Nat.sub_add_cancel, dite_eq_ite]
 [Meta.Tactic.simp.rewrite] h:1000, 1 ≤ x ==> True
-[Meta.Tactic.simp.rewrite] @Nat.sub_add_cancel:1000, x - 1 + 1 ==> x
-[Meta.Tactic.simp.rewrite] @dite_eq_ite:1000, if h : 1 ≤ x then x else 0 ==> if 1 ≤ x then x else 0
-[Meta.Tactic.simp.rewrite] @dite_eq_ite:1000, if _h : 1 ≤ x then x else 0 ==> if 1 ≤ x then x else 0
-[Meta.Tactic.simp.rewrite] @eq_self:1000, (if 1 ≤ x then x else 0) = if 1 ≤ x then x else 0 ==> True
+[Meta.Tactic.simp.rewrite] Nat.sub_add_cancel:1000, x - 1 + 1 ==> x
+[Meta.Tactic.simp.rewrite] dite_eq_ite:1000, if h : 1 ≤ x then x else 0 ==> if 1 ≤ x then x else 0
+[Meta.Tactic.simp.rewrite] dite_eq_ite:1000, if _h : 1 ≤ x then x else 0 ==> if 1 ≤ x then x else 0
+[Meta.Tactic.simp.rewrite] eq_self:1000, (if 1 ≤ x then x else 0) = if 1 ≤ x then x else 0 ==> True
 Try this: simp only [and_self]
 [Meta.Tactic.simp.rewrite] and_self:1000, b ∧ b ==> b
 [Meta.Tactic.simp.rewrite] iff_self:1000, a ∧ b ↔ a ∧ b ==> True
 Try this: simp only [my_thm]
-[Meta.Tactic.simp.rewrite] @my_thm:1000, b ∧ b ==> b
-[Meta.Tactic.simp.rewrite] @eq_self:1000, (a ∧ b) = (a ∧ b) ==> True
+[Meta.Tactic.simp.rewrite] my_thm:1000, b ∧ b ==> b
+[Meta.Tactic.simp.rewrite] eq_self:1000, (a ∧ b) = (a ∧ b) ==> True
 Try this: simp (discharger := sorry) only [Nat.sub_add_cancel]
 simp_trace.lean:83:0-83:7: warning: declaration uses 'sorry'
-[Meta.Tactic.simp.rewrite] @Nat.sub_add_cancel:1000, x - 1 + 1 ==> x
-[Meta.Tactic.simp.rewrite] @eq_self:1000, x = x ==> True
+[Meta.Tactic.simp.rewrite] Nat.sub_add_cancel:1000, x - 1 + 1 ==> x
+[Meta.Tactic.simp.rewrite] eq_self:1000, x = x ==> True
 Try this: simp only [bla, h] at *
 [Meta.Tactic.simp.rewrite] unfold bla, bla x ==> match h x with
     | Sum.inl (y, z) => y + z
@@ -86,7 +86,7 @@ h₂ : xs.length + ys.length = y
     | Sum.inl (y, z) => y + z
     | Sum.inr val => 0
 [Meta.Tactic.simp.rewrite] unfold h, h x ==> Sum.inl (x, x)
-[Meta.Tactic.simp.rewrite] @List.length_append:1000, (xs ++ ys).length ==> xs.length + ys.length
+[Meta.Tactic.simp.rewrite] List.length_append:1000, (xs ++ ys).length ==> xs.length + ys.length
 Try this: simp only [bla, h, List.length_append] at *
 simp_trace.lean:103:101-104:53: error: unsolved goals
 x y : Nat
@@ -99,7 +99,7 @@ h₂ : xs.length + ys.length = y
     | Sum.inl (y, z) => y + z
     | Sum.inr val => 0
 [Meta.Tactic.simp.rewrite] unfold h, h x ==> Sum.inl (x, x)
-[Meta.Tactic.simp.rewrite] @List.length_append:1000, (xs ++ ys).length ==> xs.length + ys.length
+[Meta.Tactic.simp.rewrite] List.length_append:1000, (xs ++ ys).length ==> xs.length + ys.length
 Try this: simp only [bla, h] at *
 [Meta.Tactic.simp.rewrite] unfold bla, bla x ==> match h x with
     | Sum.inl (y, z) => y + z
@@ -122,7 +122,7 @@ Try this: simp only [HasProp.toProp]
 Try this: simp only [← h]
 [Meta.Tactic.simp.rewrite] ← h:1000, Q ==> P
 Try this: simp only [← my_thm']
-[Meta.Tactic.simp.rewrite] ← @my_thm':1000, P ∧ P ==> P
+[Meta.Tactic.simp.rewrite] ← my_thm':1000, P ∧ P ==> P
 [Meta.Tactic.simp.rewrite] iff_self:1000, P ↔ P ==> True
 Try this: simp only [h]
 [Meta.Tactic.simp.rewrite] h:1000, P ==> True