rfc: linter.missingDocs for lakefile deps

Stream: lean4

[Alok Singh]

set_option linter.missingDocs true

/- Core utilities: arrays, data structures, and basic tactics. Provides efficient implementations without mathlib overhead -/
require batteries from git "https://github.com/leanprover-community/batteries" @ "main"

I've found the hover it provides handy for myself and AI. But though deps can take doc comments, the linter doesn't fire for them.

[Eric Wieser]

This seems backwards to me; the doc-comment should go on the package batteries declaration, such that hovering over it in your lakefile tells you how batteries describes itself

[Alok Singh]

That too, really id like the linter to just complain about any missing doc
comment opportunities. Even if they don’t hover yet they may in the future.

[Eric Wieser]

Where would you want the hover for the docstring above? I'd argue in your specific example this is almost harmful, because your documentation can easily diverge from what batteries actually is, since it lives outside batteries.

[Alok Singh]

Touché, I had forgotten they’d clash. But if I had it, maybe below the package’s own docstring.