chore: remove set_option grind.warning false (#8714)

This PR removes the now unnecessary `set_option grind.warning false`
statements, now that the warning is disabled by default.

src/Std/Tactic/BVDecide/LRAT/Internal/Assignment.lean

@@ -9,8 +9,6 @@ import Std.Tactic.BVDecide.LRAT.Internal.Entails
 import Std.Tactic.BVDecide.LRAT.Internal.PosFin
 import Init.Grind
 
-set_option grind.warning false
-
 namespace Std.Tactic.BVDecide
 namespace LRAT
 namespace Internal

src/Std/Tactic/BVDecide/LRAT/Internal/CNF.lean

@@ -6,8 +6,6 @@ Authors: Josh Clune
 prelude
 import Std.Tactic.BVDecide.LRAT.Internal.Formula.Class
 
-set_option grind.warning false
-
 namespace Std.Tactic.BVDecide
 namespace LRAT
 namespace Internal

src/Std/Tactic/BVDecide/LRAT/Internal/Clause.lean

@@ -12,8 +12,6 @@ import Std.Tactic.BVDecide.LRAT.Internal.PosFin
 import Std.Tactic.BVDecide.LRAT.Internal.Assignment
 import Init.Grind
 
-set_option grind.warning false
-
 namespace Std.Tactic.BVDecide
 namespace LRAT
 namespace Internal

src/Std/Tactic/BVDecide/LRAT/Internal/Formula/Lemmas.lean

@@ -7,8 +7,6 @@ prelude
 import Std.Tactic.BVDecide.LRAT.Internal.Formula.Implementation
 import Std.Tactic.BVDecide.LRAT.Internal.CNF
 
-set_option grind.warning false -- I've only made a partial effort to use grind here so far.
-
 /-!
 This module contains basic statements about the invariants that are satisfied by the LRAT checker
 implementation in `Implementation`.

src/Std/Tactic/BVDecide/LRAT/Internal/Formula/RatAddResult.lean

@@ -11,8 +11,6 @@ This module contains the implementation of RAT-based clause adding for the defau
 implementation.
 -/
 
-set_option grind.warning false -- I've only made a partial effort to use grind here so far.
-
 namespace Std.Tactic.BVDecide
 namespace LRAT
 namespace Internal

src/Std/Tactic/BVDecide/LRAT/Internal/Formula/RatAddSound.lean

@@ -11,8 +11,6 @@ This module contains the verification of RAT-based clause adding for the default
 implementation.
 -/
 
-set_option grind.warning false -- I've only made a partial effort to use grind here so far.
-
 namespace Std.Tactic.BVDecide
 namespace LRAT
 namespace Internal

src/Std/Tactic/BVDecide/LRAT/Internal/Formula/RupAddResult.lean

@@ -11,8 +11,6 @@ This module contains the implementation of RUP-based clause adding for the defau
 implementation.
 -/
 
-set_option grind.warning false -- I've only made a partial effort to use grind here so far.
-
 namespace Std.Tactic.BVDecide
 namespace LRAT
 namespace Internal

src/Std/Tactic/BVDecide/LRAT/Internal/Formula/RupAddSound.lean

@@ -11,7 +11,6 @@ This module contains the verification of RUP-based clause adding for the default
 implementation.
 -/
 
-set_option grind.warning false -- I've only made a partial effort to use grind here so far.
 namespace Std.Tactic.BVDecide
 namespace LRAT
 namespace Internal

src/Std/Tactic/BVDecide/LRAT/Internal/LRATCheckerSound.lean

@@ -8,8 +8,6 @@ import Std.Tactic.BVDecide.LRAT.Internal.LRATChecker
 import Std.Tactic.BVDecide.LRAT.Internal.CNF
 import Std.Tactic.BVDecide.LRAT.Internal.Actions
 
-set_option grind.warning false
-
 namespace Std.Tactic.BVDecide
 namespace LRAT
 namespace Internal

tests/lean/grind/experiments/list.lean

@@ -6,8 +6,6 @@ It may still be a good source of ideas for `grind` attributes, or `grind` bugs!
 But it's also fine to just delete it at some point.
 -/
 
-set_option grind.warning false
-
 -- Rejected `grind` attributes:
 -- attribute [grind] List.getElem?_eq_getElem -- This is way too slow, it adds about 30% time to this file.
 -- attribute [grind] List.not_mem_nil -- unnecessary

tests/lean/grind/experiments/map.lean

@@ -1,8 +1,6 @@
 import Std.Data.HashMap
 import Std.Data.DHashMap
 import Std.Data.ExtHashMap
-set_option grind.warning false
-
 open Std
 
 -- Do we want this?

tests/lean/grind/experiments/option.lean

@@ -1,7 +1,5 @@
 open Option
 
-set_option grind.warning false
-
 -- TODO: the following lemmas currently fail, but could be solved with some subset of the following attributes:
 -- I haven't added them yet, because the nuclear option of `[grind cases]` is tempting, but a bit scary.
 

tests/lean/grind/grind_lrat_internal_error.lean

@@ -1,5 +1,3 @@
-set_option grind.warning false
-
 namespace Std
 namespace Sat
 

tests/lean/grind/grind_palindrome.lean

@@ -1,5 +1,3 @@
-set_option grind.warning false
-
 def IsPalindrome (xs : Array Nat) : Prop := xs.reverse = xs
 
 def checkPalin1 (xs : Array Nat) : Bool :=

tests/lean/grind/ordered_modules.lean

@@ -1,7 +1,5 @@
 open Lean.Grind
 
-set_option grind.warning false
-
 variable (R : Type u) [IntModule R] [NoNatZeroDivisors R] [Preorder R] [IntModule.IsOrdered R]
 
 example (a b c : R) (h : a < b) : a + c < b + c := by grind

tests/lean/grind/sublist.lean

@@ -1,7 +1,5 @@
 open List
 
-set_option grind.warning false
-
 example (h : zs <+ ys) (w : xs ++ ys <+ zs) (h' : ¬xs = []) : False := by
   fail_if_success grind
   -- I'm not sure how to make progress here without manually adding that since `xs ≠ []`, it must be a `cons`.

tests/lean/run/grind_abstract_mvars.lean

@@ -1,5 +1,3 @@
-set_option grind.warning false
-
 example (xs : Array Nat)
     (w : ∀ (j : Nat), 0 ≤ j → ∀ (x : j < xs.size / 2), xs[j] = xs[xs.size - 1 - j])
     (i : Nat) (hi₁ : i < xs.reverse.size) (hi₂ : i < xs.size) (h : i < xs.size / 2) : xs.reverse[i] = xs[i] := by

tests/lean/run/grind_append_issue.lean

@@ -1,6 +1,4 @@
 reset_grind_attrs%
-set_option grind.warning false
-
 attribute [grind] List.length_cons List.length_nil List.length_append
 attribute [grind] List.nil_append List.getElem_cons
 attribute [grind] List.eq_nil_of_length_eq_zero List.getElem_append_right

tests/lean/run/grind_array.lean

@@ -1,4 +1,2 @@
-set_option grind.warning false
-
 example {l : List α} {i : USize} {a : α} {h : i.toNat < l.toArray.size} :
     l.toArray.uset i a h = (l.set i.toNat a).toArray := by grind

tests/lean/run/grind_bintree.lean

@@ -1,4 +1,3 @@
-set_option grind.warning false
 reset_grind_attrs%
 
 attribute [grind] List.append_assoc List.cons_append List.nil_append

tests/lean/run/grind_bool_diseq.lean

@@ -1,5 +1,3 @@
-set_option grind.warning false
-
 example (f : Bool → Nat) : (x = y ↔ q) → ¬ q → y = false → f x = 0 → f true = 0 := by
   grind (splits := 0)
 

tests/lean/run/grind_bool_prop.lean

@@ -1,4 +1,3 @@
-set_option grind.warning false
 example (f : Bool → Nat) : f (a && b) = 0 → a = false → f false = 0 := by grind (splits := 0)
 example (f : Bool → Nat) : f (a && b) = 0 → b = false → f false = 0 := by grind (splits := 0)
 example (f : Bool → Nat) : f (a && b) = 0 → a = true → f b = 0 := by grind (splits := 0)

tests/lean/run/grind_casting_issue.lean

@@ -1,5 +1,4 @@
 
-set_option grind.warning false
 @[grind] def codelen (c: List Bool) : Int := c.length
 
 theorem issue1 : codelen [] = 0 := by grind

tests/lean/run/grind_cat.lean

@@ -1,5 +1,3 @@
-set_option grind.warning false
-
 universe v v₁ v₂ v₃ u u₁ u₂ u₃
 
 namespace CategoryTheory

tests/lean/run/grind_clear_error.lean

@@ -1,6 +1,4 @@
 reset_grind_attrs%
-set_option grind.warning false
-
 attribute [grind] List.not_mem_nil
 
 /--

tests/lean/run/grind_congr.lean

@@ -1,6 +1,4 @@
 import Lean
-set_option grind.warning false
-
 def f (a : Nat) := a + a + a
 def g (a : Nat) := a + a
 

tests/lean/run/grind_congr_hash_issue.lean

@@ -1,4 +1,3 @@
-set_option grind.warning false
 set_option grind.debug true
 
 opaque f : Nat → Nat

tests/lean/run/grind_constProp.lean

@@ -1,7 +1,5 @@
 reset_grind_attrs%
 
-set_option grind.warning false
-
 attribute [grind cases] Or
 attribute [grind =] List.length_nil List.length_cons Option.getD
 

tests/lean/run/grind_const_pattern.lean

@@ -1,4 +1,3 @@
-set_option grind.warning false
 reset_grind_attrs%
 
 attribute [grind] List.map_append

tests/lean/run/grind_countP.lean

@@ -1,4 +1,3 @@
-set_option grind.warning false
 variable {α : Type u} {l : List α} {P Q : α → Bool}
 
 attribute [grind] List.countP_nil List.countP_cons

tests/lean/run/grind_cutsat_auto.lean

@@ -1,5 +1,3 @@
-set_option grind.warning false
-
 example : ∀ x : Int, x > 7 → 2 * x > 14 := by
   grind
 

tests/lean/run/grind_cutsat_cooper.lean

@@ -1,6 +1,4 @@
 import Std.Internal.Rat
-set_option grind.warning false
-
 example (x y : Int) :
     27 ≤ 11*x + 13*y →
     11*x + 13*y ≤ 45 →

tests/lean/run/grind_cutsat_diseq_1.lean

@@ -1,4 +1,3 @@
-set_option grind.warning false
 set_option grind.debug true
 open Int.Linear
 

tests/lean/run/grind_cutsat_diseq_2.lean

@@ -1,4 +1,3 @@
-set_option grind.warning false
 set_option grind.debug true
 open Int.Linear
 

tests/lean/run/grind_cutsat_diseq_3.lean

@@ -1,4 +1,3 @@
-set_option grind.warning false
 set_option grind.debug true
 open Int.Linear
 

tests/lean/run/grind_cutsat_diseq_cooper.lean

@@ -1,5 +1,3 @@
-set_option grind.warning false
-
 theorem ex1 (x : Int) : 10 ≤ x → x ≤ 20 → x ≠ 11 → 11 ∣ x → False := by
   grind
 

tests/lean/run/grind_cutsat_div_1.lean

@@ -1,4 +1,3 @@
-set_option grind.warning false
 set_option grind.debug true
 set_option pp.structureInstances false
 open Int.Linear

tests/lean/run/grind_cutsat_div_mod.lean

@@ -1,5 +1,3 @@
-set_option grind.warning false
-
 example (x y : Int) : x / 2 + y = 3 → x = 5 → y = 1 := by
   grind
 

tests/lean/run/grind_cutsat_eq_1.lean

@@ -1,4 +1,3 @@
-set_option grind.warning false
 set_option grind.debug true
 open Int.Linear
 

tests/lean/run/grind_cutsat_le_1.lean

@@ -1,4 +1,3 @@
-set_option grind.warning false
 set_option grind.debug true
 
 /--

tests/lean/run/grind_cutsat_le_2.lean

@@ -1,4 +1,3 @@
-set_option grind.warning false
 set_option grind.debug true
 open Int.Linear
 

tests/lean/run/grind_cutsat_natCast_propagation.lean

@@ -1,5 +1,3 @@
-set_option grind.warning false
-
 example (a b : Nat) : a  = a + b - b := by
   grind
 

tests/lean/run/grind_cutsat_nat_dvd.lean

@@ -1,5 +1,3 @@
-set_option grind.warning false
-
 theorem ex₁ (a : Nat) (h₁ : 2 ∣ a) (h₂ : 2 ∣ a + 1) : False := by
   grind
 

tests/lean/run/grind_cutsat_nat_eq.lean

@@ -1,5 +1,3 @@
-set_option grind.warning false
-
 example (a b c : Nat) : a = 0 → b = 0 → c ≥ a + b := by
   grind
 

tests/lean/run/grind_cutsat_nat_le.lean

@@ -1,5 +1,3 @@
-set_option grind.warning false
-
 theorem ex1 (x y z : Nat) : x < y + z → y + 1 < z → z + x < 3*z := by
   grind
 

tests/lean/run/grind_cutsat_omega.lean

@@ -1,5 +1,3 @@
-set_option grind.warning false
-
 example (_ : (1 : Int) < (0 : Int)) : False := by grind
 example (_ : (0 : Int) < (0 : Int)) : False := by grind
 example (_ : (0 : Int) < (1 : Int)) : True := by grind

tests/lean/run/grind_cutsat_tests.lean

@@ -1,5 +1,3 @@
-set_option grind.warning false
-
 example (w x y z : Int) :
   2*w + 3*x - 4*y + z = 10 →
   w - x + 2*y - 3*z = 5 →

tests/lean/run/grind_ematch_gen_pattern.lean

@@ -1,5 +1,3 @@
-set_option grind.warning false
-
 def f (x : Option Nat) (h : x ≠ none) : Nat :=
   match x with
   | none => by contradiction

tests/lean/run/grind_ematch_ground_implicit_inst.lean

@@ -1,5 +1,3 @@
-set_option grind.warning false
-
 example (a : Nat) : max a a = a := by
   grind
 

tests/lean/run/grind_ematch_theorem_activation.lean

@@ -1,6 +1,4 @@
 reset_grind_attrs%
-set_option grind.warning false
-
 attribute [grind] List.length_set
 attribute [grind →] List.eq_nil_of_length_eq_zero
 attribute [grind] List.getElem_set

tests/lean/run/grind_ematch_type_error.lean

@@ -1,5 +1,3 @@
-set_option grind.warning false
-
 example (xs : Array Nat) (w : xs.reverse = xs) (j : Nat) (hj : 0 ≤ j) (hj' : j < xs.size / 2) :
     xs[j] = xs[xs.size - 1 - j] := by
   grind

tests/lean/run/grind_eq_bwd.lean

@@ -1,5 +1,3 @@
-set_option grind.warning false
-
 theorem dummy (x : Nat) : x = x :=
   rfl
 

tests/lean/run/grind_eq_false_of_imp_eq_false.lean

@@ -1,5 +1,4 @@
 reset_grind_attrs%
-set_option grind.warning false
 open List
 
 attribute [grind] List.map_nil

tests/lean/run/grind_eqres_bug.lean

@@ -1,5 +1,3 @@
-set_option grind.warning false
-
 /--
 trace: [grind.eqResolution] ∀ (x : Nat), p x a → ∀ (y : Nat), p y b → ¬x = y, ∀ (y : Nat), p y a → p y b → False
 [grind.ematch.instance] local_0: p c a → ¬p c b

tests/lean/run/grind_eta.lean

@@ -1,6 +1,4 @@
 reset_grind_attrs%
-set_option grind.warning false
-
 example {l : List α} {f : β → α → β} {b : β} :
     l.foldl f b = l.reverse.foldr (fun x y => f y x) b := by
   grind [List.foldr_reverse]

tests/lean/run/grind_etaStruct.lean

@@ -1,5 +1,3 @@
-set_option grind.warning false
-
 opaque f (a : Nat) : Nat × Bool
 
 example (a b : Nat) : (f a).1 = (f b).1 → (f a).2 = (f b).2 → f a = f b := by

tests/lean/run/grind_exfalso.lean

@@ -1,5 +1,3 @@
-set_option grind.warning false
-
 example (x : Nat) (h : x < 0) : Nat → Nat := by
   grind
 

tests/lean/run/grind_fastEraseDups.lean

@@ -3,8 +3,6 @@ import Std.Data.HashSet
 
 open Std
 
-set_option grind.warning false
-
 namespace List
 
 -- Fast duplicate-removing function, using a hash set to check if an element was seen before

tests/lean/run/grind_funext.lean

@@ -1,5 +1,3 @@
-set_option grind.warning false
-
 example (f : (Nat → Nat) → Nat → Nat → Nat) : a = b → f (fun x => a + x) 1 b = f (fun x => b + x) 1 a := by
   grind
 

tests/lean/run/grind_getElem.lean

@@ -1,4 +1,3 @@
-set_option grind.warning false
 reset_grind_attrs%
 
 attribute [grind]

tests/lean/run/grind_getLast_dropLast.lean

@@ -1,6 +1,4 @@
 reset_grind_attrs%
-set_option grind.warning false
-
 open List
 
 theorem length_pos_of_ne_nil {l : List α} (h : l ≠ []) : 0 < l.length := by

tests/lean/run/grind_guide.lean

@@ -11,8 +11,6 @@ we keep all the facts we know about the current goal.
 Remark: Terms known to be true (false) belong to the equivalence class of the term `True` (`False`).
 -/
 
-set_option grind.warning false -- Disables warning messages stating that `grind` is WIP.
-
 example (a b c : α) (f : α → α) : f a = c → a = b → c = f b := by
   grind
 

tests/lean/run/grind_hashmap_list.lean

@@ -1,5 +1,4 @@
 import Std.Data.HashMap
-set_option grind.warning false
 reset_grind_attrs%
 
 open Std

tests/lean/run/grind_hcongr.lean

@@ -1,4 +1,3 @@
-set_option grind.warning false
 def Matrix (m : Type) (n : Type) (α : Type) : Type :=
   m → n → α
 

tests/lean/run/grind_heapsort.lean

@@ -1,6 +1,4 @@
 import Lean
-set_option grind.warning false
-
 /-
 Use `grind` as one of the tactics for array-element access and termination proofs.
 -/

tests/lean/run/grind_heartbeats.lean

@@ -1,5 +1,3 @@
-set_option grind.warning false
-
 opaque f : Nat → Nat
 opaque op : Nat → Nat → Nat
 @[grind] theorem op_comm : op x y = op y x := sorry

tests/lean/run/grind_indexmap.lean

@@ -4,8 +4,6 @@
 
 import Std.Data.HashMap
 
-set_option grind.warning false
-
 macro_rules | `(tactic| get_elem_tactic_extensible) => `(tactic| grind)
 
 open Std

tests/lean/run/grind_indexmap_pre.lean

@@ -3,8 +3,6 @@
 
 import Std.Data.HashMap
 
-set_option grind.warning false
-
 open Std
 
 structure IndexMap (α : Type u) (β : Type v) [BEq α] [Hashable α] where

tests/lean/run/grind_ite.lean

@@ -111,8 +111,6 @@ def IfNormalization : Type := { Z : IfExpr → IfExpr // ∀ e, (Z e).normalized
 -/
 
 -- `grind` is currently experimental, but for now we can suppress the warnings about this.
-set_option grind.warning false
-
 namespace IfExpr
 
 /--

tests/lean/run/grind_ite_congr.lean

@@ -1,5 +1,3 @@
-set_option grind.warning false
-
 example : ((if true then id else id) false) = false := by
   grind
 

tests/lean/run/grind_ite_split_issue.lean

@@ -1,5 +1,3 @@
-set_option grind.warning false
-
 example (a b : Int) : min a b = 10 → a ≥ 10 := by
   grind
 

tests/lean/run/grind_ite_unused_match.lean

@@ -99,8 +99,6 @@ def IfNormalization : Type := { Z : IfExpr → IfExpr // ∀ e, (Z e).normalized
 -/
 
 -- `grind` is currently experimental, but for now we can suppress the warnings about this.
-set_option grind.warning false
-
 namespace IfExpr
 
 attribute [grind] List.mem_cons List.not_mem_nil List.mem_append

tests/lean/run/grind_linarith_1.lean

@@ -1,5 +1,3 @@
-set_option grind.warning false
-
 open Lean.Grind
 
 example [IntModule α] [Preorder α] [IntModule.IsOrdered α] (a b : α)

tests/lean/run/grind_list.lean

@@ -1,6 +1,4 @@
 reset_grind_attrs%
-set_option grind.warning false
-
 namespace List
 
 attribute [local grind =] List.length_cons in

tests/lean/run/grind_list2.lean

@@ -10,7 +10,6 @@
 -- `tests/lean/grind/experiments/list.lean` contains everything from `Data/List/Lemmas.lean`
 -- that still resists `grind`!
 
-set_option grind.warning false
 open List Nat
 
 namespace Hidden

tests/lean/run/grind_list_count.lean

@@ -1,6 +1,4 @@
 
-set_option grind.warning false
-
 open List Nat
 
 namespace List'

tests/lean/run/grind_list_issue.lean

@@ -1,5 +1,4 @@
 reset_grind_attrs%
-set_option grind.warning false
 open List Nat
 
 attribute [grind] List.filter_nil List.filter_cons

tests/lean/run/grind_list_sublist.lean

@@ -1,7 +1,5 @@
 open List
 
-set_option grind.warning false
-
 variable {α} {l₁ l₂ l₃ l₄ l₅ : List α}
 
 example : l₂ ++ l₄ ⊆ l₁ ++ l₂ ++ l₃ ++ l₄ ++ l₅ := by

tests/lean/run/grind_lookahead.lean

@@ -1,4 +1,3 @@
-set_option grind.warning false
 reset_grind_attrs%
 
 attribute [grind] List.eq_nil_of_length_eq_zero

tests/lean/run/grind_map.lean

@@ -4,8 +4,6 @@ import Std.Data.ExtHashMap
 import Std.Data.HashSet
 import Std.Data.TreeMap
 
-set_option grind.warning false
-
 open Std
 
 section

tests/lean/run/grind_mark_nested_proofs_bug.lean

@@ -1,5 +1,3 @@
-set_option grind.warning false
-
 example (as bs cs : Array α) (v : α)
         (i : Nat)
         (h₁ : i < as.size)

tests/lean/run/grind_match_with_eq.lean

@@ -1,5 +1,3 @@
-set_option grind.warning false
-
 def f (a : Option Nat) (h : a ≠ none) : Nat :=
  match a with
  | some a => a

tests/lean/run/grind_mbtc_1.lean

@@ -1,5 +1,3 @@
-set_option grind.warning false
-
 example (f : Int → Int) (x : Int)
     : 0 ≤ x → x ≠ 0 → x ≤ 1 → f x = 2 → f 1 = 2 := by
   grind

tests/lean/run/grind_min.lean

@@ -1,5 +1,3 @@
-set_option grind.warning false
-
 example (as : Array α) (lo hi i j : Nat) (h₁ : lo ≤ i) (_ : i < j) (_ : j ≤ hi) (_ : j < as.size)
     (_ : ¬as.size = 0) : min lo (as.size - 1) ≤ i := by
   grind

tests/lean/run/grind_mvar.lean

@@ -1,7 +1,5 @@
 open List
 reset_grind_attrs%
-set_option grind.warning false
-
 attribute [grind →] Array.eq_empty_of_append_eq_empty eq_nil_of_length_eq_zero
 attribute [grind] Vector.getElem?_append getElem?_dropLast
 

tests/lean/run/grind_natCast.lean

@@ -1,5 +1,3 @@
-set_option grind.warning false
-
 example (x : Nat) : x ≥ (0 : Int) := by grind
 example (x : Nat) : Int.ofNat x ≥ (0 : Int) := by grind
 example (x : Nat) : NatCast.natCast x ≥ 0 := by grind

tests/lean/run/grind_nochrono.lean

@@ -1,5 +1,3 @@
-set_option grind.warning false
-
 -- In the following test, the first 8 case-splits are irrelevant,
 -- and non-choronological backtracking is used to avoid searching
 -- (2^8 - 1) irrelevant branches

tests/lean/run/grind_offset_cnstr.lean

@@ -1,4 +1,3 @@
-set_option grind.warning false
 set_option grind.debug true
 
 /--

tests/lean/run/grind_omega_examples.lean

@@ -1,4 +1,3 @@
-set_option grind.warning false
 example {x y : Nat} (_ : x + y > 10) (_ : x < 5) (_ : y < 5) : False := by grind
 example {x y : Nat} (_ : x + y > 10) (_ : 2 * x < 11) (_ : y < 5) : False := by grind
 example {x y : Nat} (_ : 2 * x + 4 * y = 5) : False := by grind

tests/lean/run/grind_option.lean

@@ -2,8 +2,6 @@
 -- This may prove fragile, so remember it is okay to update the expected output if appropriate!
 -- Hopefully these will act as regression tests against `grind` activating irrelevant lemmas.
 
-set_option grind.warning false
-
 section
 
 variable [BEq α] {o₁ o₂ o₃ o₄ o₅ : Option α}

tests/lean/run/grind_overapplied_ite.lean

@@ -1,5 +1,3 @@
-set_option grind.warning false
-
 example : (if (!false) = true then id else id) false = false := by
   grind
 

tests/lean/run/grind_palindrome2.lean

@@ -1,5 +1,3 @@
-set_option grind.warning false
-
 def IsPalindrome (xs : Array Nat) : Prop := xs.reverse = xs
 
 def checkPalin1 (xs : Array Nat) : Bool :=

tests/lean/run/grind_panic_invariant.lean

@@ -5,8 +5,6 @@
   | star_step : ∀ x y z, R x y → star R y z → star R x z
 
 set_option grind.debug true
-set_option grind.warning false
-
 inductive com: Type where
   | SKIP
   | ASSIGN

tests/lean/run/grind_pre.lean

@@ -1,5 +1,4 @@
 abbrev f (a : α) := a
-set_option grind.warning false
 set_option grind.debug true
 set_option grind.debug.proofs true
 

tests/lean/run/grind_product_eta_and_split.lean

@@ -1,4 +1,3 @@
-set_option grind.warning false
 set_option grind.debug true
 
 def α : Type := Unit × Unit

tests/lean/run/grind_qsort.lean

@@ -5,8 +5,6 @@ Authors: Kim Morrison
 -/
 
 -- TODO: when `grind` is ready for production use, move this file to `src/Init/Data/Array/QSort/Lemmas.lean`.
-set_option grind.warning false
-
 /-!
 # Verification of `Array.qsort`
 

tests/lean/run/grind_regression.lean

@@ -4,7 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Marcus Rossel, Kim Morrison
 -/
 import Lean.Elab.Term
-set_option grind.warning false
 /-!
 These tests are originally from the `lean-egg` repository at
 https://github.com/marcusrossel/lean-egg and were written by Marcus Rossel.

tests/lean/run/grind_ring_1.lean

@@ -1,4 +1,3 @@
-set_option grind.warning false
 set_option grind.debug true
 
 open Lean.Grind

tests/lean/run/grind_ring_2.lean

@@ -1,4 +1,3 @@
-set_option grind.warning false
 set_option grind.debug true
 open Lean.Grind
 

tests/lean/run/grind_ring_3.lean

@@ -1,7 +1,5 @@
 open Lean.Grind
 
-set_option grind.warning false
-
 example {α} [CommRing α] [IsCharP α 0]
     (d t : α)
   (Δ40 : d + t + d * t = 0)