diff --git a/test/Explode.lean b/test/Explode.lean index 1091edfa1499ad..365331fea18442 100644 --- 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 index da09045e68174f..0428a0cc91ba1c 100644 --- 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 index 656d3da768f53b..bf8cdf89bf6f18 100644 --- 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 index 3ff71afaa98a8e..871d32076caa6d 100644 --- 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 index 05ec457919f65f..68798c6dd16270 100644 --- 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 index 18bcb03f6c14f6..c1679d90a92840 100644 --- 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 index cdca02d1d189f6..6828096e096964 100644 --- 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