Fix setOption linter in tests: mostly disable it; in one instance, on…

…e option could be simply removed.
leanprover-community · May 22, 2024 · b683b75 · b683b75
1 parent b9903b0
commit b683b75
Show file tree

Hide file tree

Showing 7 changed files with 6 additions and 2 deletions.
diff --git a/test/Explode.lean b/test/Explode.lean
@@ -24,6 +24,7 @@ info: true_iff : ∀ (p : Prop), (True ↔ p) = p
 -/
 #guard_msgs in #explode true_iff
 
+set_option linter.setOption false
 -- On command line, tests format functions with => rather than ↦ without this.
 set_option pp.unicode.fun true
 

diff --git a/test/LibrarySearch/IsCompact.lean b/test/LibrarySearch/IsCompact.lean
@@ -1,8 +1,6 @@
 import Mathlib.Topology.Instances.Real
 import Mathlib.Topology.Algebra.Order.Compact
 
-set_option pp.unicode.fun true
-
 -- TODO: uses sorry, but is hidden behind the `apply?`
 /-- warning: declaration uses 'sorry' -/
 #guard_msgs(warning, drop info) in

diff --git a/test/LibrarySearch/basic.lean b/test/LibrarySearch/basic.lean
@@ -6,6 +6,7 @@ import Mathlib.Data.Real.Basic
 
 set_option autoImplicit true
 
+set_option linter.setOption false
 -- Enable this option for tracing:
 -- set_option trace.Tactic.librarySearch true
 -- And this option to trace all candidate lemmas before application.

diff --git a/test/Recall.lean b/test/Recall.lean
@@ -3,6 +3,7 @@ import Mathlib.Analysis.Calculus.Deriv.Basic
 import Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
 import Mathlib.Data.Complex.Exponential
 
+set_option linter.setOption false
 -- Remark: When the test is run by make/CI, this option is not set, so we set it here.
 set_option pp.unicode.fun true
 set_option autoImplicit true

diff --git a/test/delabLinearIndependent.lean b/test/delabLinearIndependent.lean
@@ -1,5 +1,6 @@
 import Mathlib.LinearAlgebra.LinearIndependent
 
+set_option linter.setOption false
 set_option pp.unicode.fun true
 
 variable {K V : Type*} [DivisionRing K] [AddCommGroup V] [Module K V] {s : Set V} {x : V}

diff --git a/test/linarith.lean b/test/linarith.lean
@@ -8,6 +8,7 @@ import Mathlib.Data.Rat.Order
 private axiom test_sorry : ∀ {α}, α
 set_option linter.unusedVariables false
 set_option autoImplicit true
+set_option linter.setOption false
 set_option pp.mvars false
 
 example [LinearOrderedCommRing α] {a b : α} (h : a < b) (w : b < a) : False := by

diff --git a/test/vec_notation.lean b/test/vec_notation.lean
@@ -8,6 +8,7 @@ open Lean
 open Lean.Meta
 open Qq
 
+set_option linter.setOption false in
 set_option pp.unicode.fun false
 
 /-! These tests are testing `PiFin.toExpr` and fail with