Linter for attribute [...] in declarations

Linter for global attributes created via attribute [...] in declarations.

The syntax attribute [instance] instName in can be used to accidentally create a global instance. This is not obvious from reading the code, and in fact happened twice during the port, hence, we lint against it.

Example: before this was discovered, Mathlib/Topology/Category/TopCat/Basic.lean contained the following code:

attribute [instance] ConcreteCategory.instFunLike in
instance (X Y : TopCat.{u}) : CoeFun (X ⟶ Y) fun _ => X → Y where
  coe f := f

Despite the in, this makes ConcreteCategory.instFunLike a global instance.

This seems to apply to all attributes. For example:

theorem what : False := sorry

attribute [simp] what in
#guard true

-- the `simp` attribute persists
example : False := by simp  -- `simp` finds `what`

theorem who {x y : Nat} : x = y := sorry

attribute [ext] who in
#guard true

-- the `ext` attribute persists
example {x y : Nat} : x = y := by ext

Therefore, we lint against this pattern on all instances.

For removing attributes, the in works as expected.

/--
error: failed to synthesize
  Add Nat
-/
#guard_msgs in
attribute [-instance] instAddNat in
#synth Add Nat

-- the `instance` persists
/-- info: instAddNat -/
#guard_msgs in
#synth Add Nat

@[simp]
theorem what : False := sorry

/-- error: simp made no progress -/
#guard_msgs in
attribute [-simp] what in
example : False := by simp

-- the `simp` attribute persists
#guard_msgs in
example : False := by simp

opaque Mathlib.Linter.linter.globalAttributeIn : Lean.Option Bool

Lint on any occurrence of attribute [...] name in which is not local or scoped: these are a footgun, as the attribute is applied globally (despite the in).

def Mathlib.Linter.globalAttributeInLinter.getLinterGlobalAttributeIn (o : Lean.Options) : Bool

Gets the value of the linter.globalAttributeIn option.

Equations

• Mathlib.Linter.globalAttributeInLinter.getLinterGlobalAttributeIn o = Lean.Linter.getLinterValue Mathlib.Linter.linter.globalAttributeIn o

def Mathlib.Linter.globalAttributeInLinter.getGlobalAttributesIn? : Lean.Syntax → Option (Lean.Ident × Array (Lean.TSyntax `attr))

getGlobalAttributesIn? cmd assumes that cmd represents a attribute [...] id in ... command. If this is the case, then it returns (id, #[non-local nor scoped attributes]). Otherwise, it returns default.

Equations

• One or more equations did not get rendered due to their size.

def Mathlib.Linter.globalAttributeInLinter.globalAttributeIn : Lean.Linter

The globalAttributeInLinter linter flags any global attributes generated by an attribute [...] in declaration. (This includes the instance, simp and ext attributes.)

Despite the in, these define global instances, which can be rather misleading. Instead, remove the in or mark them with local.

Equations

• One or more equations did not get rendered due to their size.