docstring linter and where-definitions

Stream: mathlib4

[Joachim Breitner]

I regularly get bitten by a failing CI because I used a where clause to define a helper function, and then the docstring linter asks for a docstring for it.

My assumption is that where is “just” some macro that defines a top-level function (namespace-prefixed with the containing function name), and the docstring linter doesn't even know it came from a where, which explains the current behavior.

Is this behavior desirable, or should these definitions somehow be marked “internal” in some sense, and not require docstrings?

[Kyle Miller]

@Joachim Breitner I've complained about this too. The where clause is syntax sugar for let rec. I'd like the docstring linter to be able to know that these are auxiliary definitions and don't need docstrings. Maybe Lean could give default docstrings for let rec definitions ("This is an auxiliary definition generated by foo.")

[Joachim Breitner]

So a proper fix would be to have where or let rec annotate them somehow, and have the linter pick that annotation up?
The current linter code doesn’t look like it’s looking for anything we can use here… And the nolint attribute is defined in std4, while where is defined in lean, so that’d be an odd inversion of control.

And it’s not just the linter – wouldn’t you expect such local definitions to be hidden from the generated API documentation? So maybe it _is_ a more general concept.

How does this relate to the private modifier? Should where and let rec use the private modifier? Would this not solve the problem?

Let’s see: lean4#2717. Hmm, maybe not the best way.

Created a RFC at lean4#2719.

[Alex J. Best]

I have an alternative fix in mind which is for the doc-string linter to detect this type of "sub-declaration" (i.e. a declaration added to the environment as part of some larger def) using the declarationRanges and simply ignore them

[Joachim Breitner]

Using declarationRanges is clever, but sounds a bit hacky to me… I’d rather see an explicit flag added to the definition that indicates that this has been lifted out of its context by the elaborator.