remove set_option pairs

leanprover-community · Oct 8, 2024 · b0fef9b · b0fef9b
1 parent 7ba27f0
commit b0fef9b
Show file tree

Hide file tree

Showing 9 changed files with 14 additions and 89 deletions.
diff --git a/test/AdmitLinter.lean b/test/AdmitLinter.lean
@@ -1,13 +1,14 @@
 import Mathlib.Tactic.Linter.AdmitLinter
 
+set_option linter.admit true
+
 /--
 warning: declaration uses 'sorry'
 ---
 warning: The `admit` tactic is discouraged: please consider using the synonymous `sorry` instead.
 note: this linter can be disabled with `set_option linter.admit false`
 -/
 #guard_msgs in
-set_option linter.admit true in
 example : True := by admit
 
 /--
@@ -26,7 +27,6 @@ warning: The `admit` tactic is discouraged: please consider using the synonymous
 note: this linter can be disabled with `set_option linter.admit false`
 -/
 #guard_msgs in
-set_option linter.admit true in
 example : True ∧ True := by
   have : True := by
     · admit

diff --git a/test/FlexibleLinter.lean b/test/FlexibleLinter.lean
@@ -3,7 +3,7 @@ import Mathlib.Tactic.Linter.FlexibleLinter
 import Mathlib.Tactic.Abel
 import Mathlib.Tactic.Ring
 
-set_option linter.flexible false
+set_option linter.flexible true
 
 /--
 warning: 'simp at h' is a flexible tactic modifying 'h'…
@@ -12,7 +12,6 @@ note: this linter can be disabled with `set_option linter.flexible false`
 info: … and 'exact h' uses 'h'!
 -/
 #guard_msgs in
-set_option linter.flexible true in
 example (h : 0 + 0 = 0) : True := by
   simp at h
   try exact h
@@ -45,7 +44,6 @@ note: this linter can be disabled with `set_option linter.flexible false`
 info: … and 'assumption' uses '⊢'!
 -/
 #guard_msgs in
-set_option linter.flexible true in
 example {a b : Nat} (h : a = b) : a + 0 = b := by
   simp
   induction a <;> assumption
@@ -58,7 +56,6 @@ note: this linter can be disabled with `set_option linter.flexible false`
 info: … and 'exact h' uses 'h'!
 -/
 #guard_msgs in
-set_option linter.flexible true in
 example (h : 0 = 0 ∨ 0 = 0) : True := by
   cases h <;>
     rename_i h <;>
@@ -78,7 +75,6 @@ note: this linter can be disabled with `set_option linter.flexible false`
 info: … and 'contradiction' uses '⊢'!
 -/
 #guard_msgs in
-set_option linter.flexible true in
 example (h : 0 = 1 ∨ 0 = 1) : 0 = 1 ∧ 0 = 1 := by
   cases h <;> simp
   on_goal 2 => · contradiction
@@ -100,7 +96,6 @@ note: this linter can be disabled with `set_option linter.flexible false`
 info: … and 'contradiction' uses '⊢'!
 -/
 #guard_msgs in
-set_option linter.flexible true in
 example (h : 0 = 1 ∨ 0 = 1) : 0 = 1 ∧ 0 = 1 := by
   cases h <;> simp
   · contradiction
@@ -119,7 +114,6 @@ info: … and 'rw [← Classical.not_not (a := True)] at h' uses 'h'!
 -/
 #guard_msgs in
 -- `simp at h` stains `h` but not other locations
-set_option linter.flexible true in
 example {h : 0 = 0} {k : 1 = 1} : True := by
   simp at h k;
   rw [← Classical.not_not (a := True)]
@@ -149,7 +143,6 @@ info: … and 'rw [add_comm]' uses '⊢'!
 -/
 #guard_msgs in
 -- `norm_num` is allowed after `simp`, but "passes along the stain".
-set_option linter.flexible true in
 example {a : Rat} : a + (0 + 2 + 1 : Rat) = 3 + a := by
   simp
   norm_num
@@ -163,7 +156,6 @@ info: … and 'exact h.symm' uses '⊢'!
 -/
 #guard_msgs in
 -- `congr` is allowed after `simp`, but "passes along the stain".
-set_option linter.flexible true in
 example {a b : Nat} (h : a = b) : a + b + 0 = b + a := by
   simp
   congr
@@ -208,7 +200,6 @@ note: this linter can be disabled with `set_option linter.flexible false`
 info: … and 'contradiction' uses '⊢'!
 -/
 #guard_msgs in
-set_option linter.flexible true in
 example (h : 0 = 1 ∨ 0 = 1) : 0 = 1 ∧ 0 = 1 := by
   cases h <;> simp
   · simp_all
@@ -234,7 +225,6 @@ note: this linter can be disabled with `set_option linter.flexible false`
 info: … and 'rw [← Classical.not_not (a := True)] at h' uses 'h'!
 -/
 #guard_msgs in
