chore: quiet some tests (#376)

Std/Tactic/RunCmd.lean

@@ -32,6 +32,27 @@ elab (name := runCmd) "run_cmd " elems:doSeq : command => do
       (mkApp (mkConst ``CommandElabM) (mkConst ``Unit))
       (← `(discard do $elems))
 
+/--
+The `run_elab doSeq` command executes code in `TermElabM Unit`.
+This is almost the same as `#eval show TermElabM Unit from do doSeq`,
+except that it doesn't print an empty diagnostic.
+-/
+elab (name := runElab) "run_elab " elems:doSeq : command => do
+  ← liftTermElabM <|
+    unsafe evalTerm (CommandElabM Unit)
+      (mkApp (mkConst ``CommandElabM) (mkConst ``Unit))
+      (← `(Command.liftTermElabM <| discard do $elems))
+
+/--
+The `run_meta doSeq` command executes code in `MetaM Unit`.
+This is almost the same as `#eval show MetaM Unit from do doSeq`,
+except that it doesn't print an empty diagnostic.
+
+(This is effectively a synonym for `run_elab`.)
+-/
+macro (name := runMeta) "run_meta " elems:doSeq : command =>
+  `(command| run_elab (show MetaM Unit from do $elems))
+
 /-- The `run_tac doSeq` tactic executes code in `TacticM Unit`. -/
 elab (name := runTac) "run_tac " e:doSeq : tactic => do
   ← unsafe evalTerm (TacticM Unit) (mkApp (mkConst ``TacticM) (mkConst ``Unit))

test/add_suggestion.lean

@@ -1,4 +1,5 @@
 import Std.Tactic.TryThis
+import Std.Tactic.GuardMsgs
 
 set_option linter.unusedVariables false
 set_option linter.missingDocs false
@@ -26,6 +27,7 @@ elab "test" : tactic => do
 
 end Std.Tactic.TryThis
 
+#guard_msgs (drop info, drop warning) in
 -- ideally we would have a #guard_widgets or #guard_infos too, but instead we can simply check by
 -- hand that the widget suggestion (not the message) fits into 100 columns
 theorem asda (a b : Nat) (h : a = b) : 2 * a = 2 * b := by

test/case.lean

@@ -184,6 +184,14 @@ example : True ∧ ∀ x : Nat, x = x := by
   rfl
 
 -- Test focusing by full match, suffix match, and prefix match
+/--
+warning: unused variable `x` [linter.unusedVariables]
+---
+warning: unused variable `y` [linter.unusedVariables]
+---
+warning: unused variable `z` [linter.unusedVariables]
+-/
+#guard_msgs in
 example : True := by
   have x : Bool := ?a
   have y : Nat := ?a.b.c

test/ext.lean

@@ -1,5 +1,6 @@
 import Std.Tactic.Ext
 import Std.Logic
+import Std.Tactic.GuardMsgs
 
 set_option linter.missingDocs false
 axiom mySorry {α : Sort _} : α
@@ -41,6 +42,8 @@ example (f g : Nat × Nat → Nat) : f = g := by
   guard_target = f (x, y) = g (x, y); exact mySorry
 
 -- Check that we generate a warning if there are too many patterns.
+/-- warning: `ext` did not consume the patterns: [j] [linter.unusedRCasesPattern] -/
+#guard_msgs in
 example (f g : Nat → Nat) (h : f = g) : f = g := by
   ext i j
   exact h ▸ rfl
@@ -77,12 +80,14 @@ example (f : Empty → Empty) : f = f := by
 
 @[ext] theorem ext_intros {n m : Nat} (w : ∀ n m : Nat, n = m) : n = m := by apply w
 
+#guard_msgs (drop warning) in
 example : 3 = 7 := by
   ext : 1
   rename_i n m
   guard_target = n = m
   admit
 
+#guard_msgs (drop warning) in
 example : 3 = 7 := by
   ext n m : 1
   guard_target = n = m

test/lintTC.lean

@@ -1,14 +1,24 @@
 import Std.Tactic.Lint.TypeClass
+import Std.Tactic.GuardMsgs
+import Std.Tactic.RunCmd
+
 open Std.Tactic.Lint
 
 namespace A
+
+/-- warning: unused variable `β` [linter.unusedVariables] -/
+#guard_msgs in
 local instance impossible {α β : Type} [Inhabited α] : Nonempty α := ⟨default⟩
-#eval do guard (← impossibleInstance.test ``impossible).isSome
+
+run_meta guard (← impossibleInstance.test ``impossible).isSome
+
 end A
 
 namespace B
 instance bad : Nat := 1
-#eval do guard (← nonClassInstance.test ``bad).isSome
+
+run_meta guard (← nonClassInstance.test ``bad).isSome
 instance good : Inhabited Nat := ⟨1⟩
-#eval do guard (← nonClassInstance.test ``good).isNone
+
+run_meta guard (← nonClassInstance.test ``good).isNone
 end B

test/lint_unreachableTactic.lean

@@ -14,7 +14,10 @@ example : 1 = 1 := by
   stop
   rfl
 
+#guard_msgs (drop warning) in
 def t : Nat → Nat := sorry
+
+#guard_msgs (drop warning) in
 @[simp]
 theorem a : aa = 0 → t aa = 0 := sorry
 

test/lintsimp.lean

@@ -1,4 +1,7 @@
 import Std.Tactic.Lint
+import Std.Tactic.GuardMsgs
+import Std.Tactic.RunCmd
+
 open Std.Tactic.Lint
 set_option linter.missingDocs false
 
@@ -7,13 +10,14 @@ def g : Nat := 0
 def h : Nat := 0
 @[simp] theorem fg : f = g := rfl
 @[simp] theorem fh : f = h := rfl
-#eval do guard (← [``fg, ``fh].anyM fun n => return (← simpNF.test n).isSome)
+
+run_meta guard (← [``fg, ``fh].anyM fun n => return (← simpNF.test n).isSome)
 
 @[simp] theorem and_comm : a ∧ b ↔ b ∧ a := And.comm
-#eval do guard (← simpComm.test ``and_comm).isSome
+run_meta guard (← simpComm.test ``and_comm).isSome
 
 @[simp] theorem Prod.mk_fst : (a, b).1 = id a := rfl
-#eval do guard (← simpVarHead.test ``Prod.mk_fst).isSome
+run_meta guard (← simpVarHead.test ``Prod.mk_fst).isSome
 
 def SemiconjBy [Mul M] (a x y : M) : Prop :=
   a * x = y * a
@@ -31,11 +35,13 @@ instance [Mul α] : Mul αᵐᵒᵖ where mul x y := op (unop y * unop x)
 theorem unop_inj {x y : αᵐᵒᵖ} : unop x = unop y ↔ x = y := by
   cases x; cases y; simp
 
+#guard_msgs (drop warning) in
 @[simp]
 theorem semiconj_by_unop [Mul α] {a x y : αᵐᵒᵖ} :
     SemiconjBy (unop a) (unop y) (unop x) ↔ SemiconjBy a x y := sorry
 
-#eval do guard (← simpComm.test ``unop_inj).isNone
-#eval do guard (← simpComm.test ``semiconj_by_unop).isNone
+run_meta guard (← simpComm.test ``unop_inj).isNone
+
+run_meta guard (← simpComm.test ``semiconj_by_unop).isNone
 
 end MulOpposite

test/lintunused.lean

@@ -1,6 +1,9 @@
 import Std.Tactic.Lint
+import Std.Tactic.GuardMsgs
 
 -- should be ignored as the proof contains sorry
+/-- warning: declaration uses 'sorry' -/
+#guard_msgs in
 theorem Foo (h : 1 = 1) : True :=
   sorry
 

test/norm_cast.lean

@@ -72,7 +72,7 @@ example (a b : Nat) (h2 : ((a + b + 0 : Nat) : Int) = 10) :
   push_cast [Int.add_zero] at h2
   exact h2
 
-theorem b (h g : true) : true ∧ true := by
+theorem b (_h g : true) : true ∧ true := by
   constructor
   assumption_mod_cast
   assumption_mod_cast

test/simp_trace.lean

@@ -1,8 +1,13 @@
 import Std.Tactic.SqueezeScope
+import Std.Tactic.GuardMsgs
 
 set_option linter.missingDocs false
 
+/-- info: Try this: simp only [Nat.add_comm] -/
+#guard_msgs in
 example : x + 1 = 1 + x := by simp? [Nat.add_comm, Nat.mul_comm]
+/-- info: Try this: dsimp only -/
+#guard_msgs in
 example : 1 + 1 = 2 := by dsimp?
 
 @[simp] def bar (z : Nat) := 1 + z
@@ -12,11 +17,19 @@ example : 1 + 1 = 2 := by dsimp?
   | 0, z => bar z
   | _+1, z => baz z
 
+/--
+info: Try this: simp only [foo, bar]
+---
+info: Try this: simp only [foo, baz]
+-/
+#guard_msgs in
 example : foo x y = 1 + y := by
   cases x <;> simp? -- two printouts:
   -- "Try this: simp only [foo, bar]"
   -- "Try this: simp only [foo, baz]"
 
+/-- info: Try this: simp only [foo, bar, baz] -/
+#guard_msgs in
 example : foo x y = 1 + y := by
   squeeze_scope
     cases x <;> simp -- only one printout: "Try this: simp only [foo, baz, bar]"

test/simpa.lean

@@ -17,10 +17,13 @@ def foo (n : α) := [n]
 
 section unnecessarySimpa
 
--- TODO: check that these lint in the test harness
+/-- warning: try 'simp' instead of 'simpa' [linter.unnecessarySimpa] -/
+#guard_msgs in
 example : foo n = [n] := by
   simpa only [foo]
 
+/-- warning: try 'simp at h' instead of 'simpa using h' [linter.unnecessarySimpa] -/
+#guard_msgs in
 example (h : foo n ≠ [n]) : False := by
   simpa [foo] using h
 
@@ -70,8 +73,10 @@ theorem implicit_lambda2 (h : a = 2) : ∀ {x : Nat}, a = 2 := by
 theorem no_implicit_lambda (h : ∀ {x : Nat}, a = x) : ∀ {x : Nat}, a = x := by
   simpa using @h
 
+#guard_msgs (drop warning) in
 theorem thm : (a : Int) ≤ b - c ↔ a + b ≤ c := sorry
 
+#guard_msgs (drop warning) in
 theorem thm2 : (b : Int) - c ≤ (a - b) - (a - c) := sorry
 
 example : (b - c : Int) + (a - b) + a ≤ c := by