chore: classify porting notes about #12096, missing instance_priority…

… lint
leanprover-community · Apr 12, 2024 · 88696fc · 88696fc
1 parent b0aea61
commit 88696fc
Show file tree

Hide file tree

Showing 4 changed files with 7 additions and 4 deletions.
diff --git a/Mathlib/Algebra/AddTorsor.lean b/Mathlib/Algebra/AddTorsor.lean
@@ -53,13 +53,15 @@ class AddTorsor (G : outParam (Type*)) (P : Type*) [outParam <| AddGroup G] exte
   vadd_vsub' : ∀ (g : G) (p : P), g +ᵥ p -ᵥ p = g
 #align add_torsor AddTorsor
 
-attribute [instance 100] AddTorsor.nonempty -- Porting note: removers `nolint instance_priority`
+ -- Porting note(#12096): removed `nolint instance_priority`; lint not ported yet
+attribute [instance 100] AddTorsor.nonempty
 
 -- Porting note: removed
 --attribute [nolint dangerous_instance] AddTorsor.toVSub
 
 /-- An `AddGroup G` is a torsor for itself. -/
---@[nolint instance_priority] Porting note: linter does not exist
+-- Porting note(#12096): linter not ported yet
+--@[nolint instance_priority]
 instance addGroupIsAddTorsor (G : Type*) [AddGroup G] : AddTorsor G G
     where
   vsub := Sub.sub

diff --git a/Mathlib/Algebra/Algebra/Tower.lean b/Mathlib/Algebra/Algebra/Tower.lean
@@ -177,7 +177,7 @@ instance (priority := 999) subsemiring (U : Subsemiring S) : IsScalarTower U S A
   of_algebraMap_eq fun _x => rfl
 #align is_scalar_tower.subsemiring IsScalarTower.subsemiring
 
--- Porting note: @[nolint instance_priority]
+-- Porting note(#12096): removed @[nolint instance_priority], linter not ported yet
 instance (priority := 999) of_algHom {R A B : Type*} [CommSemiring R] [CommSemiring A]
     [CommSemiring B] [Algebra R A] [Algebra R B] (f : A →ₐ[R] B) :
     @IsScalarTower R A B _ f.toRingHom.toAlgebra.toSMul _ :=

diff --git a/Mathlib/Data/Finite/Basic.lean b/Mathlib/Data/Finite/Basic.lean
@@ -57,7 +57,7 @@ instance (priority := 100) of_subsingleton {α : Sort*} [Subsingleton α] : Fini
 #align finite.of_subsingleton Finite.of_subsingleton
 
 -- Higher priority for `Prop`s
--- @[nolint instance_priority] -- Porting note: linter not found
+-- Porting note(#12096): removed @[nolint instance_priority], linter not ported yet
 instance prop (p : Prop) : Finite p :=
   Finite.of_subsingleton
 #align finite.prop Finite.prop

diff --git a/Mathlib/Geometry/Manifold/Algebra/LeftInvariantDerivation.lean b/Mathlib/Geometry/Manifold/Algebra/LeftInvariantDerivation.lean
@@ -31,6 +31,7 @@ variable {𝕜 : Type*} [NontriviallyNormedField 𝕜] {E : Type*} [NormedAddCom
   [TopologicalSpace G] [ChartedSpace H G] [Monoid G] [SmoothMul I G] (g h : G)
 
 -- Generate trivial has_sizeof instance. It prevents weird type class inference timeout problems
+-- Porting note(#12096): removed @[nolint instance_priority], linter not ported yet
 -- @[local nolint instance_priority, local instance 10000]
 -- private def disable_has_sizeof {α} : SizeOf α :=
 --   ⟨fun _ => 0⟩