From db6aa9d8d3dd2ce2cda1e21ec2beab168c01201a Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Fri, 6 Mar 2026 11:23:27 +0800 Subject: [PATCH] feat: move instance-class check to declaration site (#12325) This PR adds a warning to any `def` of class type that does not also declare an appropriate reducibility. The warning check runs after elaboration (checking the actual reducibility status via `getReducibilityStatus`) rather than syntactically checking modifiers before elaboration. This is necessary to accommodate patterns like `@[to_additive (attr := implicit_reducible)]` in Mathlib, where the reducibility attribute is applied during `.afterCompilation` by another attribute, and would be missed by a purely syntactic check. --------- Co-authored-by: Paul Reichert <6992158+datokrat@users.noreply.github.com> Co-authored-by: Kim Morrison Co-authored-by: Claude Opus 4.6 --- .github/workflows/build-template.yml | 2 +- src/Init/Data/Char/Lemmas.lean | 4 +- .../Combinators/Monadic/FlatMap.lean | 3 +- src/Init/Data/Iterators/Consumers/Loop.lean | 6 +- .../Iterators/Consumers/Monadic/Loop.lean | 10 +- .../Internal/LawfulMonadLiftFunction.lean | 4 +- .../Data/Iterators/Lemmas/Consumers/Loop.lean | 4 +- .../Lemmas/Consumers/Monadic/Loop.lean | 2 +- src/Init/Data/Iterators/ToIterator.lean | 4 +- src/Init/Data/Order/Factories.lean | 10 +- src/Init/Data/Order/FactoriesExtra.lean | 4 +- src/Init/Data/Order/Opposite.lean | 6 +- src/Init/Data/Order/PackageFactories.lean | 14 +- .../Data/Range/Polymorphic/RangeIterator.lean | 9 +- .../Range/Polymorphic/UpwardEnumerable.lean | 4 +- src/Lean/Elab/Deriving/TypeName.lean | 11 +- src/Lean/Elab/MutualDef.lean | 25 ++- .../Iterators/Lemmas/Equivalence/HetT.lean | 3 +- stage0/src/stdlib_flags.h | 2 + tests/elab/1158.lean | 2 + tests/elab/1692.lean | 2 + tests/elab/2115.lean.out.expected | 4 + tests/elab/2461.lean | 2 + tests/elab/366.lean.out.expected | 1 + tests/elab/3965_2.lean | 2 + tests/elab/3965_2.lean.out.expected | 26 +-- tests/elab/3965_3.lean | 2 + tests/elab/3965_3.lean.out.expected | 58 +++--- tests/elab/4171.lean | 2 + tests/elab/4171.lean.out.expected | 56 +++--- tests/elab/4203.lean | 2 + tests/elab/5176.lean | 2 + tests/elab/6123_cat_adjunction.lean | 2 + .../6123_cat_adjunction.lean.out.expected | 38 ++-- tests/elab/616.lean | 2 + tests/elab/664.lean | 2 + tests/elab/796.lean | 2 + tests/elab/9624.lean | 2 + tests/elab/KyleAlg.lean | 2 + tests/elab/aStructPerfIssue.lean | 2 + tests/elab/binop_binrel_perf_issue.lean | 2 + .../binop_binrel_perf_issue.lean.out.expected | 80 ++++---- tests/elab/congrSimpMathlibIssue.lean | 2 + tests/elab/derivingBEq.lean | 2 + tests/elab/derivingBEqLinear.lean | 2 + tests/elab/derivingInhabited.lean | 2 + tests/elab/derivingNonempty.lean | 2 + tests/elab/grind_cat2.lean | 2 + tests/elab/grind_cat2.lean.out.expected | 4 +- tests/elab/grind_section_var.lean | 2 + tests/elab/inductionTacticBug.lean | 2 + tests/elab/instanceReducible.lean | 4 + tests/elab/instanceUsingFalse.lean | 2 + tests/elab/methodSpecs.lean | 6 +- tests/elab/modAsClasses.lean | 2 + tests/elab/newfrontend1.lean | 2 + tests/elab/order.lean | 15 +- tests/elab/order.lean.out.expected | 4 +- tests/elab/propagateExpectedType.lean | 2 + tests/elab/simproc_timeout.lean | 2 + tests/elab/simproc_timeout.lean.out.expected | 36 ++-- tests/elab/structInst2.lean | 2 + tests/elab/structWithAlgTCSynth.lean | 2 + .../structWithAlgTCSynth.lean.out.expected | 188 +++++++++--------- tests/elab/synthInstsIssue.lean | 2 + tests/elab/synthInstsIssue.lean.out.expected | 2 +- tests/elab/typeclass_diamond.lean | 2 + tests/elab_fail/2273.lean.out.expected | 1 + .../phashmap_inst_coherence.lean.out.expected | 1 + ...InstanceOutsideNamespace.lean.out.expected | 1 + tests/elab_fail/tcloop.lean.out.expected | 1 + .../run/classDefReducibilityAfterAttr.lean | 31 +++ tests/pkg/module/Module/Imported.lean | 2 + 73 files changed, 447 insertions(+), 305 deletions(-) create mode 100644 tests/lean/run/classDefReducibilityAfterAttr.lean diff --git a/.github/workflows/build-template.yml b/.github/workflows/build-template.yml index 2f41e54ce6..4023f6dfac 100644 --- a/.github/workflows/build-template.yml +++ b/.github/workflows/build-template.yml @@ -131,7 +131,7 @@ jobs: [ -d build ] || mkdir build cd build # arguments passed to `cmake` - OPTIONS=(-DLEAN_EXTRA_MAKE_OPTS=-DwarningAsError=true) + OPTIONS=() if [[ -n '${{ matrix.release }}' ]]; then # this also enables githash embedding into stage 1 library, which prohibits reusing # `.olean`s across commits, so we don't do it in the fast non-release CI diff --git a/src/Init/Data/Char/Lemmas.lean b/src/Init/Data/Char/Lemmas.lean index 25514c8f25..5246a1107b 100644 --- a/src/Init/Data/Char/Lemmas.lean +++ b/src/Init/Data/Char/Lemmas.lean @@ -62,7 +62,7 @@ instance ltTrichotomous : Std.Trichotomous (· < · : Char → Char → Prop) wh trichotomous _ _ h₁ h₂ := Char.le_antisymm (by simpa using h₂) (by simpa using h₁) @[deprecated ltTrichotomous (since := "2025-10-27")] -def notLTAntisymm : Std.Antisymm (¬ · < · : Char → Char → Prop) where +theorem notLTAntisymm : Std.Antisymm (¬ · < · : Char → Char → Prop) where antisymm := Char.ltTrichotomous.trichotomous instance ltAsymm : Std.Asymm (· < · : Char → Char → Prop) where @@ -73,7 +73,7 @@ instance leTotal : Std.Total (· ≤ · : Char → Char → Prop) where -- This instance is useful while setting up instances for `String`. @[deprecated ltAsymm (since := "2025-08-01")] -def notLTTotal : Std.Total (¬ · < · : Char → Char → Prop) where +theorem notLTTotal : Std.Total (¬ · < · : Char → Char → Prop) where total := fun x y => by simpa using Char.le_total y x @[simp] theorem ofNat_toNat (c : Char) : Char.ofNat c.toNat = c := by diff --git a/src/Init/Data/Iterators/Combinators/Monadic/FlatMap.lean b/src/Init/Data/Iterators/Combinators/Monadic/FlatMap.lean index 2658a94191..a1ce3074bf 100644 --- a/src/Init/Data/Iterators/Combinators/Monadic/FlatMap.lean +++ b/src/Init/Data/Iterators/Combinators/Monadic/FlatMap.lean @@ -362,8 +362,7 @@ def Flatten.instProductivenessRelation [Monad m] [Iterator α m (IterM (α := α case innerDone => apply Flatten.productiveRel_of_right₂ -@[no_expose] -public def Flatten.instProductive [Monad m] [Iterator α m (IterM (α := α₂) m β)] [Iterator α₂ m β] +public theorem Flatten.instProductive [Monad m] [Iterator α m (IterM (α := α₂) m β)] [Iterator α₂ m β] [Finite α m] [Productive α₂ m] : Productive (Flatten α α₂ β m) m := .of_productivenessRelation instProductivenessRelation diff --git a/src/Init/Data/Iterators/Consumers/Loop.lean b/src/Init/Data/Iterators/Consumers/Loop.lean index 005feac839..46a6b6b950 100644 --- a/src/Init/Data/Iterators/Consumers/Loop.lean +++ b/src/Init/Data/Iterators/Consumers/Loop.lean @@ -35,7 +35,7 @@ A `ForIn'` instance for iterators. Its generic membership relation is not easy t so this is not marked as `instance`. This way, more convenient instances can be built on top of it or future library improvements will make it more comfortable. -/ -@[always_inline, inline] +@[always_inline, inline, expose, implicit_reducible] def Iter.instForIn' {α : Type w} {β : Type w} {n : Type x → Type x'} [Monad n] [Iterator α Id β] [IteratorLoop α Id n] : ForIn' n (Iter (α := α) β) β ⟨fun it out => it.IsPlausibleIndirectOutput out⟩ where @@ -53,7 +53,7 @@ instance (α : Type w) (β : Type w) (n : Type x → Type x') [Monad n] /-- An implementation of `for h : ... in ... do ...` notation for partial iterators. -/ -@[always_inline, inline] +@[always_inline, inline, expose, implicit_reducible] def Iter.Partial.instForIn' {α : Type w} {β : Type w} {n : Type x → Type x'} [Monad n] [Iterator α Id β] [IteratorLoop α Id n] : ForIn' n (Iter.Partial (α := α) β) β ⟨fun it out => it.it.IsPlausibleIndirectOutput out⟩ where @@ -71,7 +71,7 @@ instance (α : Type w) (β : Type w) (n : Type x → Type x') [Monad n] A `ForIn'` instance for iterators that is guaranteed to terminate after finitely many steps. It is not marked as an instance because the membership predicate is difficult to work with. -/ -@[always_inline, inline] +@[always_inline, inline, expose, implicit_reducible] def Iter.Total.instForIn' {α : Type w} {β : Type w} {n : Type x → Type x'} [Monad n] [Iterator α Id β] [IteratorLoop α Id n] [Finite α Id] : ForIn' n (Iter.Total (α := α) β) β ⟨fun it out => it.it.IsPlausibleIndirectOutput out⟩ where diff --git a/src/Init/Data/Iterators/Consumers/Monadic/Loop.lean b/src/Init/Data/Iterators/Consumers/Monadic/Loop.lean index dd36749558..6cc1564a27 100644 --- a/src/Init/Data/Iterators/Consumers/Monadic/Loop.lean +++ b/src/Init/Data/Iterators/Consumers/Monadic/Loop.lean @@ -159,7 +159,7 @@ This is the default implementation of the `IteratorLoop` class. It simply iterates through the iterator using `IterM.step`. For certain iterators, more efficient implementations are possible and should be used instead. -/ -@[always_inline, inline, expose] +@[always_inline, inline, expose, implicit_reducible] def IteratorLoop.defaultImplementation {α : Type w} {m : Type w → Type w'} {n : Type x → Type x'} [Monad n] [Iterator α m β] : IteratorLoop α m n where @@ -211,7 +211,7 @@ theorem IteratorLoop.wellFounded_of_productive {α β : Type w} {m : Type w → /-- This `ForIn'`-style loop construct traverses a finite iterator using an `IteratorLoop` instance. -/ -@[always_inline, inline] +@[always_inline, inline, expose, implicit_reducible] def IteratorLoop.finiteForIn' {m : Type w → Type w'} {n : Type x → Type x'} {α : Type w} {β : Type w} [Iterator α m β] [IteratorLoop α m n] [Monad n] (lift : ∀ γ δ, (γ → n δ) → m γ → n δ) : @@ -224,7 +224,7 @@ A `ForIn'` instance for iterators. Its generic membership relation is not easy t so this is not marked as `instance`. This way, more convenient instances can be built on top of it or future library improvements will make it more comfortable. -/ -@[always_inline, inline] +@[always_inline, inline, expose, implicit_reducible] def IterM.instForIn' {m : Type w → Type w'} {n : Type w → Type w''} {α : Type w} {β : Type w} [Iterator α m β] [IteratorLoop α m n] [Monad n] [MonadLiftT m n] : @@ -239,7 +239,7 @@ instance IterM.instForInOfIteratorLoop {m : Type w → Type w'} {n : Type w → instForInOfForIn' /-- Internal implementation detail of the iterator library. -/ -@[always_inline, inline] +@[always_inline, inline, expose, implicit_reducible] def IterM.Partial.instForIn' {m : Type w → Type w'} {n : Type w → Type w''} {α : Type w} {β : Type w} [Iterator α m β] [IteratorLoop α m n] [MonadLiftT m n] [Monad n] : ForIn' n (IterM.Partial (α := α) m β) β ⟨fun it out => it.it.IsPlausibleIndirectOutput out⟩ where @@ -247,7 +247,7 @@ def IterM.Partial.instForIn' {m : Type w → Type w'} {n : Type w → Type w''} haveI := @IterM.instForIn'; forIn' it.it init f /-- Internal implementation detail of the iterator library. -/ -@[always_inline, inline] +@[always_inline, inline, expose, implicit_reducible] def IterM.Total.instForIn' {m : Type w → Type w'} {n : Type w → Type w''} {α : Type w} {β : Type w} [Iterator α m β] [IteratorLoop α m n] [MonadLiftT m n] [Monad n] [Finite α m] : diff --git a/src/Init/Data/Iterators/Internal/LawfulMonadLiftFunction.lean b/src/Init/Data/Iterators/Internal/LawfulMonadLiftFunction.lean index 7bdc8f04e1..f60c104c18 100644 --- a/src/Init/Data/Iterators/Internal/LawfulMonadLiftFunction.lean +++ b/src/Init/Data/Iterators/Internal/LawfulMonadLiftFunction.lean @@ -70,7 +70,7 @@ theorem LawfulMonadLiftFunction.lift_seqRight [LawfulMonad m] [LawfulMonad n] abbrev idToMonad [Monad m] ⦃α : Type u⦄ (x : Id α) : m α := pure x.run -def LawfulMonadLiftFunction.idToMonad [Monad m] [LawfulMonad m] : +theorem LawfulMonadLiftFunction.idToMonad [LawfulMonad m] : LawfulMonadLiftFunction (m := Id) (n := m) idToMonad where lift_pure := by simp [Internal.idToMonad] lift_bind := by simp [Internal.idToMonad] @@ -95,7 +95,7 @@ instance [LawfulMonadLiftBindFunction (n := n) (fun _ _ f x => lift x >>= f)] [L simpa using LawfulMonadLiftBindFunction.liftBind_bind (n := n) (liftBind := fun _ _ f x => lift x >>= f) (β := β) (γ := γ) (δ := γ) pure x g -def LawfulMonadLiftBindFunction.id [Monad m] [LawfulMonad m] : +theorem LawfulMonadLiftBindFunction.id [LawfulMonad m] : LawfulMonadLiftBindFunction (m := Id) (n := m) (fun _ _ f x => f x.run) where liftBind_pure := by simp liftBind_bind := by simp diff --git a/src/Init/Data/Iterators/Lemmas/Consumers/Loop.lean b/src/Init/Data/Iterators/Lemmas/Consumers/Loop.lean index c89d4e99ae..f776f4d5e3 100644 --- a/src/Init/Data/Iterators/Lemmas/Consumers/Loop.lean +++ b/src/Init/Data/Iterators/Lemmas/Consumers/Loop.lean @@ -32,7 +32,7 @@ theorem Iter.forIn'_eq {α β : Type w} [Iterator α Id β] [Finite α Id] IterM.DefaultConsumers.forIn' (n := m) (fun _ _ f x => f x.run) γ (fun _ _ _ => True) it.toIterM init _ (fun _ => id) (fun out h acc => return ⟨← f out (Iter.isPlausibleIndirectOutput_iff_isPlausibleIndirectOutput_toIterM.mpr h) acc, trivial⟩) := by - simp +instances only [instForIn', ForIn'.forIn', IteratorLoop.finiteForIn'] + simp +instances only [ForIn'.forIn'] have : ∀ a b c, f a b c = (Subtype.val <$> (⟨·, trivial⟩) <$> f a b c) := by simp simp +singlePass only [this] rw [hl.lawful (fun _ _ f x => f x.run) (wf := IteratorLoop.wellFounded_of_finite)] @@ -81,7 +81,7 @@ theorem Iter.forIn'_eq_forIn'_toIterM {α β : Type w} [Iterator α Id β] letI : ForIn' m (IterM (α := α) Id β) β _ := IterM.instForIn' ForIn'.forIn' it.toIterM init (fun out h acc => f out (isPlausibleIndirectOutput_iff_isPlausibleIndirectOutput_toIterM.mpr h) acc) := by - simp +instances [ForIn'.forIn', Iter.instForIn', IterM.instForIn', monadLift] + simp +instances [ForIn'.forIn', monadLift] theorem Iter.forIn_eq_forIn_toIterM {α β : Type w} [Iterator α Id β] [Finite α Id] {m : Type w → Type w''} [Monad m] [LawfulMonad m] diff --git a/src/Init/Data/Iterators/Lemmas/Consumers/Monadic/Loop.lean b/src/Init/Data/Iterators/Lemmas/Consumers/Monadic/Loop.lean index 984a77cfff..e23e717779 100644 --- a/src/Init/Data/Iterators/Lemmas/Consumers/Monadic/Loop.lean +++ b/src/Init/Data/Iterators/Lemmas/Consumers/Monadic/Loop.lean @@ -109,7 +109,7 @@ theorem IterM.forIn'_eq {α β : Type w} {m : Type w → Type w'} [Iterator α m letI : ForIn' n (IterM (α := α) m β) β _ := IterM.instForIn' ForIn'.forIn' (α := β) (m := n) it init f = IterM.DefaultConsumers.forIn' (n := n) (fun _ _ f x => monadLift x >>= f) γ (fun _ _ _ => True) it init _ (fun _ => id) (return ⟨← f · · ·, trivial⟩) := by - simp +instances only [instForIn', ForIn'.forIn', IteratorLoop.finiteForIn'] + simp +instances only [ForIn'.forIn'] have : f = (Subtype.val <$> (⟨·, trivial⟩) <$> f · · ·) := by simp rw [this, hl.lawful (fun _ _ f x => monadLift x >>= f) (wf := IteratorLoop.wellFounded_of_finite)] simp +instances [IteratorLoop.defaultImplementation] diff --git a/src/Init/Data/Iterators/ToIterator.lean b/src/Init/Data/Iterators/ToIterator.lean index a365afe497..df49741d3a 100644 --- a/src/Init/Data/Iterators/ToIterator.lean +++ b/src/Init/Data/Iterators/ToIterator.lean @@ -32,14 +32,14 @@ def ToIterator.iter [ToIterator γ Id α β] (x : γ) : Iter (α := α) β := ToIterator.iterM x |>.toIter /-- Creates a monadic `ToIterator` instance. -/ -@[always_inline, inline, expose, instance_reducible] +@[always_inline, inline, expose, implicit_reducible] def ToIterator.ofM (α : Type w) (iterM : γ → IterM (α := α) m β) : ToIterator γ m α β where iterMInternal x := iterM x /-- Creates a pure `ToIterator` instance. -/ -@[always_inline, inline, expose, instance_reducible] +@[always_inline, inline, expose, implicit_reducible] def ToIterator.of (α : Type w) (iter : γ → Iter (α := α) β) : ToIterator γ Id α β where diff --git a/src/Init/Data/Order/Factories.lean b/src/Init/Data/Order/Factories.lean index cbfcba3e1f..c9edc2cb41 100644 --- a/src/Init/Data/Order/Factories.lean +++ b/src/Init/Data/Order/Factories.lean @@ -147,7 +147,7 @@ public theorem LawfulOrderMin.of_min_le {α : Type u} [Min α] [LE α] This lemma characterizes in terms of `LE α` when a `Max α` instance "behaves like a supremum operator". -/ -public def LawfulOrderSup.of_le {α : Type u} [Max α] [LE α] +public theorem LawfulOrderSup.of_le {α : Type u} [Max α] [LE α] (max_le_iff : ∀ a b c : α, max a b ≤ c ↔ a ≤ c ∧ b ≤ c) : LawfulOrderSup α where max_le_iff := max_le_iff @@ -159,7 +159,7 @@ instances. The produced instance entails `LawfulOrderSup α` and `MaxEqOr α`. -/ -public def LawfulOrderMax.of_max_le_iff {α : Type u} [Max α] [LE α] +public theorem LawfulOrderMax.of_max_le_iff {α : Type u} [Max α] [LE α] (max_le_iff : ∀ a b c : α, max a b ≤ c ↔ a ≤ c ∧ b ≤ c := by exact LawfulOrderInf.le_min_iff) (max_eq_or : ∀ a b : α, max a b = a ∨ max a b = b := by exact MaxEqOr.max_eq_or) : LawfulOrderMax α where @@ -196,7 +196,7 @@ Creates a *total* `LE α` instance from an `LT α` instance. This only makes sense for asymmetric `LT α` instances (see `Std.Asymm`). -/ -@[inline] +@[inline, implicit_reducible, expose] public def _root_.LE.ofLT (α : Type u) [LT α] : LE α where le a b := ¬ b < a @@ -276,7 +276,7 @@ public theorem LawfulOrderMin.of_lt {α : Type u} [Min α] [LT α] This lemma characterizes in terms of `LT α` when a `Max α` instance "behaves like an supremum operator" with respect to `LE.ofLT α`. -/ -public def LawfulOrderSup.of_lt {α : Type u} [Max α] [LT α] +public theorem LawfulOrderSup.of_lt {α : Type u} [Max α] [LT α] (lt_max_iff : ∀ a b c : α, c < max a b ↔ c < a ∨ c < b) : haveI := LE.ofLT α LawfulOrderSup α := @@ -293,7 +293,7 @@ Derives a `LawfulOrderMax α` instance for `LE.ofLT` from two properties involvi The produced instance entails `LawfulOrderSup α` and `MaxEqOr α`. -/ -public def LawfulOrderMax.of_lt {α : Type u} [Max α] [LT α] +public theorem LawfulOrderMax.of_lt {α : Type u} [Max α] [LT α] (lt_max_iff : ∀ a b c : α, c < max a b ↔ c < a ∨ c < b) (max_eq_or : ∀ a b : α, max a b = a ∨ max a b = b) : haveI := LE.ofLT α diff --git a/src/Init/Data/Order/FactoriesExtra.lean b/src/Init/Data/Order/FactoriesExtra.lean index cbce850566..cd1aa38bef 100644 --- a/src/Init/Data/Order/FactoriesExtra.lean +++ b/src/Init/Data/Order/FactoriesExtra.lean @@ -26,7 +26,7 @@ public def _root_.LE.ofOrd (α : Type u) [Ord α] : LE α where /-- Creates an `DecidableLE α` instance using a well-behaved `Ord α` instance. -/ -@[inline, expose] +@[inline, expose, implicit_reducible] public def _root_.DecidableLE.ofOrd (α : Type u) [LE α] [Ord α] [LawfulOrderOrd α] : DecidableLE α := fun a b => match h : (compare a b).isLE with @@ -93,7 +93,7 @@ grind_pattern compare_ne_eq => compare a b, Ordering.eq where /-- Creates a `DecidableLT α` instance using a well-behaved `Ord α` instance. -/ -@[inline, expose] +@[inline, expose, implicit_reducible] public def _root_.DecidableLT.ofOrd (α : Type u) [LE α] [LT α] [Ord α] [LawfulOrderOrd α] [LawfulOrderLT α] : DecidableLT α := diff --git a/src/Init/Data/Order/Opposite.lean b/src/Init/Data/Order/Opposite.lean index b202947e49..341aca53b4 100644 --- a/src/Init/Data/Order/Opposite.lean +++ b/src/Init/Data/Order/Opposite.lean @@ -52,7 +52,8 @@ def max' [LE α] [DecidableLE α] (a b : α) : α := Without the `open scoped` command, Lean would not find the required {lit}`DecidableLE α` instance for the opposite order. -/ -@[implicit_reducible] def LE.opposite (le : LE α) : LE α where +@[implicit_reducible] +def LE.opposite (le : LE α) : LE α where le a b := b ≤ a theorem LE.opposite_def {le : LE α} : @@ -89,6 +90,7 @@ example [LE α] [LT α] [Std.LawfulOrderLT α] [Std.IsLinearOrder α] {x y : α} Without the `open scoped` command, Lean would not find the {lit}`LawfulOrderLT α` and {lit}`IsLinearOrder α` instances for the opposite order that are required by {name}`not_le`. -/ +@[implicit_reducible] def LT.opposite (lt : LT α) : LT α where lt a b := b < a @@ -125,6 +127,7 @@ example [LE α] [DecidableLE α] [Min α] [Std.LawfulOrderLeftLeaningMin α] {a Without the `open scoped` command, Lean would not find the {lit}`LawfulOrderLeftLeaningMax α` instance for the opposite order that is required by {name}`max_eq_if`. -/ +@[implicit_reducible] def Min.oppositeMax (min : Min α) : Max α where max a b := Min.min a b @@ -161,6 +164,7 @@ example [LE α] [DecidableLE α] [Max α] [Std.LawfulOrderLeftLeaningMax α] {a Without the `open scoped` command, Lean would not find the {lit}`LawfulOrderLeftLeaningMin α` instance for the opposite order that is required by {name}`min_eq_if`. -/ +@[implicit_reducible] def Max.oppositeMin (max : Max α) : Min α where min a b := Max.max a b diff --git a/src/Init/Data/Order/PackageFactories.lean b/src/Init/Data/Order/PackageFactories.lean index 5b7b6eb159..6551483c25 100644 --- a/src/Init/Data/Order/PackageFactories.lean +++ b/src/Init/Data/Order/PackageFactories.lean @@ -47,7 +47,7 @@ public instance instLawfulOrderBEqOfDecidableLE {α : Type u} [LE α] [Decidable beq_iff_le_and_ge := by simp [BEq.beq] /-- If `LT` can be characterized in terms of a decidable `LE`, then `LT` is decidable either. -/ -@[expose, instance_reducible] +@[inline, expose, implicit_reducible] public def decidableLTOfLE {α : Type u} [LE α] {_ : LT α} [DecidableLE α] [LawfulOrderLT α] : DecidableLT α := fun a b => @@ -171,7 +171,7 @@ automatically. If it fails, it is necessary to provide some of the fields manual * Other proof obligations, namely `le_refl` and `le_trans`, can be omitted if `Refl` and `Trans` instances can be synthesized. -/ -@[expose, implicit_reducible] +@[inline, expose, implicit_reducible] public def PreorderPackage.ofLE (α : Type u) (args : Packages.PreorderOfLEArgs α := by exact {}) : PreorderPackage α where toLE := args.le @@ -256,7 +256,7 @@ automatically. If it fails, it is necessary to provide some of the fields manual * Other proof obligations, namely `le_refl`, `le_trans` and `le_antisymm`, can be omitted if `Refl`, `Trans` and `Antisymm` instances can be synthesized. -/ -@[expose, implicit_reducible] +@[inline, expose, implicit_reducible] public def PartialOrderPackage.ofLE (α : Type u) (args : Packages.PartialOrderOfLEArgs α := by exact {}) : PartialOrderPackage α where toPreorderPackage := .ofLE α args.toPreorderOfLEArgs @@ -385,7 +385,7 @@ automatically. If it fails, it is necessary to provide some of the fields manual * Other proof obligations, namely `le_total` and `le_trans`, can be omitted if `Total` and `Trans` instances can be synthesized. -/ -@[expose, implicit_reducible] +@[inline, expose, implicit_reducible] public def LinearPreorderPackage.ofLE (α : Type u) (args : Packages.LinearPreorderOfLEArgs α := by exact {}) : LinearPreorderPackage α where toPreorderPackage := .ofLE α args.toPreorderOfLEArgs @@ -487,7 +487,7 @@ automatically. If it fails, it is necessary to provide some of the fields manual * Other proof obligations, namely `le_total`, `le_trans` and `le_antisymm`, can be omitted if `Total`, `Trans` and `Antisymm` instances can be synthesized. -/ -@[expose, implicit_reducible] +@[inline, expose, implicit_reducible] public def LinearOrderPackage.ofLE (α : Type u) (args : Packages.LinearOrderOfLEArgs α := by exact {}) : LinearOrderPackage α where toLinearPreorderPackage := .ofLE α args.toLinearPreorderOfLEArgs @@ -647,7 +647,7 @@ automatically. If it fails, it is necessary to provide some of the fields manual * Other proof obligations, for example `transOrd`, can be omitted if a matching instance can be synthesized. -/ -@[expose, instance_reducible] +@[inline, expose, implicit_reducible] public def LinearPreorderPackage.ofOrd (α : Type u) (args : Packages.LinearPreorderOfOrdArgs α := by exact {}) : LinearPreorderPackage α := letI := args.ord @@ -793,7 +793,7 @@ automatically. If it fails, it is necessary to provide some of the fields manual * Other proof obligations, such as `transOrd`, can be omitted if matching instances can be synthesized. -/ -@[expose, instance_reducible] +@[inline, expose, implicit_reducible] public def LinearOrderPackage.ofOrd (α : Type u) (args : Packages.LinearOrderOfOrdArgs α := by exact {}) : LinearOrderPackage α := -- set_option backward.isDefEq.respectTransparency false in diff --git a/src/Init/Data/Range/Polymorphic/RangeIterator.lean b/src/Init/Data/Range/Polymorphic/RangeIterator.lean index 4989c0da67..0069a56024 100644 --- a/src/Init/Data/Range/Polymorphic/RangeIterator.lean +++ b/src/Init/Data/Range/Polymorphic/RangeIterator.lean @@ -597,8 +597,7 @@ instance Iterator.instLawfulIteratorLoop [UpwardEnumerable α] [LE α] [Decidabl LawfulIteratorLoop (Rxc.Iterator α) Id n where lawful := by intro lift instLawfulMonadLiftFunction γ it init Pl wf f - simp +instances only [IteratorLoop.defaultImplementation, IteratorLoop.forIn, - IterM.DefaultConsumers.forIn'_eq_wf Pl wf] + simp +instances only [IteratorLoop.forIn, IterM.DefaultConsumers.forIn'_eq_wf Pl wf] rw [IterM.DefaultConsumers.forIn'.wf] split; rotate_left · simp only [IterM.step_eq, @@ -1173,8 +1172,7 @@ instance Iterator.instLawfulIteratorLoop [UpwardEnumerable α] [LT α] [Decidabl LawfulIteratorLoop (Rxo.Iterator α) Id n where lawful := by intro lift instLawfulMonadLiftFunction γ it init Pl wf f - simp +instances only [IteratorLoop.defaultImplementation, IteratorLoop.forIn, - IterM.DefaultConsumers.forIn'_eq_wf Pl wf] + simp +instances only [IteratorLoop.forIn, IterM.DefaultConsumers.forIn'_eq_wf Pl wf] rw [IterM.DefaultConsumers.forIn'.wf] split; rotate_left · simp [IterM.step_eq, Monadic.step, Internal.LawfulMonadLiftBindFunction.liftBind_pure (liftBind := lift)] @@ -1639,8 +1637,7 @@ instance Iterator.instLawfulIteratorLoop [UpwardEnumerable α] LawfulIteratorLoop (Rxi.Iterator α) Id n where lawful := by intro lift instLawfulMonadLiftFunction γ it init Pl wf f - simp +instances only [IteratorLoop.defaultImplementation, IteratorLoop.forIn, - IterM.DefaultConsumers.forIn'_eq_wf Pl wf] + simp +instances only [IteratorLoop.forIn, IterM.DefaultConsumers.forIn'_eq_wf Pl wf] rw [IterM.DefaultConsumers.forIn'.wf] split; rotate_left · simp [Monadic.step_eq_step, Monadic.step, Internal.LawfulMonadLiftBindFunction.liftBind_pure] diff --git a/src/Init/Data/Range/Polymorphic/UpwardEnumerable.lean b/src/Init/Data/Range/Polymorphic/UpwardEnumerable.lean index 4e86610496..9f6c937a42 100644 --- a/src/Init/Data/Range/Polymorphic/UpwardEnumerable.lean +++ b/src/Init/Data/Range/Polymorphic/UpwardEnumerable.lean @@ -438,6 +438,7 @@ protected theorem UpwardEnumerable.le_iff {α : Type u} [LE α] [UpwardEnumerabl [LawfulUpwardEnumerableLE α] {a b : α} : a ≤ b ↔ UpwardEnumerable.LE a b := LawfulUpwardEnumerableLE.le_iff a b +@[expose, implicit_reducible] def UpwardEnumerable.instLETransOfLawfulUpwardEnumerableLE {α : Type u} [LE α] [UpwardEnumerable α] [LawfulUpwardEnumerable α] [LawfulUpwardEnumerableLE α] : Trans (α := α) (· ≤ ·) (· ≤ ·) (· ≤ ·) where @@ -502,12 +503,13 @@ protected theorem UpwardEnumerable.lt_succ_iff {α : Type u} [UpwardEnumerable ← succMany?_eq_some_iff_succMany] at hn exact ⟨n, hn⟩ +@[expose, implicit_reducible] def UpwardEnumerable.instLTTransOfLawfulUpwardEnumerableLT {α : Type u} [LT α] [UpwardEnumerable α] [LawfulUpwardEnumerable α] [LawfulUpwardEnumerableLT α] : Trans (α := α) (· < ·) (· < ·) (· < ·) where trans := by simpa [UpwardEnumerable.lt_iff] using @UpwardEnumerable.lt_trans -def UpwardEnumerable.instLawfulOrderLTOfLawfulUpwardEnumerableLT {α : Type u} [LT α] [LE α] +theorem UpwardEnumerable.instLawfulOrderLTOfLawfulUpwardEnumerableLT {α : Type u} [LT α] [LE α] [UpwardEnumerable α] [LawfulUpwardEnumerable α] [LawfulUpwardEnumerableLT α] [LawfulUpwardEnumerableLE α] : LawfulOrderLT α where diff --git a/src/Lean/Elab/Deriving/TypeName.lean b/src/Lean/Elab/Deriving/TypeName.lean index 07c30e6448..e98863454a 100644 --- a/src/Lean/Elab/Deriving/TypeName.lean +++ b/src/Lean/Elab/Deriving/TypeName.lean @@ -19,11 +19,12 @@ private def deriveTypeNameInstance (declNames : Array Name) : CommandElabM Bool let cinfo ← getConstInfo declName unless cinfo.levelParams.isEmpty do throwError m!"{.ofConstName declName} has universe level parameters" - elabCommand <| ← withFreshMacroScope `( - unsafe def instImpl : TypeName @$(mkCIdent declName) := .mk _ $(quote declName) - @[implemented_by instImpl] opaque inst : TypeName @$(mkCIdent declName) - instance : TypeName @$(mkCIdent declName) := inst - ) + withScope (fun scope => { scope with opts := scope.opts.setBool `warn.classDefReducibility false }) do + elabCommand <| ← withFreshMacroScope `( + unsafe def instImpl : TypeName @$(mkCIdent declName) := .mk _ $(quote declName) + @[implemented_by instImpl] opaque inst : TypeName @$(mkCIdent declName) + instance : TypeName @$(mkCIdent declName) := inst + ) return true initialize diff --git a/src/Lean/Elab/MutualDef.lean b/src/Lean/Elab/MutualDef.lean index 0692f09a22..a61040ac94 100644 --- a/src/Lean/Elab/MutualDef.lean +++ b/src/Lean/Elab/MutualDef.lean @@ -1172,6 +1172,11 @@ private def checkAllDeclNamesDistinct (preDefs : Array PreDefinition) : TermElab structure AsyncBodyInfo where deriving TypeName +register_builtin_option warn.classDefReducibility : Bool := { + defValue := true + descr := "warn when a `def` of class type is not marked `@[reducible]` or `@[implicit_reducible]`" +} + register_builtin_option warn.exposeOnPrivate : Bool := { defValue := true descr := "warn about uses of `@[expose]` on private declarations" @@ -1213,9 +1218,11 @@ where -- Now that we have elaborated types, default data instances to `[implicit_reducible]`. This -- should happen before attribute application as `[instance]` will check for it. for header in headers do - if header.kind == .instance && !header.modifiers.anyAttr (·.name matches `reducible | `irreducible) then - if !(← isProp header.type) then - setReducibilityStatus header.declName .implicitReducible + -- TODO: remove `instance_reducible once the alias is deprecated + if !header.modifiers.anyAttr (·.name matches `reducible | `implicit_reducible | `instance_reducible | `irreducible) then + if header.kind == .instance then + if !(← isProp header.type) then + setReducibilityStatus header.declName .implicitReducible if let (#[view], #[declId]) := (views, expandedDeclIds) then if Elab.async.get (← getOptions) && view.kind.isTheorem && @@ -1225,6 +1232,18 @@ where elabAsync headers[0]! view declId else elabSync headers else elabSync headers + + -- Warn about class-typed `def`s that aren't marked with a reducibility attribute. + -- This check runs after elaboration so that attributes applied by other attributes + -- (e.g. `to_additive (attr := implicit_reducible)`) are accounted for. + for header in headers do + if header.kind == .def then + if warn.classDefReducibility.get (← getOptions) && + (← isClass? header.type).isSome /-TODO-/ && + !header.type.getForallBody.getAppFn.constName? matches ``Decidable | ``DecidableEq | ``Setoid then + let status ← getReducibilityStatus header.declName + unless status matches .reducible | .implicitReducible | .irreducible do + logWarning m!"Definition `{header.declName}` of class type must be marked with `@[reducible]` or `@[implicit_reducible]`" for view in views, declId in expandedDeclIds do -- NOTE: this should be the full `ref`, and thus needs to be done after any snapshotting -- that depends only on a part of the ref diff --git a/src/Std/Data/Iterators/Lemmas/Equivalence/HetT.lean b/src/Std/Data/Iterators/Lemmas/Equivalence/HetT.lean index dc6a978e33..de2ba5a6b2 100644 --- a/src/Std/Data/Iterators/Lemmas/Equivalence/HetT.lean +++ b/src/Std/Data/Iterators/Lemmas/Equivalence/HetT.lean @@ -28,6 +28,7 @@ class ComputableSmall (α : Type v) where class Small (α : Type v) : Prop where h : Nonempty (ComputableSmall.{u} α) +@[implicit_reducible] noncomputable def ComputableSmall.choose (α : Type v) [small : Small.{u} α] : ComputableSmall.{u} α := haveI : Nonempty (ComputableSmall.{u} α) := Small.h Classical.ofNonempty (α := ComputableSmall.{u} α) @@ -93,7 +94,7 @@ instance {α : Type v} {x : α} : Small.{u} (Subtype (· = x)) where inflate_deflate := by rintro ⟨_, rfl⟩; rfl }⟩ -def Small.of_surjective (α : Type v) {β : Type w} (f : α → β) [Small.{u} α] +theorem Small.of_surjective (α : Type v) {β : Type w} (f : α → β) [Small.{u} α] (h : ∀ b, ∃ a, f a = b) : Small.{u} β where h := ⟨{ Target := Quot (fun a a' : USquash α => f a.inflate = f a'.inflate) diff --git a/stage0/src/stdlib_flags.h b/stage0/src/stdlib_flags.h index 79a0e58edd..744657ae20 100644 --- a/stage0/src/stdlib_flags.h +++ b/stage0/src/stdlib_flags.h @@ -1,5 +1,7 @@ #include "util/options.h" +// Dear CI, please build stage 2 first + namespace lean { options get_default_options() { options opts; diff --git a/tests/elab/1158.lean b/tests/elab/1158.lean index 8ba0a3f12c..2bcf7b875f 100644 --- a/tests/elab/1158.lean +++ b/tests/elab/1158.lean @@ -1,3 +1,5 @@ +set_option warn.classDefReducibility false + class magma (α) where op : α → α → α infix:70 " ⋆ " => magma.op (self := inferInstance) diff --git a/tests/elab/1692.lean b/tests/elab/1692.lean index f8eaa2732e..8fae358a0c 100644 --- a/tests/elab/1692.lean +++ b/tests/elab/1692.lean @@ -1,5 +1,7 @@ import Lean.Hygiene +set_option warn.classDefReducibility false + def otherInhabited : Inhabited Nat := ⟨42⟩ def f := Id.run do diff --git a/tests/elab/2115.lean.out.expected b/tests/elab/2115.lean.out.expected index 05cae9321e..5d767ce090 100644 --- a/tests/elab/2115.lean.out.expected +++ b/tests/elab/2115.lean.out.expected @@ -1,8 +1,12 @@ +2115.lean:16:0-16:36: warning: Definition `foo` of class type must be marked with `@[reducible]` or `@[implicit_reducible]` def foo : {α : Type} → [D α] → A α := fun {α : Type} [inst : D α] => @inferInstance.{1} (A α) (@B.toA α (@D.toB α inst)) +2115.lean:21:0-21:36: warning: Definition `bla` of class type must be marked with `@[reducible]` or `@[implicit_reducible]` def bla : {α : Type} → [D α] → A α := fun {α : Type} [inst : D α] => @inferInstance.{1} (A α) (@C.toA α (@D.toC α inst)) +2115.lean:26:0-26:36: warning: Definition `boo` of class type must be marked with `@[reducible]` or `@[implicit_reducible]` def boo : {α : Type} → [D α] → A α := fun {α : Type} [inst : D α] => @inferInstance.{1} (A α) (@B.toA α (@D.toB α inst)) +2115.lean:31:0-31:37: warning: Definition `boo2` of class type must be marked with `@[reducible]` or `@[implicit_reducible]` def boo2 : {α : Type} → [D α] → A α := fun {α : Type} [inst : D α] => @inferInstance.{1} (A α) (@C.toA α (@D.toC α inst)) diff --git a/tests/elab/2461.lean b/tests/elab/2461.lean index bf1f08e8ab..67caf3506b 100644 --- a/tests/elab/2461.lean +++ b/tests/elab/2461.lean @@ -1,3 +1,5 @@ +set_option warn.classDefReducibility false + section algebra_hierarchy_classes_to_comm_ring class Semiring (α : Type) extends Add α, Mul α, Zero α, One α diff --git a/tests/elab/366.lean.out.expected b/tests/elab/366.lean.out.expected index 3e6d9425c7..055cf20fa2 100644 --- a/tests/elab/366.lean.out.expected +++ b/tests/elab/366.lean.out.expected @@ -1,3 +1,4 @@ +366.lean:1:0-2:72: warning: Definition `foo` of class type must be marked with `@[reducible]` or `@[implicit_reducible]` [Meta.synthInstance] ✅️ Inhabited Nat [Meta.synthInstance] new goal Inhabited Nat [Meta.synthInstance.instances] #[@instInhabitedOfMonad, instInhabitedNat] diff --git a/tests/elab/3965_2.lean b/tests/elab/3965_2.lean index ee0df78c25..4a4c495d12 100644 --- a/tests/elab/3965_2.lean +++ b/tests/elab/3965_2.lean @@ -1,3 +1,5 @@ +set_option warn.classDefReducibility false + section Mathlib.Init.Order.Defs universe u diff --git a/tests/elab/3965_2.lean.out.expected b/tests/elab/3965_2.lean.out.expected index 430a94c85b..d4010da443 100644 --- a/tests/elab/3965_2.lean.out.expected +++ b/tests/elab/3965_2.lean.out.expected @@ -1,14 +1,14 @@ -3965_2.lean:9:8-9:19: warning: declaration uses `sorry` -3965_2.lean:30:12-30:18: warning: declaration uses `sorry` -3965_2.lean:32:28-32:33: warning: declaration uses `sorry` -3965_2.lean:32:28-32:33: warning: declaration uses `sorry` -3965_2.lean:39:18-39:27: warning: declaration uses `sorry` +3965_2.lean:11:8-11:19: warning: declaration uses `sorry` +3965_2.lean:32:12-32:18: warning: declaration uses `sorry` +3965_2.lean:34:28-34:33: warning: declaration uses `sorry` +3965_2.lean:34:28-34:33: warning: declaration uses `sorry` 3965_2.lean:41:18-41:27: warning: declaration uses `sorry` -3965_2.lean:81:4-81:8: warning: declaration uses `sorry` -3965_2.lean:81:4-81:8: warning: declaration uses `sorry` -3965_2.lean:81:4-81:8: warning: declaration uses `sorry` -3965_2.lean:81:4-81:8: warning: declaration uses `sorry` -3965_2.lean:81:4-81:8: warning: declaration uses `sorry` -3965_2.lean:81:4-81:8: warning: declaration uses `sorry` -3965_2.lean:81:4-81:8: warning: declaration uses `sorry` -3965_2.lean:89:8-89:25: warning: declaration uses `sorry` +3965_2.lean:43:18-43:27: warning: declaration uses `sorry` +3965_2.lean:83:4-83:8: warning: declaration uses `sorry` +3965_2.lean:83:4-83:8: warning: declaration uses `sorry` +3965_2.lean:83:4-83:8: warning: declaration uses `sorry` +3965_2.lean:83:4-83:8: warning: declaration uses `sorry` +3965_2.lean:83:4-83:8: warning: declaration uses `sorry` +3965_2.lean:83:4-83:8: warning: declaration uses `sorry` +3965_2.lean:83:4-83:8: warning: declaration uses `sorry` +3965_2.lean:91:8-91:25: warning: declaration uses `sorry` diff --git a/tests/elab/3965_3.lean b/tests/elab/3965_3.lean index 67fc629219..b281a05832 100644 --- a/tests/elab/3965_3.lean +++ b/tests/elab/3965_3.lean @@ -1,3 +1,5 @@ +set_option warn.classDefReducibility false + section Mathlib.Init.Order.Defs universe u diff --git a/tests/elab/3965_3.lean.out.expected b/tests/elab/3965_3.lean.out.expected index 0090d9a2ca..381bedb779 100644 --- a/tests/elab/3965_3.lean.out.expected +++ b/tests/elab/3965_3.lean.out.expected @@ -1,30 +1,30 @@ -3965_3.lean:8:8-8:16: warning: declaration uses `sorry` -3965_3.lean:50:19-50:26: warning: @Sup.sup does not have a doc string -3965_3.lean:53:19-53:26: warning: @Inf.inf does not have a doc string -3965_3.lean:93:4-93:21: warning: declaration uses `sorry` -3965_3.lean:125:8-125:14: warning: declaration uses `sorry` -3965_3.lean:138:8-138:19: warning: declaration uses `sorry` -3965_3.lean:140:8-140:18: warning: declaration uses `sorry` -3965_3.lean:148:14-148:28: warning: declaration uses `sorry` -3965_3.lean:148:14-148:28: warning: declaration uses `sorry` -3965_3.lean:148:14-148:28: warning: declaration uses `sorry` -3965_3.lean:148:14-148:28: warning: declaration uses `sorry` -3965_3.lean:148:14-148:28: warning: declaration uses `sorry` -3965_3.lean:148:14-148:28: warning: declaration uses `sorry` -3965_3.lean:148:14-148:28: warning: declaration uses `sorry` -3965_3.lean:156:14-156:28: warning: declaration uses `sorry` -3965_3.lean:156:14-156:28: warning: declaration uses `sorry` -3965_3.lean:156:14-156:28: warning: declaration uses `sorry` -3965_3.lean:156:14-156:28: warning: declaration uses `sorry` -3965_3.lean:156:14-156:28: warning: declaration uses `sorry` -3965_3.lean:156:14-156:28: warning: declaration uses `sorry` -3965_3.lean:156:14-156:28: warning: declaration uses `sorry` -3965_3.lean:217:8-217:15: warning: declaration uses `sorry` -3965_3.lean:227:8-227:15: warning: declaration uses `sorry` -3965_3.lean:260:9-260:17: warning: declaration uses `sorry` +3965_3.lean:10:8-10:16: warning: declaration uses `sorry` +3965_3.lean:52:19-52:26: warning: @Sup.sup does not have a doc string +3965_3.lean:55:19-55:26: warning: @Inf.inf does not have a doc string +3965_3.lean:95:4-95:21: warning: declaration uses `sorry` +3965_3.lean:127:8-127:14: warning: declaration uses `sorry` +3965_3.lean:140:8-140:19: warning: declaration uses `sorry` +3965_3.lean:142:8-142:18: warning: declaration uses `sorry` +3965_3.lean:150:14-150:28: warning: declaration uses `sorry` +3965_3.lean:150:14-150:28: warning: declaration uses `sorry` +3965_3.lean:150:14-150:28: warning: declaration uses `sorry` +3965_3.lean:150:14-150:28: warning: declaration uses `sorry` +3965_3.lean:150:14-150:28: warning: declaration uses `sorry` +3965_3.lean:150:14-150:28: warning: declaration uses `sorry` +3965_3.lean:150:14-150:28: warning: declaration uses `sorry` +3965_3.lean:158:14-158:28: warning: declaration uses `sorry` +3965_3.lean:158:14-158:28: warning: declaration uses `sorry` +3965_3.lean:158:14-158:28: warning: declaration uses `sorry` +3965_3.lean:158:14-158:28: warning: declaration uses `sorry` +3965_3.lean:158:14-158:28: warning: declaration uses `sorry` +3965_3.lean:158:14-158:28: warning: declaration uses `sorry` +3965_3.lean:158:14-158:28: warning: declaration uses `sorry` +3965_3.lean:219:8-219:15: warning: declaration uses `sorry` +3965_3.lean:229:8-229:15: warning: declaration uses `sorry` 3965_3.lean:262:9-262:17: warning: declaration uses `sorry` -3965_3.lean:278:4-278:23: warning: declaration uses `sorry` -3965_3.lean:278:4-278:23: warning: declaration uses `sorry` -3965_3.lean:278:4-278:23: warning: declaration uses `sorry` -3965_3.lean:278:4-278:23: warning: declaration uses `sorry` -3965_3.lean:287:0-287:7: warning: declaration uses `sorry` +3965_3.lean:264:9-264:17: warning: declaration uses `sorry` +3965_3.lean:280:4-280:23: warning: declaration uses `sorry` +3965_3.lean:280:4-280:23: warning: declaration uses `sorry` +3965_3.lean:280:4-280:23: warning: declaration uses `sorry` +3965_3.lean:280:4-280:23: warning: declaration uses `sorry` +3965_3.lean:289:0-289:7: warning: declaration uses `sorry` diff --git a/tests/elab/4171.lean b/tests/elab/4171.lean index fba0b819c1..32b2effcd0 100644 --- a/tests/elab/4171.lean +++ b/tests/elab/4171.lean @@ -1,3 +1,5 @@ +set_option warn.classDefReducibility false + /-! This is a minimization of a problem in Mathlib where a simp lemma `foo` would not fire, but variants: diff --git a/tests/elab/4171.lean.out.expected b/tests/elab/4171.lean.out.expected index 0c49ad7c1e..97e7900d01 100644 --- a/tests/elab/4171.lean.out.expected +++ b/tests/elab/4171.lean.out.expected @@ -1,28 +1,28 @@ -4171.lean:201:9-201:25: warning: declaration uses `sorry` -4171.lean:201:9-201:25: warning: declaration uses `sorry` -4171.lean:201:9-201:25: warning: declaration uses `sorry` -4171.lean:295:9-295:26: warning: declaration uses `sorry` -4171.lean:295:9-295:26: warning: declaration uses `sorry` -4171.lean:348:8-348:20: warning: declaration uses `sorry` -4171.lean:352:8-352:20: warning: declaration uses `sorry` -4171.lean:379:9-379:27: warning: declaration uses `sorry` -4171.lean:418:7-418:14: warning: declaration uses `sorry` -4171.lean:422:4-422:19: warning: declaration uses `sorry` -4171.lean:460:4-460:12: warning: declaration uses `sorry` -4171.lean:485:4-485:11: warning: declaration uses `sorry` -4171.lean:485:4-485:11: warning: declaration uses `sorry` -4171.lean:484:2-484:6: warning: declaration uses `sorry` -4171.lean:505:0-505:8: warning: declaration uses `sorry` -4171.lean:505:0-505:8: warning: declaration uses `sorry` -4171.lean:513:8-513:11: warning: declaration uses `sorry` -4171.lean:516:8-516:15: warning: declaration uses `sorry` -4171.lean:519:8-519:17: warning: declaration uses `sorry` -4171.lean:534:9-534:26: warning: declaration uses `sorry` -4171.lean:534:9-534:26: warning: declaration uses `sorry` -4171.lean:533:2-533:6: warning: declaration uses `sorry` -4171.lean:563:9-563:20: warning: declaration uses `sorry` -4171.lean:599:0-599:8: warning: declaration uses `sorry` -4171.lean:599:0-599:8: warning: declaration uses `sorry` -4171.lean:606:15-606:18: warning: declaration uses `sorry` -4171.lean:618:4-618:27: warning: declaration uses `sorry` -4171.lean:659:4-659:12: warning: declaration uses `sorry` +4171.lean:203:9-203:25: warning: declaration uses `sorry` +4171.lean:203:9-203:25: warning: declaration uses `sorry` +4171.lean:203:9-203:25: warning: declaration uses `sorry` +4171.lean:297:9-297:26: warning: declaration uses `sorry` +4171.lean:297:9-297:26: warning: declaration uses `sorry` +4171.lean:350:8-350:20: warning: declaration uses `sorry` +4171.lean:354:8-354:20: warning: declaration uses `sorry` +4171.lean:381:9-381:27: warning: declaration uses `sorry` +4171.lean:420:7-420:14: warning: declaration uses `sorry` +4171.lean:424:4-424:19: warning: declaration uses `sorry` +4171.lean:462:4-462:12: warning: declaration uses `sorry` +4171.lean:487:4-487:11: warning: declaration uses `sorry` +4171.lean:487:4-487:11: warning: declaration uses `sorry` +4171.lean:486:2-486:6: warning: declaration uses `sorry` +4171.lean:507:0-507:8: warning: declaration uses `sorry` +4171.lean:507:0-507:8: warning: declaration uses `sorry` +4171.lean:515:8-515:11: warning: declaration uses `sorry` +4171.lean:518:8-518:15: warning: declaration uses `sorry` +4171.lean:521:8-521:17: warning: declaration uses `sorry` +4171.lean:536:9-536:26: warning: declaration uses `sorry` +4171.lean:536:9-536:26: warning: declaration uses `sorry` +4171.lean:535:2-535:6: warning: declaration uses `sorry` +4171.lean:565:9-565:20: warning: declaration uses `sorry` +4171.lean:601:0-601:8: warning: declaration uses `sorry` +4171.lean:601:0-601:8: warning: declaration uses `sorry` +4171.lean:608:15-608:18: warning: declaration uses `sorry` +4171.lean:620:4-620:27: warning: declaration uses `sorry` +4171.lean:661:4-661:12: warning: declaration uses `sorry` diff --git a/tests/elab/4203.lean b/tests/elab/4203.lean index d968b82d54..1d73b4d2c8 100644 --- a/tests/elab/4203.lean +++ b/tests/elab/4203.lean @@ -16,6 +16,8 @@ error: failed to synthesize instance of type class Fintype v Hint: Type class instance resolution failures can be inspected with the `set_option trace.Meta.synthInstance true` command. +--- +warning: Definition `MappishOrder` of class type must be marked with `@[reducible]` or `@[implicit_reducible]` -/ #guard_msgs in def MappishOrder [DecidableEq dIn] : Preorder diff --git a/tests/elab/5176.lean b/tests/elab/5176.lean index 231e6db4f9..7cd30534b0 100644 --- a/tests/elab/5176.lean +++ b/tests/elab/5176.lean @@ -1,3 +1,5 @@ +set_option warn.classDefReducibility false + class Foo where class Bar extends Foo where diff --git a/tests/elab/6123_cat_adjunction.lean b/tests/elab/6123_cat_adjunction.lean index eb6069d782..2997ffbf02 100644 --- a/tests/elab/6123_cat_adjunction.lean +++ b/tests/elab/6123_cat_adjunction.lean @@ -1,3 +1,5 @@ +set_option warn.classDefReducibility false + section Mathlib.CategoryTheory.ConcreteCategory.Bundled universe u v diff --git a/tests/elab/6123_cat_adjunction.lean.out.expected b/tests/elab/6123_cat_adjunction.lean.out.expected index 64dfdc3690..133bd2f629 100644 --- a/tests/elab/6123_cat_adjunction.lean.out.expected +++ b/tests/elab/6123_cat_adjunction.lean.out.expected @@ -1,33 +1,33 @@ -6123_cat_adjunction.lean:139:14-139:16: warning: declaration uses `sorry` -6123_cat_adjunction.lean:145:4-145:9: warning: declaration uses `sorry` -6123_cat_adjunction.lean:200:4-200:9: warning: declaration uses `sorry` -6123_cat_adjunction.lean:239:17-239:24: warning: declaration uses `sorry` -6123_cat_adjunction.lean:410:4-410:7: warning: declaration uses `sorry` -6123_cat_adjunction.lean:412:4-412:10: warning: declaration uses `sorry` -6123_cat_adjunction.lean:414:4-414:17: warning: declaration uses `sorry` -6123_cat_adjunction.lean:437:4-437:34: warning: declaration uses `sorry` -6123_cat_adjunction.lean:441:4-441:41: warning: declaration uses `sorry` -6123_cat_adjunction.lean:446:4-446:35: warning: declaration uses `sorry` -6123_cat_adjunction.lean:470:4-470:23: warning: declaration uses `sorry` -6123_cat_adjunction.lean:470:4-470:23: warning: declaration uses `sorry` -6123_cat_adjunction.lean:470:4-470:23: warning: declaration uses `sorry` -6123_cat_adjunction.lean:479:67-479:71: warning: This simp argument is unused: +6123_cat_adjunction.lean:141:14-141:16: warning: declaration uses `sorry` +6123_cat_adjunction.lean:147:4-147:9: warning: declaration uses `sorry` +6123_cat_adjunction.lean:202:4-202:9: warning: declaration uses `sorry` +6123_cat_adjunction.lean:241:17-241:24: warning: declaration uses `sorry` +6123_cat_adjunction.lean:412:4-412:7: warning: declaration uses `sorry` +6123_cat_adjunction.lean:414:4-414:10: warning: declaration uses `sorry` +6123_cat_adjunction.lean:416:4-416:17: warning: declaration uses `sorry` +6123_cat_adjunction.lean:439:4-439:34: warning: declaration uses `sorry` +6123_cat_adjunction.lean:443:4-443:41: warning: declaration uses `sorry` +6123_cat_adjunction.lean:448:4-448:35: warning: declaration uses `sorry` +6123_cat_adjunction.lean:472:4-472:23: warning: declaration uses `sorry` +6123_cat_adjunction.lean:472:4-472:23: warning: declaration uses `sorry` +6123_cat_adjunction.lean:472:4-472:23: warning: declaration uses `sorry` +6123_cat_adjunction.lean:481:67-481:71: warning: This simp argument is unused: of_α Hint: Omit it from the simp argument list. simp_all only [typeToCat_obj, Functor.id_obj, typeToCat_map, o̵f̵_̵α̵,̵ ̵id_eq] Note: This linter can be disabled with `set_option linter.unusedSimpArgs false` -6123_cat_adjunction.lean:479:73-479:78: warning: This simp argument is unused: +6123_cat_adjunction.lean:481:73-481:78: warning: This simp argument is unused: id_eq Hint: Omit it from the simp argument list. simp_all only [typeToCat_obj, Functor.id_obj, typeToCat_map, of_α,̵ ̵i̵d̵_̵e̵q̵] Note: This linter can be disabled with `set_option linter.unusedSimpArgs false` -6123_cat_adjunction.lean:486:4-486:35: warning: declaration uses `sorry` -6123_cat_adjunction.lean:486:4-486:35: warning: declaration uses `sorry` -6123_cat_adjunction.lean:494:45-494:49: warning: This simp argument is unused: +6123_cat_adjunction.lean:488:4-488:35: warning: declaration uses `sorry` +6123_cat_adjunction.lean:488:4-488:35: warning: declaration uses `sorry` +6123_cat_adjunction.lean:496:45-496:49: warning: This simp argument is unused: of_α Hint: Omit it from the simp argument list. @@ -35,7 +35,7 @@ Hint: Omit it from the simp argument list. Functor.comp_map, typeToCat_map, o̵f̵_̵α̵,̵ ̵id_eq] Note: This linter can be disabled with `set_option linter.unusedSimpArgs false` -6123_cat_adjunction.lean:494:51-494:56: warning: This simp argument is unused: +6123_cat_adjunction.lean:496:51-496:56: warning: This simp argument is unused: id_eq Hint: Omit it from the simp argument list. diff --git a/tests/elab/616.lean b/tests/elab/616.lean index ff3a8407bd..c77f996248 100644 --- a/tests/elab/616.lean +++ b/tests/elab/616.lean @@ -1,3 +1,5 @@ +set_option warn.classDefReducibility false + def bug : Monad (λ α : Type _ => α → Prop) where pure x := (.=x) bind s f y := ∃ x, s x ∧ f x y diff --git a/tests/elab/664.lean b/tests/elab/664.lean index 39951d3fb3..338cb75874 100644 --- a/tests/elab/664.lean +++ b/tests/elab/664.lean @@ -1,3 +1,5 @@ +set_option warn.classDefReducibility false + class A (α : Type _) where a : α → Unit instance : A Empty where a x := nomatch x diff --git a/tests/elab/796.lean b/tests/elab/796.lean index 1bb37bb9f0..fe4701d984 100644 --- a/tests/elab/796.lean +++ b/tests/elab/796.lean @@ -1,3 +1,5 @@ +set_option warn.classDefReducibility false + namespace Ex1 structure A class B (a : outParam A) (α : Sort u) diff --git a/tests/elab/9624.lean b/tests/elab/9624.lean index b1ee23ccb2..5232f19507 100644 --- a/tests/elab/9624.lean +++ b/tests/elab/9624.lean @@ -1,3 +1,5 @@ +set_option warn.classDefReducibility false + set_option warn.sorry false inductive T : Type u where diff --git a/tests/elab/KyleAlg.lean b/tests/elab/KyleAlg.lean index b6712c5a23..9c3b567f29 100644 --- a/tests/elab/KyleAlg.lean +++ b/tests/elab/KyleAlg.lean @@ -1,5 +1,7 @@ import Lean +set_option warn.classDefReducibility false + /- from core: class OfNat (α : Type u) (n : Nat) where ofNat : α diff --git a/tests/elab/aStructPerfIssue.lean b/tests/elab/aStructPerfIssue.lean index 3c8b45ffe4..1cc587472a 100644 --- a/tests/elab/aStructPerfIssue.lean +++ b/tests/elab/aStructPerfIssue.lean @@ -1,3 +1,5 @@ +set_option warn.classDefReducibility false + noncomputable section namespace MWE diff --git a/tests/elab/binop_binrel_perf_issue.lean b/tests/elab/binop_binrel_perf_issue.lean index 8e77254833..7b071ebc0a 100644 --- a/tests/elab/binop_binrel_perf_issue.lean +++ b/tests/elab/binop_binrel_perf_issue.lean @@ -1,3 +1,5 @@ +set_option warn.classDefReducibility false + /-! This is a minimization of an `isDefEq` timeout from Mathlib.Algebra.Module.Submodule.Localization, where it is reasonably fast with `set_option backward.isDefEq.lazyWhnfCore false`, diff --git a/tests/elab/binop_binrel_perf_issue.lean.out.expected b/tests/elab/binop_binrel_perf_issue.lean.out.expected index 6d075637e8..a062ea13dc 100644 --- a/tests/elab/binop_binrel_perf_issue.lean.out.expected +++ b/tests/elab/binop_binrel_perf_issue.lean.out.expected @@ -1,40 +1,40 @@ -binop_binrel_perf_issue.lean:314:14-314:26: warning: declaration uses `sorry` -binop_binrel_perf_issue.lean:314:14-314:26: warning: declaration uses `sorry` -binop_binrel_perf_issue.lean:320:14-320:26: warning: declaration uses `sorry` -binop_binrel_perf_issue.lean:337:14-337:26: warning: declaration uses `sorry` -binop_binrel_perf_issue.lean:343:14-343:26: warning: declaration uses `sorry` -binop_binrel_perf_issue.lean:343:14-343:26: warning: declaration uses `sorry` -binop_binrel_perf_issue.lean:364:14-364:22: warning: declaration uses `sorry` -binop_binrel_perf_issue.lean:383:9-383:25: warning: declaration uses `sorry` -binop_binrel_perf_issue.lean:386:9-386:25: warning: declaration uses `sorry` -binop_binrel_perf_issue.lean:386:9-386:25: warning: declaration uses `sorry` -binop_binrel_perf_issue.lean:402:9-402:21: warning: declaration uses `sorry` -binop_binrel_perf_issue.lean:418:27-418:30: warning: declaration uses `sorry` -binop_binrel_perf_issue.lean:427:27-427:30: warning: declaration uses `sorry` -binop_binrel_perf_issue.lean:481:9-481:12: warning: declaration uses `sorry` -binop_binrel_perf_issue.lean:484:9-484:13: warning: declaration uses `sorry` -binop_binrel_perf_issue.lean:491:9-491:14: warning: declaration uses `sorry` -binop_binrel_perf_issue.lean:499:26-499:39: warning: declaration uses `sorry` -binop_binrel_perf_issue.lean:499:26-499:39: warning: declaration uses `sorry` -binop_binrel_perf_issue.lean:503:26-503:37: warning: declaration uses `sorry` -binop_binrel_perf_issue.lean:503:26-503:37: warning: declaration uses `sorry` -binop_binrel_perf_issue.lean:503:26-503:37: warning: declaration uses `sorry` -binop_binrel_perf_issue.lean:566:9-566:15: warning: declaration uses `sorry` -binop_binrel_perf_issue.lean:577:4-577:8: warning: declaration uses `sorry` -binop_binrel_perf_issue.lean:587:9-587:37: warning: declaration uses `sorry` -binop_binrel_perf_issue.lean:591:9-591:21: warning: declaration uses `sorry` -binop_binrel_perf_issue.lean:596:9-596:18: warning: declaration uses `sorry` -binop_binrel_perf_issue.lean:596:9-596:18: warning: declaration uses `sorry` -binop_binrel_perf_issue.lean:596:9-596:18: warning: declaration uses `sorry` -binop_binrel_perf_issue.lean:605:9-605:15: warning: declaration uses `sorry` -binop_binrel_perf_issue.lean:608:9-608:15: warning: declaration uses `sorry` -binop_binrel_perf_issue.lean:611:9-611:37: warning: declaration uses `sorry` -binop_binrel_perf_issue.lean:615:9-615:17: warning: declaration uses `sorry` -binop_binrel_perf_issue.lean:615:9-615:17: warning: declaration uses `sorry` -binop_binrel_perf_issue.lean:615:9-615:17: warning: declaration uses `sorry` -binop_binrel_perf_issue.lean:666:4-666:12: warning: declaration uses `sorry` -binop_binrel_perf_issue.lean:837:9-837:17: warning: declaration uses `sorry` -binop_binrel_perf_issue.lean:851:0-851:8: warning: declaration uses `sorry` -binop_binrel_perf_issue.lean:853:23-853:32: warning: declaration uses `sorry` -binop_binrel_perf_issue.lean:872:18-872:37: warning: declaration uses `sorry` -binop_binrel_perf_issue.lean:912:9-912:16: warning: declaration uses `sorry` +binop_binrel_perf_issue.lean:316:14-316:26: warning: declaration uses `sorry` +binop_binrel_perf_issue.lean:316:14-316:26: warning: declaration uses `sorry` +binop_binrel_perf_issue.lean:322:14-322:26: warning: declaration uses `sorry` +binop_binrel_perf_issue.lean:339:14-339:26: warning: declaration uses `sorry` +binop_binrel_perf_issue.lean:345:14-345:26: warning: declaration uses `sorry` +binop_binrel_perf_issue.lean:345:14-345:26: warning: declaration uses `sorry` +binop_binrel_perf_issue.lean:366:14-366:22: warning: declaration uses `sorry` +binop_binrel_perf_issue.lean:385:9-385:25: warning: declaration uses `sorry` +binop_binrel_perf_issue.lean:388:9-388:25: warning: declaration uses `sorry` +binop_binrel_perf_issue.lean:388:9-388:25: warning: declaration uses `sorry` +binop_binrel_perf_issue.lean:404:9-404:21: warning: declaration uses `sorry` +binop_binrel_perf_issue.lean:420:27-420:30: warning: declaration uses `sorry` +binop_binrel_perf_issue.lean:429:27-429:30: warning: declaration uses `sorry` +binop_binrel_perf_issue.lean:483:9-483:12: warning: declaration uses `sorry` +binop_binrel_perf_issue.lean:486:9-486:13: warning: declaration uses `sorry` +binop_binrel_perf_issue.lean:493:9-493:14: warning: declaration uses `sorry` +binop_binrel_perf_issue.lean:501:26-501:39: warning: declaration uses `sorry` +binop_binrel_perf_issue.lean:501:26-501:39: warning: declaration uses `sorry` +binop_binrel_perf_issue.lean:505:26-505:37: warning: declaration uses `sorry` +binop_binrel_perf_issue.lean:505:26-505:37: warning: declaration uses `sorry` +binop_binrel_perf_issue.lean:505:26-505:37: warning: declaration uses `sorry` +binop_binrel_perf_issue.lean:568:9-568:15: warning: declaration uses `sorry` +binop_binrel_perf_issue.lean:579:4-579:8: warning: declaration uses `sorry` +binop_binrel_perf_issue.lean:589:9-589:37: warning: declaration uses `sorry` +binop_binrel_perf_issue.lean:593:9-593:21: warning: declaration uses `sorry` +binop_binrel_perf_issue.lean:598:9-598:18: warning: declaration uses `sorry` +binop_binrel_perf_issue.lean:598:9-598:18: warning: declaration uses `sorry` +binop_binrel_perf_issue.lean:598:9-598:18: warning: declaration uses `sorry` +binop_binrel_perf_issue.lean:607:9-607:15: warning: declaration uses `sorry` +binop_binrel_perf_issue.lean:610:9-610:15: warning: declaration uses `sorry` +binop_binrel_perf_issue.lean:613:9-613:37: warning: declaration uses `sorry` +binop_binrel_perf_issue.lean:617:9-617:17: warning: declaration uses `sorry` +binop_binrel_perf_issue.lean:617:9-617:17: warning: declaration uses `sorry` +binop_binrel_perf_issue.lean:617:9-617:17: warning: declaration uses `sorry` +binop_binrel_perf_issue.lean:668:4-668:12: warning: declaration uses `sorry` +binop_binrel_perf_issue.lean:839:9-839:17: warning: declaration uses `sorry` +binop_binrel_perf_issue.lean:853:0-853:8: warning: declaration uses `sorry` +binop_binrel_perf_issue.lean:855:23-855:32: warning: declaration uses `sorry` +binop_binrel_perf_issue.lean:874:18-874:37: warning: declaration uses `sorry` +binop_binrel_perf_issue.lean:914:9-914:16: warning: declaration uses `sorry` diff --git a/tests/elab/congrSimpMathlibIssue.lean b/tests/elab/congrSimpMathlibIssue.lean index dab087d3e6..62524870bf 100644 --- a/tests/elab/congrSimpMathlibIssue.lean +++ b/tests/elab/congrSimpMathlibIssue.lean @@ -1,5 +1,7 @@ import Lean.Elab.Term +set_option warn.classDefReducibility false + /-! # Turán's theorem -/ diff --git a/tests/elab/derivingBEq.lean b/tests/elab/derivingBEq.lean index 6528a760ea..904efc3cef 100644 --- a/tests/elab/derivingBEq.lean +++ b/tests/elab/derivingBEq.lean @@ -1,5 +1,7 @@ module +set_option warn.classDefReducibility false + set_option deriving.beq.linear_construction_threshold 1000 public section diff --git a/tests/elab/derivingBEqLinear.lean b/tests/elab/derivingBEqLinear.lean index c3bbd022f9..acbd004a7c 100644 --- a/tests/elab/derivingBEqLinear.lean +++ b/tests/elab/derivingBEqLinear.lean @@ -1,5 +1,7 @@ module +set_option warn.classDefReducibility false + set_option deriving.beq.linear_construction_threshold 0 public section diff --git a/tests/elab/derivingInhabited.lean b/tests/elab/derivingInhabited.lean index 672ed79b62..4e8f9eb4fe 100644 --- a/tests/elab/derivingInhabited.lean +++ b/tests/elab/derivingInhabited.lean @@ -1,5 +1,7 @@ module +set_option warn.classDefReducibility false + inductive Foo (α : Type u) (β : Type v) where | mk₁ : α → Foo α β | mk₂ : List β → Foo α β diff --git a/tests/elab/derivingNonempty.lean b/tests/elab/derivingNonempty.lean index b96a642bcc..99c762ecba 100644 --- a/tests/elab/derivingNonempty.lean +++ b/tests/elab/derivingNonempty.lean @@ -1,5 +1,7 @@ module +set_option warn.classDefReducibility false + inductive Foo (α : Type u) (β : Type v) where | mk₁ : α → Foo α β | mk₂ : List β → Foo α β diff --git a/tests/elab/grind_cat2.lean b/tests/elab/grind_cat2.lean index 49df86ec1f..be61bdc91f 100644 --- a/tests/elab/grind_cat2.lean +++ b/tests/elab/grind_cat2.lean @@ -1,4 +1,6 @@ module + +set_option warn.classDefReducibility false @[expose] public section -- import Lean.Meta.Tactic.Grind universe v v₁ v₂ v₃ u u₁ u₂ u₃ diff --git a/tests/elab/grind_cat2.lean.out.expected b/tests/elab/grind_cat2.lean.out.expected index 1f18c7753e..9bb4fceac1 100644 --- a/tests/elab/grind_cat2.lean.out.expected +++ b/tests/elab/grind_cat2.lean.out.expected @@ -1,2 +1,2 @@ -grind_cat2.lean:177:4-177:14: warning: declaration uses `sorry` -grind_cat2.lean:242:4-242:19: warning: declaration uses `sorry` +grind_cat2.lean:179:4-179:14: warning: declaration uses `sorry` +grind_cat2.lean:244:4-244:19: warning: declaration uses `sorry` diff --git a/tests/elab/grind_section_var.lean b/tests/elab/grind_section_var.lean index b878e41db8..3c3bcc474c 100644 --- a/tests/elab/grind_section_var.lean +++ b/tests/elab/grind_section_var.lean @@ -1,5 +1,7 @@ import Std.Do +set_option warn.classDefReducibility false + /- Section variables should not be included. -/ diff --git a/tests/elab/inductionTacticBug.lean b/tests/elab/inductionTacticBug.lean index 9455bc5cfd..96186e8024 100644 --- a/tests/elab/inductionTacticBug.lean +++ b/tests/elab/inductionTacticBug.lean @@ -1,3 +1,5 @@ +set_option warn.classDefReducibility false + def ex {α} : Subsingleton (Squash α) := Subsingleton.intro $ by intro a b induction a using Squash.ind diff --git a/tests/elab/instanceReducible.lean b/tests/elab/instanceReducible.lean index 1da9f6de09..89f58fe50e 100644 --- a/tests/elab/instanceReducible.lean +++ b/tests/elab/instanceReducible.lean @@ -2,6 +2,8 @@ module /-! Applying `[instance]` after the fact should check for appropriate reducibility. -/ +/-- warning: Definition `unexposed` of class type must be marked with `@[reducible]` or `@[implicit_reducible]` -/ +#guard_msgs in public def unexposed : Inhabited Nat := inferInstance /-- warning: instance `unexposed` must be marked with `@[expose]` -/ @@ -12,6 +14,8 @@ attribute [instance] unexposed #guard_msgs in attribute [local instance] unexposed +/-- warning: Definition `exposed` of class type must be marked with `@[reducible]` or `@[implicit_reducible]` -/ +#guard_msgs in @[expose] public def exposed : Inhabited Nat := inferInstance diff --git a/tests/elab/instanceUsingFalse.lean b/tests/elab/instanceUsingFalse.lean index fa963db8cd..b506a333d0 100644 --- a/tests/elab/instanceUsingFalse.lean +++ b/tests/elab/instanceUsingFalse.lean @@ -1,3 +1,5 @@ +set_option warn.classDefReducibility false + class WrappedNat (α : Type) where n : Nat diff --git a/tests/elab/methodSpecs.lean b/tests/elab/methodSpecs.lean index 2337f7d8cb..04eb3ef794 100644 --- a/tests/elab/methodSpecs.lean +++ b/tests/elab/methodSpecs.lean @@ -109,7 +109,11 @@ error: expected `aS` to be a type class instance, but its type `S` does not look #guard_msgs in @[method_specs] def aS : S := ⟨1⟩ @[class] inductive indClass where | mk -/-- error: `indClass` is not a structure -/ +/-- +error: `indClass` is not a structure +--- +warning: Definition `instIndClass` of class type must be marked with `@[reducible]` or `@[implicit_reducible]` +-/ #guard_msgs in @[method_specs] def instIndClass : indClass := .mk -- This used to fail until we eta-reduced the field values diff --git a/tests/elab/modAsClasses.lean b/tests/elab/modAsClasses.lean index b510192510..9abd2c70be 100644 --- a/tests/elab/modAsClasses.lean +++ b/tests/elab/modAsClasses.lean @@ -1,3 +1,5 @@ +set_option warn.classDefReducibility false + class MyMod := (a : Nat) diff --git a/tests/elab/newfrontend1.lean b/tests/elab/newfrontend1.lean index a0e08eb5da..287bfc9e08 100644 --- a/tests/elab/newfrontend1.lean +++ b/tests/elab/newfrontend1.lean @@ -1,3 +1,5 @@ +set_option warn.classDefReducibility false + def x := 1 #check x diff --git a/tests/elab/order.lean b/tests/elab/order.lean index b023428dae..1feca79185 100644 --- a/tests/elab/order.lean +++ b/tests/elab/order.lean @@ -1,6 +1,7 @@ - import Init.Data.Order.PackageFactories +set_option warn.classDefReducibility false + variable {α : Type u} opaque X : Type := Unit @@ -60,7 +61,7 @@ end X section -def packageWithoutSynthesizableInstances : Std.LinearOrderPackage X := .ofLE X { +@[implicit_reducible] def packageWithoutSynthesizableInstances : Std.LinearOrderPackage X := .ofLE X { le := X.instLE decidableLE := X.instDecidableLE } @@ -70,7 +71,7 @@ section attribute [local instance] X.LinearOrderPackage.packageOfLE -def packageWithoutSynthesizableInstances' : Std.LinearOrderPackage X := .ofLE X { +@[implicit_reducible] def packageWithoutSynthesizableInstances' : Std.LinearOrderPackage X := .ofLE X { le := X.instLE decidableLE := X.instDecidableLE } @@ -90,11 +91,11 @@ this✝ : LT α := inferInstance ⊢ ∀ (a b : α), a < b ↔ a ≤ b ∧ ¬b ≤ a -/ #guard_msgs in -def packageOfLEOfLT1 [LE α] [DecidableLE α] [LT α] : Std.PreorderPackage α := .ofLE α { +@[implicit_reducible] def packageOfLEOfLT1 [LE α] [DecidableLE α] [LT α] : Std.PreorderPackage α := .ofLE α { le_refl := sorry le_trans := sorry } -def packageOfLEOfLT2 [LE α] [DecidableLE α] [LT α] (h : ∀ a b : α, a < b ↔ a ≤ b ∧ ¬ b ≤ a) : +@[implicit_reducible] def packageOfLEOfLT2 [LE α] [DecidableLE α] [LT α] (h : ∀ a b : α, a < b ↔ a ≤ b ∧ ¬ b ≤ a) : Std.PreorderPackage α := .ofLE α { lt_iff := h le_refl := sorry @@ -113,7 +114,7 @@ opaque _root_.X.instTransOrd : haveI := X.instOrd; Std.TransOrd X := sorry #guard_msgs(error, drop warning) in opaque _root_.X.instLawfulEqOrd : haveI := X.instOrd; Std.LawfulEqOrd X := sorry -def packageWithoutSynthesizableInstances : Std.LinearOrderPackage X := .ofOrd X { +@[implicit_reducible] def packageWithoutSynthesizableInstances : Std.LinearOrderPackage X := .ofOrd X { ord := X.instOrd transOrd := X.instTransOrd eq_of_compare := by @@ -128,7 +129,7 @@ section WithSynthesizableInstances attribute [scoped instance] X.instOrd X.instTransOrd X.instLawfulEqOrd -def packageWithSynthesizableInstances : Std.LinearOrderPackage X := .ofOrd X +@[implicit_reducible] def packageWithSynthesizableInstances : Std.LinearOrderPackage X := .ofOrd X end WithSynthesizableInstances diff --git a/tests/elab/order.lean.out.expected b/tests/elab/order.lean.out.expected index da02c3a410..bda5b910ae 100644 --- a/tests/elab/order.lean.out.expected +++ b/tests/elab/order.lean.out.expected @@ -1,2 +1,2 @@ -order.lean:97:4-97:20: warning: declaration uses `sorry` -order.lean:97:4-97:20: warning: declaration uses `sorry` +order.lean:98:26-98:42: warning: declaration uses `sorry` +order.lean:98:26-98:42: warning: declaration uses `sorry` diff --git a/tests/elab/propagateExpectedType.lean b/tests/elab/propagateExpectedType.lean index 44b313e357..62c5236ef8 100644 --- a/tests/elab/propagateExpectedType.lean +++ b/tests/elab/propagateExpectedType.lean @@ -1,3 +1,5 @@ +set_option warn.classDefReducibility false + variable {α : Type _} (r : α → α → Prop) (π : α → α) inductive rel : α → α → Prop diff --git a/tests/elab/simproc_timeout.lean b/tests/elab/simproc_timeout.lean index beb8d456b8..9315e7e6a8 100644 --- a/tests/elab/simproc_timeout.lean +++ b/tests/elab/simproc_timeout.lean @@ -1,3 +1,5 @@ +set_option warn.classDefReducibility false + -- Minimisation of a timeout triggered by leanprover/lean4#3124 -- in Mathlib.Computability.PartrecCode diff --git a/tests/elab/simproc_timeout.lean.out.expected b/tests/elab/simproc_timeout.lean.out.expected index 311d23ff46..53e4127688 100644 --- a/tests/elab/simproc_timeout.lean.out.expected +++ b/tests/elab/simproc_timeout.lean.out.expected @@ -1,19 +1,19 @@ -simproc_timeout.lean:52:8-52:23: warning: declaration uses `sorry` -simproc_timeout.lean:69:4-69:19: warning: declaration uses `sorry` -simproc_timeout.lean:73:4-73:17: warning: declaration uses `sorry` -simproc_timeout.lean:77:4-77:11: warning: declaration uses `sorry` -simproc_timeout.lean:83:9-83:32: warning: declaration uses `sorry` -simproc_timeout.lean:98:9-98:31: warning: declaration uses `sorry` -simproc_timeout.lean:116:4-116:7: warning: declaration uses `sorry` -simproc_timeout.lean:147:9-147:30: warning: declaration uses `sorry` -simproc_timeout.lean:183:26-183:39: warning: declaration uses `sorry` -simproc_timeout.lean:185:9-185:15: warning: declaration uses `sorry` -simproc_timeout.lean:198:18-198:24: warning: declaration uses `sorry` -simproc_timeout.lean:200:8-200:12: warning: declaration uses `sorry` -simproc_timeout.lean:209:9-209:13: warning: declaration uses `sorry` -simproc_timeout.lean:220:8-220:11: warning: declaration uses `sorry` +simproc_timeout.lean:54:8-54:23: warning: declaration uses `sorry` +simproc_timeout.lean:71:4-71:19: warning: declaration uses `sorry` +simproc_timeout.lean:75:4-75:17: warning: declaration uses `sorry` +simproc_timeout.lean:79:4-79:11: warning: declaration uses `sorry` +simproc_timeout.lean:85:9-85:32: warning: declaration uses `sorry` +simproc_timeout.lean:100:9-100:31: warning: declaration uses `sorry` +simproc_timeout.lean:118:4-118:7: warning: declaration uses `sorry` +simproc_timeout.lean:149:9-149:30: warning: declaration uses `sorry` +simproc_timeout.lean:185:26-185:39: warning: declaration uses `sorry` +simproc_timeout.lean:187:9-187:15: warning: declaration uses `sorry` +simproc_timeout.lean:200:18-200:24: warning: declaration uses `sorry` +simproc_timeout.lean:202:8-202:12: warning: declaration uses `sorry` +simproc_timeout.lean:211:9-211:13: warning: declaration uses `sorry` simproc_timeout.lean:222:8-222:11: warning: declaration uses `sorry` -simproc_timeout.lean:235:8-235:21: warning: declaration uses `sorry` -simproc_timeout.lean:246:8-246:19: warning: declaration uses `sorry` -simproc_timeout.lean:273:9-273:13: warning: declaration uses `sorry` -simproc_timeout.lean:283:8-283:17: warning: declaration uses `sorry` +simproc_timeout.lean:224:8-224:11: warning: declaration uses `sorry` +simproc_timeout.lean:237:8-237:21: warning: declaration uses `sorry` +simproc_timeout.lean:248:8-248:19: warning: declaration uses `sorry` +simproc_timeout.lean:275:9-275:13: warning: declaration uses `sorry` +simproc_timeout.lean:285:8-285:17: warning: declaration uses `sorry` diff --git a/tests/elab/structInst2.lean b/tests/elab/structInst2.lean index 6ca44e746b..d962e6abcc 100644 --- a/tests/elab/structInst2.lean +++ b/tests/elab/structInst2.lean @@ -1,5 +1,7 @@ import Init.Control.Option +set_option warn.classDefReducibility false + universe u v diff --git a/tests/elab/structWithAlgTCSynth.lean b/tests/elab/structWithAlgTCSynth.lean index 1742700cb1..f788a8cc37 100644 --- a/tests/elab/structWithAlgTCSynth.lean +++ b/tests/elab/structWithAlgTCSynth.lean @@ -1,3 +1,5 @@ +set_option warn.classDefReducibility false + /-! # Testing for timeouts in typeclass synthesis diff --git a/tests/elab/structWithAlgTCSynth.lean.out.expected b/tests/elab/structWithAlgTCSynth.lean.out.expected index 900dda837d..71c9433efa 100644 --- a/tests/elab/structWithAlgTCSynth.lean.out.expected +++ b/tests/elab/structWithAlgTCSynth.lean.out.expected @@ -1,94 +1,94 @@ -structWithAlgTCSynth.lean:205:27-205:55: warning: declaration uses `sorry` -structWithAlgTCSynth.lean:205:27-205:55: warning: declaration uses `sorry` -structWithAlgTCSynth.lean:205:27-205:55: warning: declaration uses `sorry` -structWithAlgTCSynth.lean:290:27-290:63: warning: declaration uses `sorry` -structWithAlgTCSynth.lean:361:27-361:52: warning: declaration uses `sorry` -structWithAlgTCSynth.lean:373:27-373:64: warning: declaration uses `sorry` -structWithAlgTCSynth.lean:373:27-373:64: warning: declaration uses `sorry` -structWithAlgTCSynth.lean:373:27-373:64: warning: declaration uses `sorry` -structWithAlgTCSynth.lean:385:27-385:47: warning: declaration uses `sorry` -structWithAlgTCSynth.lean:385:27-385:47: warning: declaration uses `sorry` -structWithAlgTCSynth.lean:390:27-390:46: warning: declaration uses `sorry` -structWithAlgTCSynth.lean:390:27-390:46: warning: declaration uses `sorry` -structWithAlgTCSynth.lean:469:9-469:21: warning: declaration uses `sorry` -structWithAlgTCSynth.lean:474:9-474:25: warning: declaration uses `sorry` -structWithAlgTCSynth.lean:479:9-479:21: warning: declaration uses `sorry` -structWithAlgTCSynth.lean:479:9-479:21: warning: declaration uses `sorry` -structWithAlgTCSynth.lean:486:9-486:18: warning: declaration uses `sorry` -structWithAlgTCSynth.lean:486:9-486:18: warning: declaration uses `sorry` -structWithAlgTCSynth.lean:496:9-496:21: warning: declaration uses `sorry` -structWithAlgTCSynth.lean:496:9-496:21: warning: declaration uses `sorry` -structWithAlgTCSynth.lean:496:9-496:21: warning: declaration uses `sorry` -structWithAlgTCSynth.lean:496:9-496:21: warning: declaration uses `sorry` -structWithAlgTCSynth.lean:507:9-507:17: warning: declaration uses `sorry` -structWithAlgTCSynth.lean:598:4-598:10: warning: declaration uses `sorry` -structWithAlgTCSynth.lean:617:9-617:12: warning: declaration uses `sorry` -structWithAlgTCSynth.lean:622:9-622:21: warning: declaration uses `sorry` -structWithAlgTCSynth.lean:625:9-625:22: warning: declaration uses `sorry` -structWithAlgTCSynth.lean:625:9-625:22: warning: declaration uses `sorry` -structWithAlgTCSynth.lean:625:9-625:22: warning: declaration uses `sorry` -structWithAlgTCSynth.lean:625:9-625:22: warning: declaration uses `sorry` -structWithAlgTCSynth.lean:631:9-631:12: warning: declaration uses `sorry` -structWithAlgTCSynth.lean:634:9-634:12: warning: declaration uses `sorry` -structWithAlgTCSynth.lean:637:9-637:21: warning: declaration uses `sorry` -structWithAlgTCSynth.lean:640:9-640:21: warning: declaration uses `sorry` -structWithAlgTCSynth.lean:640:9-640:21: warning: declaration uses `sorry` -structWithAlgTCSynth.lean:664:9-664:22: warning: declaration uses `sorry` -structWithAlgTCSynth.lean:743:9-743:34: warning: declaration uses `sorry` -structWithAlgTCSynth.lean:743:9-743:34: warning: declaration uses `sorry` -structWithAlgTCSynth.lean:743:9-743:34: warning: declaration uses `sorry` -structWithAlgTCSynth.lean:743:9-743:34: warning: declaration uses `sorry` -structWithAlgTCSynth.lean:743:9-743:34: warning: declaration uses `sorry` -structWithAlgTCSynth.lean:743:9-743:34: warning: declaration uses `sorry` -structWithAlgTCSynth.lean:767:9-767:26: warning: declaration uses `sorry` -structWithAlgTCSynth.lean:774:9-774:25: warning: declaration uses `sorry` -structWithAlgTCSynth.lean:774:9-774:25: warning: declaration uses `sorry` -structWithAlgTCSynth.lean:794:9-794:30: warning: declaration uses `sorry` -structWithAlgTCSynth.lean:878:9-878:15: warning: declaration uses `sorry` -structWithAlgTCSynth.lean:881:9-881:15: warning: declaration uses `sorry` -structWithAlgTCSynth.lean:884:9-884:20: warning: declaration uses `sorry` -structWithAlgTCSynth.lean:884:9-884:20: warning: declaration uses `sorry` -structWithAlgTCSynth.lean:891:9-891:21: warning: declaration uses `sorry` -structWithAlgTCSynth.lean:891:9-891:21: warning: declaration uses `sorry` -structWithAlgTCSynth.lean:897:0-897:8: warning: declaration uses `sorry` -structWithAlgTCSynth.lean:900:9-900:15: warning: declaration uses `sorry` -structWithAlgTCSynth.lean:903:9-903:15: warning: declaration uses `sorry` -structWithAlgTCSynth.lean:906:9-906:17: warning: declaration uses `sorry` -structWithAlgTCSynth.lean:914:4-914:28: warning: declaration uses `sorry` -structWithAlgTCSynth.lean:947:9-947:18: warning: declaration uses `sorry` -structWithAlgTCSynth.lean:1049:0-1049:8: warning: declaration uses `sorry` -structWithAlgTCSynth.lean:1115:12-1115:15: warning: declaration uses `sorry` -structWithAlgTCSynth.lean:1115:12-1115:15: warning: declaration uses `sorry` -structWithAlgTCSynth.lean:1118:12-1118:15: warning: declaration uses `sorry` -structWithAlgTCSynth.lean:1118:12-1118:15: warning: declaration uses `sorry` -structWithAlgTCSynth.lean:1121:12-1121:15: warning: declaration uses `sorry` -structWithAlgTCSynth.lean:1124:12-1124:15: warning: declaration uses `sorry` -structWithAlgTCSynth.lean:1124:12-1124:15: warning: declaration uses `sorry` -structWithAlgTCSynth.lean:1128:12-1128:16: warning: declaration uses `sorry` -structWithAlgTCSynth.lean:1134:12-1134:16: warning: declaration uses `sorry` -structWithAlgTCSynth.lean:1161:9-1161:26: warning: declaration uses `sorry` -structWithAlgTCSynth.lean:1161:9-1161:26: warning: declaration uses `sorry` -structWithAlgTCSynth.lean:1161:9-1161:26: warning: declaration uses `sorry` -structWithAlgTCSynth.lean:1161:9-1161:26: warning: declaration uses `sorry` -structWithAlgTCSynth.lean:1161:9-1161:26: warning: declaration uses `sorry` -structWithAlgTCSynth.lean:1161:9-1161:26: warning: declaration uses `sorry` -structWithAlgTCSynth.lean:1161:9-1161:26: warning: declaration uses `sorry` -structWithAlgTCSynth.lean:1172:9-1172:27: warning: declaration uses `sorry` -structWithAlgTCSynth.lean:1172:9-1172:27: warning: declaration uses `sorry` -structWithAlgTCSynth.lean:1172:9-1172:27: warning: declaration uses `sorry` -structWithAlgTCSynth.lean:1172:9-1172:27: warning: declaration uses `sorry` -structWithAlgTCSynth.lean:1172:9-1172:27: warning: declaration uses `sorry` -structWithAlgTCSynth.lean:1172:9-1172:27: warning: declaration uses `sorry` -structWithAlgTCSynth.lean:1172:9-1172:27: warning: declaration uses `sorry` -structWithAlgTCSynth.lean:1182:9-1182:21: warning: declaration uses `sorry` -structWithAlgTCSynth.lean:1182:9-1182:21: warning: declaration uses `sorry` -structWithAlgTCSynth.lean:1182:9-1182:21: warning: declaration uses `sorry` -structWithAlgTCSynth.lean:1182:9-1182:21: warning: declaration uses `sorry` -structWithAlgTCSynth.lean:1190:9-1190:17: warning: declaration uses `sorry` -structWithAlgTCSynth.lean:1190:9-1190:17: warning: declaration uses `sorry` -structWithAlgTCSynth.lean:1190:9-1190:17: warning: declaration uses `sorry` -structWithAlgTCSynth.lean:1190:9-1190:17: warning: declaration uses `sorry` -structWithAlgTCSynth.lean:1190:9-1190:17: warning: declaration uses `sorry` -structWithAlgTCSynth.lean:1190:9-1190:17: warning: declaration uses `sorry` -structWithAlgTCSynth.lean:1201:9-1201:25: warning: declaration uses `sorry` -structWithAlgTCSynth.lean:1235:0-1235:8: warning: declaration uses `sorry` +structWithAlgTCSynth.lean:207:27-207:55: warning: declaration uses `sorry` +structWithAlgTCSynth.lean:207:27-207:55: warning: declaration uses `sorry` +structWithAlgTCSynth.lean:207:27-207:55: warning: declaration uses `sorry` +structWithAlgTCSynth.lean:292:27-292:63: warning: declaration uses `sorry` +structWithAlgTCSynth.lean:363:27-363:52: warning: declaration uses `sorry` +structWithAlgTCSynth.lean:375:27-375:64: warning: declaration uses `sorry` +structWithAlgTCSynth.lean:375:27-375:64: warning: declaration uses `sorry` +structWithAlgTCSynth.lean:375:27-375:64: warning: declaration uses `sorry` +structWithAlgTCSynth.lean:387:27-387:47: warning: declaration uses `sorry` +structWithAlgTCSynth.lean:387:27-387:47: warning: declaration uses `sorry` +structWithAlgTCSynth.lean:392:27-392:46: warning: declaration uses `sorry` +structWithAlgTCSynth.lean:392:27-392:46: warning: declaration uses `sorry` +structWithAlgTCSynth.lean:471:9-471:21: warning: declaration uses `sorry` +structWithAlgTCSynth.lean:476:9-476:25: warning: declaration uses `sorry` +structWithAlgTCSynth.lean:481:9-481:21: warning: declaration uses `sorry` +structWithAlgTCSynth.lean:481:9-481:21: warning: declaration uses `sorry` +structWithAlgTCSynth.lean:488:9-488:18: warning: declaration uses `sorry` +structWithAlgTCSynth.lean:488:9-488:18: warning: declaration uses `sorry` +structWithAlgTCSynth.lean:498:9-498:21: warning: declaration uses `sorry` +structWithAlgTCSynth.lean:498:9-498:21: warning: declaration uses `sorry` +structWithAlgTCSynth.lean:498:9-498:21: warning: declaration uses `sorry` +structWithAlgTCSynth.lean:498:9-498:21: warning: declaration uses `sorry` +structWithAlgTCSynth.lean:509:9-509:17: warning: declaration uses `sorry` +structWithAlgTCSynth.lean:600:4-600:10: warning: declaration uses `sorry` +structWithAlgTCSynth.lean:619:9-619:12: warning: declaration uses `sorry` +structWithAlgTCSynth.lean:624:9-624:21: warning: declaration uses `sorry` +structWithAlgTCSynth.lean:627:9-627:22: warning: declaration uses `sorry` +structWithAlgTCSynth.lean:627:9-627:22: warning: declaration uses `sorry` +structWithAlgTCSynth.lean:627:9-627:22: warning: declaration uses `sorry` +structWithAlgTCSynth.lean:627:9-627:22: warning: declaration uses `sorry` +structWithAlgTCSynth.lean:633:9-633:12: warning: declaration uses `sorry` +structWithAlgTCSynth.lean:636:9-636:12: warning: declaration uses `sorry` +structWithAlgTCSynth.lean:639:9-639:21: warning: declaration uses `sorry` +structWithAlgTCSynth.lean:642:9-642:21: warning: declaration uses `sorry` +structWithAlgTCSynth.lean:642:9-642:21: warning: declaration uses `sorry` +structWithAlgTCSynth.lean:666:9-666:22: warning: declaration uses `sorry` +structWithAlgTCSynth.lean:745:9-745:34: warning: declaration uses `sorry` +structWithAlgTCSynth.lean:745:9-745:34: warning: declaration uses `sorry` +structWithAlgTCSynth.lean:745:9-745:34: warning: declaration uses `sorry` +structWithAlgTCSynth.lean:745:9-745:34: warning: declaration uses `sorry` +structWithAlgTCSynth.lean:745:9-745:34: warning: declaration uses `sorry` +structWithAlgTCSynth.lean:745:9-745:34: warning: declaration uses `sorry` +structWithAlgTCSynth.lean:769:9-769:26: warning: declaration uses `sorry` +structWithAlgTCSynth.lean:776:9-776:25: warning: declaration uses `sorry` +structWithAlgTCSynth.lean:776:9-776:25: warning: declaration uses `sorry` +structWithAlgTCSynth.lean:796:9-796:30: warning: declaration uses `sorry` +structWithAlgTCSynth.lean:880:9-880:15: warning: declaration uses `sorry` +structWithAlgTCSynth.lean:883:9-883:15: warning: declaration uses `sorry` +structWithAlgTCSynth.lean:886:9-886:20: warning: declaration uses `sorry` +structWithAlgTCSynth.lean:886:9-886:20: warning: declaration uses `sorry` +structWithAlgTCSynth.lean:893:9-893:21: warning: declaration uses `sorry` +structWithAlgTCSynth.lean:893:9-893:21: warning: declaration uses `sorry` +structWithAlgTCSynth.lean:899:0-899:8: warning: declaration uses `sorry` +structWithAlgTCSynth.lean:902:9-902:15: warning: declaration uses `sorry` +structWithAlgTCSynth.lean:905:9-905:15: warning: declaration uses `sorry` +structWithAlgTCSynth.lean:908:9-908:17: warning: declaration uses `sorry` +structWithAlgTCSynth.lean:916:4-916:28: warning: declaration uses `sorry` +structWithAlgTCSynth.lean:949:9-949:18: warning: declaration uses `sorry` +structWithAlgTCSynth.lean:1051:0-1051:8: warning: declaration uses `sorry` +structWithAlgTCSynth.lean:1117:12-1117:15: warning: declaration uses `sorry` +structWithAlgTCSynth.lean:1117:12-1117:15: warning: declaration uses `sorry` +structWithAlgTCSynth.lean:1120:12-1120:15: warning: declaration uses `sorry` +structWithAlgTCSynth.lean:1120:12-1120:15: warning: declaration uses `sorry` +structWithAlgTCSynth.lean:1123:12-1123:15: warning: declaration uses `sorry` +structWithAlgTCSynth.lean:1126:12-1126:15: warning: declaration uses `sorry` +structWithAlgTCSynth.lean:1126:12-1126:15: warning: declaration uses `sorry` +structWithAlgTCSynth.lean:1130:12-1130:16: warning: declaration uses `sorry` +structWithAlgTCSynth.lean:1136:12-1136:16: warning: declaration uses `sorry` +structWithAlgTCSynth.lean:1163:9-1163:26: warning: declaration uses `sorry` +structWithAlgTCSynth.lean:1163:9-1163:26: warning: declaration uses `sorry` +structWithAlgTCSynth.lean:1163:9-1163:26: warning: declaration uses `sorry` +structWithAlgTCSynth.lean:1163:9-1163:26: warning: declaration uses `sorry` +structWithAlgTCSynth.lean:1163:9-1163:26: warning: declaration uses `sorry` +structWithAlgTCSynth.lean:1163:9-1163:26: warning: declaration uses `sorry` +structWithAlgTCSynth.lean:1163:9-1163:26: warning: declaration uses `sorry` +structWithAlgTCSynth.lean:1174:9-1174:27: warning: declaration uses `sorry` +structWithAlgTCSynth.lean:1174:9-1174:27: warning: declaration uses `sorry` +structWithAlgTCSynth.lean:1174:9-1174:27: warning: declaration uses `sorry` +structWithAlgTCSynth.lean:1174:9-1174:27: warning: declaration uses `sorry` +structWithAlgTCSynth.lean:1174:9-1174:27: warning: declaration uses `sorry` +structWithAlgTCSynth.lean:1174:9-1174:27: warning: declaration uses `sorry` +structWithAlgTCSynth.lean:1174:9-1174:27: warning: declaration uses `sorry` +structWithAlgTCSynth.lean:1184:9-1184:21: warning: declaration uses `sorry` +structWithAlgTCSynth.lean:1184:9-1184:21: warning: declaration uses `sorry` +structWithAlgTCSynth.lean:1184:9-1184:21: warning: declaration uses `sorry` +structWithAlgTCSynth.lean:1184:9-1184:21: warning: declaration uses `sorry` +structWithAlgTCSynth.lean:1192:9-1192:17: warning: declaration uses `sorry` +structWithAlgTCSynth.lean:1192:9-1192:17: warning: declaration uses `sorry` +structWithAlgTCSynth.lean:1192:9-1192:17: warning: declaration uses `sorry` +structWithAlgTCSynth.lean:1192:9-1192:17: warning: declaration uses `sorry` +structWithAlgTCSynth.lean:1192:9-1192:17: warning: declaration uses `sorry` +structWithAlgTCSynth.lean:1192:9-1192:17: warning: declaration uses `sorry` +structWithAlgTCSynth.lean:1203:9-1203:25: warning: declaration uses `sorry` +structWithAlgTCSynth.lean:1237:0-1237:8: warning: declaration uses `sorry` diff --git a/tests/elab/synthInstsIssue.lean b/tests/elab/synthInstsIssue.lean index b5da0b2d30..ac5965a6a7 100644 --- a/tests/elab/synthInstsIssue.lean +++ b/tests/elab/synthInstsIssue.lean @@ -1,3 +1,5 @@ +set_option warn.classDefReducibility false + /-! This is a minimization of an issue widely seen in Mathlib after https://github.com/leanprover/lean4/pull/2793. diff --git a/tests/elab/synthInstsIssue.lean.out.expected b/tests/elab/synthInstsIssue.lean.out.expected index d4f0a0e05c..cb6d208e44 100644 --- a/tests/elab/synthInstsIssue.lean.out.expected +++ b/tests/elab/synthInstsIssue.lean.out.expected @@ -1 +1 @@ -synthInstsIssue.lean:56:8-56:17: warning: declaration uses `sorry` +synthInstsIssue.lean:58:8-58:17: warning: declaration uses `sorry` diff --git a/tests/elab/typeclass_diamond.lean b/tests/elab/typeclass_diamond.lean index d83e81321f..21a4539261 100644 --- a/tests/elab/typeclass_diamond.lean +++ b/tests/elab/typeclass_diamond.lean @@ -1,3 +1,5 @@ +set_option warn.classDefReducibility false + class Top₁ (n : Nat) : Type := (u : Unit := ()) class Bot₁ (n : Nat) : Type := (u : Unit := ()) class Left₁ (n : Nat) : Type := (u : Unit := ()) diff --git a/tests/elab_fail/2273.lean.out.expected b/tests/elab_fail/2273.lean.out.expected index f9347a8f10..d52e9c1d8d 100644 --- a/tests/elab_fail/2273.lean.out.expected +++ b/tests/elab_fail/2273.lean.out.expected @@ -2,3 +2,4 @@ P 37 Hint: Type class instance resolution failures can be inspected with the `set_option trace.Meta.synthInstance true` command. +2273.lean:24:0-24:31: warning: Definition `instP` of class type must be marked with `@[reducible]` or `@[implicit_reducible]` diff --git a/tests/elab_fail/phashmap_inst_coherence.lean.out.expected b/tests/elab_fail/phashmap_inst_coherence.lean.out.expected index 55c4d79e7e..932cec424e 100644 --- a/tests/elab_fail/phashmap_inst_coherence.lean.out.expected +++ b/tests/elab_fail/phashmap_inst_coherence.lean.out.expected @@ -1,3 +1,4 @@ +phashmap_inst_coherence.lean:8:0-9:30: warning: Definition `natDiffHash` of class type must be marked with `@[reducible]` or `@[implicit_reducible]` phashmap_inst_coherence.lean:12:53-12:54: error: Application type mismatch: The argument m has type diff --git a/tests/elab_fail/scopedInstanceOutsideNamespace.lean.out.expected b/tests/elab_fail/scopedInstanceOutsideNamespace.lean.out.expected index bd8f6f24ef..fc0ec53040 100644 --- a/tests/elab_fail/scopedInstanceOutsideNamespace.lean.out.expected +++ b/tests/elab_fail/scopedInstanceOutsideNamespace.lean.out.expected @@ -4,3 +4,4 @@ scopedInstanceOutsideNamespace.lean:6:0-6:30: error: Scoped attributes must be u scopedInstanceOutsideNamespace.lean:6:0-6:30: error: invalid syntax node kind `«term_+__1»` scopedInstanceOutsideNamespace.lean:6:0-6:30: error: Scoped attributes must be used inside namespaces scopedInstanceOutsideNamespace.lean:8:2-8:17: error: Scoped attributes must be used inside namespaces +scopedInstanceOutsideNamespace.lean:8:0-10:38: warning: Definition `myInst` of class type must be marked with `@[reducible]` or `@[implicit_reducible]` diff --git a/tests/elab_fail/tcloop.lean.out.expected b/tests/elab_fail/tcloop.lean.out.expected index 4c522a2cf0..6e7b035a14 100644 --- a/tests/elab_fail/tcloop.lean.out.expected +++ b/tests/elab_fail/tcloop.lean.out.expected @@ -7,3 +7,4 @@ Note: Use `set_option synthInstance.maxHeartbeats ` to set the limit. Hint: Additional diagnostic information may be available using the `set_option diagnostics true` command. Hint: Additional diagnostic information may be available using the `set_option diagnostics true` command. +tcloop.lean:13:0-14:15: warning: Definition `f` of class type must be marked with `@[reducible]` or `@[implicit_reducible]` diff --git a/tests/lean/run/classDefReducibilityAfterAttr.lean b/tests/lean/run/classDefReducibilityAfterAttr.lean new file mode 100644 index 0000000000..cae67633c1 --- /dev/null +++ b/tests/lean/run/classDefReducibilityAfterAttr.lean @@ -0,0 +1,31 @@ +/-! +# Class-typed `def` reducibility warning checks actual status + +The `classDefReducibility` warning should check the actual reducibility status +after all attributes have been applied, not just syntactic modifiers. +This ensures attributes that set reducibility during `.afterCompilation` +(like Mathlib's `to_additive (attr := implicit_reducible)`) are respected. +-/ + +class Foo where + x : Nat + +/-! Warning should fire when no reducibility attribute is present. -/ +/-- warning: Definition `baz` of class type must be marked with `@[reducible]` or `@[implicit_reducible]` -/ +#guard_msgs in +def baz : Foo := ⟨42⟩ + +/-! No warning with direct `implicit_reducible`. -/ +#guard_msgs in +@[implicit_reducible] +def qux : Foo := ⟨42⟩ + +/-! No warning with `reducible`. -/ +#guard_msgs in +@[reducible] +def quux : Foo := ⟨42⟩ + +/-! No warning with `irreducible`. -/ +#guard_msgs in +@[irreducible] +def corge : Foo := ⟨42⟩ diff --git a/tests/pkg/module/Module/Imported.lean b/tests/pkg/module/Module/Imported.lean index 5baa85dcdb..7fa76ef58b 100644 --- a/tests/pkg/module/Module/Imported.lean +++ b/tests/pkg/module/Module/Imported.lean @@ -70,6 +70,8 @@ error: failed to synthesize instance of type class X Hint: Type class instance resolution failures can be inspected with the `set_option trace.Meta.synthInstance true` command. +--- +warning: Definition `_private.Module.Imported.0.fX` of class type must be marked with `@[reducible]` or `@[implicit_reducible]` -/ #guard_msgs in def fX : X := inferInstance