-set_option linter.flexible true in
 -- `simp at h` stains `h` but not other locations
 example {h : 0 = 0} {k : 1 = 1} : ¬ ¬ True := by
   simp at h
@@ -256,7 +246,6 @@ note: this linter can be disabled with `set_option linter.flexible false`
 info: … and 'rw [← Classical.not_not (a := True)] at h' uses 'h'!
 -/
 #guard_msgs in
-set_option linter.flexible true in
 -- `simp at h` stains `h` but not other locations
 example {h : 0 = 0} {k : 1 = 1} : True := by
   simp at h k
@@ -274,7 +263,6 @@ info: … and 'rw [← Classical.not_not (a := True)] at h' uses 'h'!
 -/
 #guard_msgs in
 -- `simp at h` stains `h` but not other locations
-set_option linter.flexible true in
 example {h : 0 = 0} : True := by
   simp at h
   rw [← Classical.not_not (a := True)]
@@ -289,7 +277,6 @@ note: this linter can be disabled with `set_option linter.flexible false`
 info: … and 'rwa [← Classical.not_not (a := False)]' uses '⊢'!
 -/
 #guard_msgs in
-set_option linter.flexible true in
 example {h : False} : 0 = 1 := by
   simp
   rw [← Classical.not_not (a := False)] at h
@@ -303,7 +290,6 @@ note: this linter can be disabled with `set_option linter.flexible false`
 info: … and 'rwa [← Classical.not_not (a := False)]' uses '⊢'!
 -/
 #guard_msgs in
-set_option linter.flexible true in
 example {h : False} : 0 = 1 ∧ 0 = 1 := by
   constructor
   · simpa

diff --git a/test/Lint.lean b/test/Lint.lean
@@ -2,17 +2,11 @@ import Mathlib.Tactic.Linter.Lint
 import Mathlib.Tactic.ToAdditive
 import Mathlib.Order.SetNotation
 
--- TODO: the linter also runs on the #guard_msg, so disable it once
--- See https://leanprover.zulipchat.com/#narrow/stream/348111-std4/topic/.23guard_msgs.20doesn't.20silence.20warnings/near/423534679
-
-set_option linter.dupNamespace false
-
 /--
 warning: The namespace 'add' is duplicated in the declaration 'add.add'
 note: this linter can be disabled with `set_option linter.dupNamespace false`
 -/
 #guard_msgs in
-set_option linter.dupNamespace true in
 def add.add := True
 
 namespace Foo
@@ -22,7 +16,6 @@ warning: The namespace 'Foo' is duplicated in the declaration 'Foo.Foo.foo'
 note: this linter can be disabled with `set_option linter.dupNamespace false`
 -/
 #guard_msgs in
-set_option linter.dupNamespace true in
 def Foo.foo := True
 
 -- the `dupNamespace` linter does not notice that `to_additive` created `Foo.add.add`.
@@ -41,7 +34,6 @@ warning: The namespace 'Nat' is duplicated in the declaration 'Foo.Nat.Nat.Nats'
 note: this linter can be disabled with `set_option linter.dupNamespace false`
 -/
 #guard_msgs in
-set_option linter.dupNamespace true in
 alias Nat.Nats := Nat
 
 end Nat
@@ -54,14 +46,12 @@ warning: The namespace 'add' is duplicated in the declaration 'add.add'
 note: this linter can be disabled with `set_option linter.dupNamespace false`
 -/
 #guard_msgs in
-set_option linter.dupNamespace true in
 export Nat (add)
 
 end add
 
 section cdotLinter
-
-set_option linter.style.cdot false
+set_option linter.style.cdot true
 
 set_option linter.globalAttributeIn false in
 /--
@@ -75,29 +65,25 @@ warning: Please, use '·' (typed as `\.`) instead of '.' as 'cdot'.
 note: this linter can be disabled with `set_option linter.style.cdot false`
 -/
 #guard_msgs in
-set_option linter.style.cdot true in
 attribute [instance] Int.add in
 instance : Inhabited Nat where
   default := by
     . have := 0
       · have : Nat → Nat → Nat := (· + .)
         . exact 0
 
-set_option linter.style.cdot false in
 /--
 warning: Please, use '·' (typed as `\.`) instead of '.' as 'cdot'.
 note: this linter can be disabled with `set_option linter.style.cdot false`
 -/
 #guard_msgs in
-set_option linter.style.cdot true in
 example : Add Nat where add := (. + ·)
 
 /--
 warning: Please, use '·' (typed as `\.`) instead of '.' as 'cdot'.
 note: this linter can be disabled with `set_option linter.style.cdot false`
 -/
 #guard_msgs in
-set_option linter.style.cdot true in
 example : Add Nat where add := (. + ·)
 
 /--
@@ -109,7 +95,6 @@ warning: This central dot `·` is isolated; please merge it with the next line.
 warning: This central dot `·` is isolated; please merge it with the next line.
 -/
 #guard_msgs in
