broken links on lean-lang.org

Stream: lean4

[Alex Meiburg]

All four "use cases" links on https://lean-lang.org/use-cases/ are broken. Not sure where they're supposed to point, just flagging!

[Julian Berman]

Looks like a wrong relative URL for the links, instead of e.g. https://lean-lang.org/cedar it looks like the intended URL is https://lean-lang.org/use-cases/cedar (and same for the rest)

[Ashley Blacquiere]

Fixed! Thanks for catching that!

[Julian Berman]

In case it's helpful, https://www.drlinkcheck.com/ (or even better Google Search Console but that requires someone who owns the domain to use it) is nice and still finds a decent number of broken links. Some are broken downstream, e.g. because someone put a broken link in their README and reservoir indexed that, but some are "real", e.g. here I see:

• https://reservoir.lean-lang.org/ has "Lean API" in its footer which goes to https://lean-lang.org/language-reference (404) -- which seems redundant because just above it is a link to the reference
• https://lean-lang.org/learn/ links to pantograph at https://git.leni.sh/aniva/Pantograph (404) which I guess is now https://github.com/leanprover/Pantograph
• https://lean-lang.org/fro/team/ links to https://www.convergentresearch.org/adam-marblestone (404)

(and there's at least 5 or 6 more that were found here before it ran out of free quota)