Documentation

Mathlib.Tactic.Linter.GlobalAttributeIn

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] HasForget.instFunLike in
instance (X Y : TopCat.{u}) : CoeFun (X ⟶ Y) fun _ => X → Y where
  coe f := f

Despite the in, this makes HasForget.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

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).

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
    Instances For

      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
        Instances For