defLemma and docBlame linters on local instances in sections

Stream: lean4

[Michael Stoll]

If I put a local instance into a section, then both the defLemma and the docBlame linter complain:

import Std.Tactic.Lint.Misc
import Std.Tactic.Lint.Frontend

/-- some class in Prop -/
class Foo (T : Type) (s t : T) : Prop where
  /-- some proof -/
  ht : s = t

section foo

local instance bar : Foo Nat 0 0 := ⟨rfl⟩

#lint
/-
-- Found 0 errors in 5 declarations (plus 4 automatically generated ones) in
the current file with 8 linters

-- All linting checks passed!
-/

end foo

#lint
/-
-- Found 2 errors in 1 declarations (plus 0 automatically generated ones) in
the current file with 14 linters

/- The `defLemma` linter reports:
INCORRECT DEF/LEMMA: -/
#check bar /- is a def, should be lemma/theorem -/

/- The `docBlame` linter reports:
DEFINITIONS ARE MISSING DOCUMENTATION STRINGS: -/
#check bar /- definition missing documentation string -/
-/

This occurs only when the #lint is outside the section with the local defs.

This looks like a bug to me.

[Michael Stoll]

Apparently, #lint uses more linters outside the section than within ?

[Mario Carneiro]

the issue is that some linters ignore instances, so local instances confuse them

[Mario Carneiro]

it's not really possible to tell whether something "was once" a local instance

[Michael Stoll]

So the only way to deal with this is to @[nolint defLemma docBlame] them?

[Mario Carneiro]

you may be able to at least fix the defLemma linter by making it a @[local instance] theorem

[Mario Carneiro]

you can also make it private (not sure if the relevant linters are looking for this)

[Michael Stoll]

Are private instances visible downstream (not by name, but for inferInstance etc.)?

[Mario Carneiro]

yes

[Mario Carneiro]

but private local instances are not

[Mario Carneiro]

but making the definition private will at least silence the docBlame linter

[Michael Stoll]

If I need to silence one of them anyway, I can as well silence both...

[Eric Wieser]

@[local instance] private theorem and @[local instance] private def seems like the best approach

[Mario Carneiro]

it would be nice if instance automatically did def/theorem properly though

[Mario Carneiro]

I'm pretty sure the only reason the defTheorem linter looks for instances is because this is a known bug in instance

[Kim Morrison]

Mario Carneiro said:

it would be nice if instance automatically did def/theorem properly though

Is there an issue for this? I couldn't find one.

[Mario Carneiro]

no, I think it was just a TODO / HACK in the linter code

[Jakob von Raumer]

This still hasn't been fixed :confused:

[Jakob von Raumer]

So the way forward here is to fix instance, not the linter, right?

[Eric Wieser]

I think there is an open PR that fixes instance