Linter for links?

Stream: mathlib4

[Kenny Lau]

In 1 there is a link "AlgebraicGeometry/PresheafedSpace/Gluing.lean" which is a 404 when one clicks on it (Permalink to source code). Maybe we can have a linter to check for links?

[Johan Commelin]

Sounds like a good idea. Anyone have experience with existing solutions? There must be many tools that check for dead links.

[Jz Pan]

There is a problem that the doc is build in a separate repository, so of course such linter is naturally added to doc-gen4 but it will not catch the problem until a day later (or so).

If you want a linter to check docstrings then its function will parallel to doc-gen4 which IMHO produces code duplications.

[Johan Commelin]

I think this type of linter shouldn't run on every PR. It should rather run once a week, and post a report to zulip.

[Jz Pan]

Johan Commelin said:

I think this type of linter shouldn't run on every PR. It should rather run once a week, and post a report to zulip.

Oh that's OK. Then we can implement it in doc-gen4 and let it generate a report each time the mathlib4 docs is rebuild (which is three times a day).

[Johan Commelin]

Sounds good, but I think it shouldn't post 3x a day. 1/d or 1/w sounds plenty.

[Eric Wieser]

I don't think we actually care about dead links. We care about filenames which don't exist. That is a much cheaper linter to run.

[Johan Commelin]

While we are at it, we might as well care about dead links.

[Eric Wieser]

I think human readers are usually a good enough tool for spotting those. At any rate, this thread was motivated by a bad filename, not a bad external link

[Michael Rothgang]

Eric Wieser said:

I don't think we actually care about dead links. We care about filenames which don't exist. That is a much cheaper linter to run.

And it could be implemented within mathlib!

[Eric Wieser]

Exactly!