strange docPrime linter behaviour

Stream: mathlib4

[Edward van de Meent]

what's going on in the following example?

import Mathlib

set_option autoImplicit false
set_option linter.docPrime true
/--
testing
-/
def Foo' := Nat

namespace Foo'

whatsnew in
-- commenting out the above line makes the linter ping the instance for no clear reason; the whatsnew command doesn't show any declaration with a name ending with a prime though
instance : Zero Foo' where
  zero := Nat.zero

def bar : Nat := 0

end Foo'

[Edward van de Meent]

i'm guessing the whatsnew in command somehow alters what declarations get made?

[Edward van de Meent]

i guess it might be beneficial if the linter error told us what declaration this is about? i'm a dumbass and cant read

[Edward van de Meent]

still, it is strange it does not recognise that Foo' already has a docstring?

[Edward van de Meent]

presumably @Damiano Testa

[David Renshaw]

In the above example, declId gets set to <missing>.

  let declId :=
    if stx[1].isOfKind ``Lean.Parser.Command.instance then
      stx[1][3][0]
    else
      stx[1][1]

https://github.com/leanprover-community/mathlib4/blob/9890d5ff187e6a1625705cce1f16623a755a22db/Mathlib/Tactic/Linter/DocPrime.lean#L50

[David Renshaw]

... which gets appended to the namespace Foo', to get a declName of Foo', which ends in a prime.

[David Renshaw]

I'm guessing this code was written without considering the possibility of an anonymous instance.

[Edward van de Meent]

so if i understand correctly, the linter only guesses the name of declarations, and triggers based off of that guess?

[David Renshaw]

I expect that adding a check for that would fix it.

[David Renshaw]

I agree that the way of extracting the declaration name from syntax seems not super reliable.

[David Renshaw]

I wonder if infotrees might provide a more reliable way.

[David Renshaw]

We could get the infotree via ← getInfoTrees and then get the declaration name via ContextInfo.parentDecl?.

[David Renshaw]

The same problem with example instead of instance:

example : True := .intro

[David Renshaw]

I'll prepare a PR with a fix for these cases.

[David Renshaw]

mathlib4#20027

[Damiano Testa]

#20027, just for the emoji bot's sake!

[Damiano Testa]

When I wrote the linter, there was not yet the utility to extract the "correct" name. Since figuring out the performance of that function is work in progress, the proposed fix looks good!

[Damiano Testa]

Oh, the bot picked up the earlier link to the PR as well: good to know!

[Edward van de Meent]

Damiano Testa said:

Oh, the bot picked up the earlier link to the PR as well: good to know!

right, the post contains #20027 and a link to the corresponding PR, is in a public channel and not in #rss ; therefore, it should find it.

[David Renshaw]

When I wrote the linter, there was not yet the utility to extract the "correct" name.

Is there such a utility now? Are infotrees the way to go?

[Damiano Testa]

There is docs#Mathlib.Linter.getNamesFrom which admittedly should get some extra filters: as is, it returns a lot of autogenerated names, with no option to sift out any "clearly unwanted" declaration.

[Damiano Testa]

It works by inspecting the DeclRange environment extension, rather than the InfoTrees. I suspect that the InfoTrees approach would also work (I experimented with them for a similar reason with the minImports command), but I suspect that it might be harder to make that more efficient.