stable links to the reference manual

Stream: lean4

[Jireh Loreaux]

The reference manual is changing continually (which is great!), but what if I want to link to a certain section without the link going stale?

Does the FRO host past versions of the reference manual on the website (I see the changelog, but I don't know how to access the reference manual for v4.21.0, for example)? Can we trust that the links (e.g., for section anchors) will be stable? I understand these will likely not be stable indefinitely, but even for a period of a few years would be suitable.

Context: I would like to link to a section of the reference manual in a paper.

[Jireh Loreaux]

@David Thrane Christiansen do you happen to have an answer to this? Even if the answer is: "we're not going to support stable links at the moment" it would be good to know.

[David Thrane Christiansen]

Hey - just got back from vacation today. The answer is that if you know what you're doing, you can make a stable link to most sections, but this should be easier than it is! Here's how to do it today:

If you look at the URL for a copy of the reference manual, it's got the following structure: https://lean-lang.org/doc/reference/VER/, where VER is either latest, stable, or a major version. So the first step is to put in the version that you're linking to, rather than using a mutable reference like stable or latest. For example: https://lean-lang.org/doc/reference/4.21.0/.

The HTML hosted at those addresses is mostly immutable. We may update it cosmetically, but we don't plan to move it around, delete it, or substantially change the contents - the changes would be things like adding a banner that says "This is the documentation for Lean 4.21. For the latest version, click here", adding some kind of analytics if we change vendors, or perhaps tweaking fonts or colors to match website updates.

To get a stable link to a section, you can use the little "link" icon to the right. Right-click it and say "copy link". This gets you a link to that section's stable identifier that will be preserved as the manual is modified - that's how you'd make an "evergreen" link that will always work. Note that it uses a bit of client-side JS to map the stable name to the destination, so for a paper you might want to just click the link and then copy-paste from the address bar. Sections or other content without the little link icon will have some kind of internally generated HTML ID that you can also link to (as long as its old content), but it may be verbose.

Does this make sense? Any further questions?

[Jireh Loreaux]

Thanks David! This is excellent. Sorry for pinging. I didn't realize you were on vacation and just wanted to avoid this being forgotten. No further questions for now.