mathlib3 docs have no warning

Stream: general

[Kevin Buzzard]

It was just pointed out to me that
a) if you go to google and search for mathlib documentation then the top link is the mathlib3 page https://leanprover-community.github.io/mathlib_docs/index.html

b) This page gives no indication that mathlib3 is deprecated and it's almost certain that you're in the wrong place.

How do I go about fixing this?

[Bryan Gin-ge Chen]

Perhaps adding some suitable warning text here to the header in doc-gen3 will be enough?

[Bryan Gin-ge Chen]

If you submit a PR I can check and deploy it when I have a chance.

[Kevin Buzzard]

That will only change the top line of the web page, right?

Where is the line that says "Welcome to mathlib 3's documentation page" stored? I think it should say "WARNING: this is the mathlib 3 documentation page. Mathlib3 is no longer maintained, and you probably want the <mathlib4 page>(link)"

[Eric Wieser]

Here: https://github.com/leanprover-community/doc-gen/blob/0ab85f2ad359ecb52311f31bbf61ea9cf60ffb4c/templates/index.j2

[Bryan Gin-ge Chen]

Eric beat me to the index template link which should be fixed as well, but my hope is that changing the header will make the warning show up on every doc page.

[Bhavik Mehta]

I think it would be super useful if those pages linked to the relevant mathlib4 doc page, if that's feasible to do.

[Eric Wieser]

In theory we can do that with the align data, but that's much more work that what Kevin suggests, and the two are orthogonal