Files with module docstrings in the wrong place

Stream: general

[Eric Wieser]

Searching for /-\nCopyright[^\n]*\n[^\n]*\nAuthor[^\n]*\n\n, I found over 100 files that seem to have their heading in the copyright comment instead of in a dedicated markdown comment (which then doesn't appear in the docs). Is this worth a lint-sprint, or automation?

[Eric Wieser]

I realized that #5222 was the tip of the iceberg

[Bryan Gin-ge Chen]

You should be able to find them in scripts/copy-mod-doc-exceptions.txt if you search for ERR_MOD.

[Bryan Gin-ge Chen]

I think at one point it was mentioned that instead of fixing them all at once with a script we should give ourselves a chance to write real module docstrings.

[Johan Commelin]

Right, if we fix them with a script, then we don't have ERR_MOD anymore to remind us of the work that needs to be done.

[Eric Wieser]

Then maybe doc-gen should learn to read the copyright header too, if it can't find a module docstring?

[Bryan Gin-ge Chen]

Ideally we would have a lint-sprint that adds proper module docs...

[Eric Wieser]

I'm thinking that just having a title visible on 100 more doc pages would be a big improvement

[Eric Wieser]

Can we add a different marker for ERR_DOC so that we keep that reminder?

[Eric Wieser]

Heck, requiring more than three non-blank lines of doc is probably enough

[Johan Commelin]

Eric Wieser said:

Can we add a different marker for ERR_DOC so that we keep that reminder?

That would solve the issue. If you can do something like that, you get my :thumbs_up: