Feedback: have Lean 3 stuff point to Lean 4 equivalent

Stream: new members

[Alex Altair]

A recurring problem that I'm having as a new person trying to learn is that I will frequently search for something, or be clicking links somewhere, and I'll end up on a page that's about Lean 3. Only, it's totally non-obvious, and sometimes it doesn't even say "3" anywhere -- just plain "Lean" or "mathlib". I have to be fairly paranoid to not accidentally spend twenty minutes reading something obsolete. And even when I've identified that I'm on a Lean 3 resource, it's often hard to figure out what the Lean 4 equivalent is.

[Alex Altair]

Here's a detailed example: the Mathlib documentation.

Let's say I do a google search and get dropped on a random page like this. The first thing I notice is that the URL has no "3" in it. There is a 3 in the top bar, but it doesn't exactly draw attention. Let's say I notice it and then want to go to the Mathlib4 version. It would be super great if I could just click something and be automatically taken there, but I don't see anything like that. Another thing I sometimes try is whether the URL has a quick modification. If there was a "3" in the URL, I would try changing it to a 4. There isn't, but I have figured out that the Mathlib4 doc URLs have a mathlib4_docs in them, so I try editing the mathlib_docs of the example URL to mathlib4_docs. Alas, that gives me a 404. And the 404 page doesn't even have the side bar for me to try to manually nagivate to the equivalent linear algebra page. So, then I just try to google search "lean 4 range_eq_of_proj". This actually brings me back to the lean 3 doc page. Nothing above the fold is a lean 4 doc link. Okay, so... I guess I can try to search from the Mathlib4 docs homepage? Fortunately https://leanprover-community.github.io/mathlib4_docs/ is a valid URL (although the home page just says "This was built using Lean 4 at commit a62d2fd4979671b76b8ab13ccbe4fdf410ec0d9d" and is mostly empty, which makes me think I'm not supposed to be on this page). I paste the name into the search bar, which brings up one result, which... isn't what I'm looking for. Then I try using the sidebar to manually find LinAlg and "Projection", and then control-f for range_eq_of_proj, which does finally work.

[Alex Altair]

Comparing the URLS for the Mathlib3 and 4 versions of this page, they are different in multiple minor ways, but in ways that seem like they could be linked between with a script.

[Alex Altair]

So my main suggestions for this use case are;

1) Put a big, colored banner at the top of the Mathlib3 docs that tell you it's deprecated and you probably want the Mathlib4 docs
2) Then also put a link to said Mathlib4 docs, to whatever level of drill-down is practical. (Even just a link to the main page would be helpful.)
3) It would help if we could get the Lean3 stuff to stop being at the top of google searches, and instead have it be the Lean4 stuff. I don't know anything about SEO but I assuming something could be done here.

[Alex Altair]

Separately, it also seems somewhat odd to me that the Mathlib docs don't have a clear link to the homepage. I can't click the big word "Documentation" nor the medium words "General documentation" instead it's the tiny word "index" below that

[Alex Altair]

Also the thing in the title bar that says e.g. "Mathlib.LinearAlgebra.Projection" looks like it should be some breadcrumbs where I could click "LinearAlgebra" to get to the main page for linalg, but it's not; instead I have to manually go through the sidebar tree to find Mathlib.LinearAlgebra.Basic" (and I have to know it's the "Basic" file that serves as a home page)

[Alex Altair]

Here's another example; AFAICT this resource nowhere indicates that it's about Lean3, but the syntax in the examples seem to be Lean3

[Patrick Massot]

Flagging https://lean-lang.org/reference/ is for @Sebastian Ullrich. The https://leanprover-community.github.io/mathlib_docs/ issue will be tackled by mathlib maintainers.

[Yaël Dillies]

Alex Altair said:

Also the thing in the title bar that says e.g. "Mathlib.LinearAlgebra.Projection" looks like it should be some breadcrumbs where I could click "LinearAlgebra" to get to the main page for linalg, but it's not; instead I have to manually go through the sidebar tree to find Mathlib.LinearAlgebra.Basic" (and I have to know it's the "Basic" file that serves as a home page)

That specific criticism is hard to act on given that there's no "main page for linalg" and in general no "main page for folder X". The .Basic files are usually the most basic ones across their folder but they do not always exist and sometimes are not so basic.

[Yaël Dillies]

We could certainly create one file per folder (at least the big common ones) whose sole purpose is to provide documentation for the folder and point to useful resources. I could stand behind that.

[Eric Wieser]

One thing that would be very valuable, but requires some time to set up, is to have the #align information in mathlib4 presented in the mathlib3 docs, so that every declaration in the mathlib docs has a "go to lean 4 version " link

[Eric Wieser]

In particular, the missing pieces here are:

• Export the align data in a way that the mathlib3 doc-gen (python code) can read it; a json dictionary would suffice
• Implement permalinks in doc-gen4. We had these in doc-gen3, but it's no long possible to link to definition if you don't also know which file its in
• Work out how to expose the latest #align output in CI to the doc-gen CI (github releases? A secret url in the mathlib4 docs that the mathlib3 docs CI fetches?)

[Patrick Massot]

Eric Wieser said:

One thing that would be very valuable, but requires some time to set up, is to have the #align information in mathlib4 presented in the mathlib3 docs, so that every declaration in the mathlib docs has a "go to lean 4 version " link

This sounds like a lot of work compared to putting a huge red banner on every mathlib3 doc page telling people they shouldn't be reading it.

[Eric Wieser]

Yes, but this doesn't help people who searched google for mathlib has_deriv_at_sin and only got offered the lean3 docs

[Julian Berman]

Perhaps adding link rel="canonical"s all over helps there.

[Alex Altair]

(Also wanna note that I have generally been having a great time learning Lean, everything is so much more functional and pleasant than I expected! I can tell that everyone has been putting tons of work into not just the port, but all aspects of the software)

[Kevin Buzzard]

Re "I blind googled and found mathlib3 docs" -- why not just bookmark the mathlib 4 docs and search them instead?

[Alex Altair]

@Kevin Buzzard Partly because I don't know enough to know where what I'm looking for is, but also, there are a whole bunch of other great resources that I might want to see results from

[Kevin Buzzard]

I can probably list on one hand the great resources in Lean 4 right now. #tpil , #mil , #nng4 (is that even a thing?), and the docs https://leanprover-community.github.io/mathlib4_docs/

[Jireh Loreaux]

Kevin, you forgot #fpil

[Alex Altair]

(There's also a lot of blog posts, mastodon posts, youtube video descriptions, any resources people write in the future that I don't know about -- I'm definitely going to keep googling stuff!)

[Kevin Buzzard]

Yes, future you should of course Google. I'm just suggesting that present you might want to consider just looking at the currently very finite list of resources.

As well as the functional programming book that Jireh mentioned there's also the lean 4 reference manual and the metaprogramming book, these are good lean 4 references to add to my list above

[Kevin Buzzard]

So we're now on two hands