-set_option linter.style.cdot true in
 example : Nat := by
   have : Nat := by
     ·
@@ -123,7 +108,6 @@ example : Nat := by
   exact 0
 
 #guard_msgs in
-set_option linter.style.cdot true in
 example : True := by
   have : Nat := by
     -- This is how code should look: no error.
@@ -132,9 +116,9 @@ example : True := by
   trivial
 
 end cdotLinter
+set_option linter.style.dollarSyntax true
 
 set_option linter.globalAttributeIn false in
-set_option linter.style.dollarSyntax false in
 /--
 warning: Please use '<|' instead of '$' for the pipe operator.
 note: this linter can be disabled with `set_option linter.style.dollarSyntax false`
@@ -143,7 +127,6 @@ warning: Please use '<|' instead of '$' for the pipe operator.
 note: this linter can be disabled with `set_option linter.style.dollarSyntax false`
 -/
 #guard_msgs in
-set_option linter.style.dollarSyntax true in
 attribute [instance] Int.add in
 instance (f g : Nat → Nat) : Inhabited Nat where
   default := by
@@ -153,15 +136,14 @@ instance (f g : Nat → Nat) : Inhabited Nat where
 
 section lambdaSyntaxLinter
 
-set_option linter.style.lambdaSyntax false
+set_option linter.style.lambdaSyntax true
 
 /--
 warning: Please use 'fun' and not 'λ' to define anonymous functions.
 The 'λ' syntax is deprecated in mathlib4.
 note: this linter can be disabled with `set_option linter.style.lambdaSyntax false`
 -/
 #guard_msgs in
-set_option linter.style.lambdaSyntax true in
 example : ℕ → ℕ := λ _ ↦ 0
 
 /--
@@ -170,7 +152,6 @@ The 'λ' syntax is deprecated in mathlib4.
 note: this linter can be disabled with `set_option linter.style.lambdaSyntax false`
 -/
 #guard_msgs in
-set_option linter.style.lambdaSyntax true in
 def foo : Bool := by
   let _f : ℕ → ℕ := λ _ ↦ 0
   exact true
@@ -183,7 +164,6 @@ The 'λ' syntax is deprecated in mathlib4.
 note: this linter can be disabled with `set_option linter.style.lambdaSyntax false`
 -/
 #guard_msgs in
-set_option linter.style.lambdaSyntax true in
 example : ℕ → ℕ := by exact λ n ↦ 3 * n + 1
 
 /--
@@ -202,7 +182,6 @@ The 'λ' syntax is deprecated in mathlib4.
 note: this linter can be disabled with `set_option linter.style.lambdaSyntax false`
 -/
 #guard_msgs in
-set_option linter.style.lambdaSyntax true in
 example : ℕ → ℕ → ℕ → ℕ := by
   have (n : ℕ) : True := trivial
   have : (Set.univ : Set ℕ) = ⋃ (i : ℕ), (Set.iUnion λ j ↦ ({0, j} : Set ℕ)) := sorry
@@ -223,7 +202,6 @@ The 'λ' syntax is deprecated in mathlib4.
 note: this linter can be disabled with `set_option linter.style.lambdaSyntax false`
 -/
 #guard_msgs in
-set_option linter.style.lambdaSyntax true in
 example : True := by
   have : 0 = 0 ∧ 0 = 0 ∧ 1 + 3 = 4 := by
     refine ⟨by trivial, by
@@ -245,27 +223,24 @@ The 'λ' syntax is deprecated in mathlib4.
 note: this linter can be disabled with `set_option linter.style.lambdaSyntax false`
 -/
 #guard_msgs in
-set_option linter.style.lambdaSyntax true in
-example : ℕ → ℕ := set_option linter.style.lambdaSyntax false in λ _ ↦ 0
+example : ℕ → ℕ := λ _ ↦ 0
 
 set_option linter.style.lambdaSyntax false
 #guard_msgs in
-example : ℕ → ℕ := set_option linter.style.lambdaSyntax true in λ _ ↦ 0
+example : ℕ → ℕ := λ _ ↦ 0
 
 end lambdaSyntaxLinter
 
-set_option linter.style.longLine false
+set_option linter.style.longLine true
 /--
 warning: This line exceeds the 100 character limit, please shorten it!
 note: this linter can be disabled with `set_option linter.style.longLine false`
 -/
 #guard_msgs in
-set_option linter.style.longLine true in
 /-!                                                                                                -/
 
 #guard_msgs in
 -- Lines with more than 100 characters containing URLs are allowed.
-set_option linter.style.longLine true in
 /-!  http                                                                                          -/
 
 set_option linter.style.longLine true
@@ -292,5 +267,4 @@ You can use "string gaps" to format long strings: within a string quotation, usi
 note: this linter can be disabled with `set_option linter.style.longLine false`
 -/
 #guard_msgs in
-set_option linter.style.longLine true in
 #check "                              \"                                                            "