search

leanprover-community / leanprover-community.github.io

Hosts the website for mathlib and other Lean community infrastructure.
https://leanprover-community.github.io/
MIT License
54 stars 123 forks source link

links inside declarations on 100 theorems page are broken #390

Closed robertylewis closed 10 months ago

robertylewis commented 1 year ago

At https://leanprover-community.github.io/100.html we format and linkify each declaration using info from doc-gen. But it seems the format of this info has changed since mathlib3 and now has relative links, so these links are broken: e.g. irrational_sqrt_2 links to https://leanprover-community.github.io/Mathlib/Data/Real/Irrational.html#irrational_sqrt_two

We could add a <base> tag to this page (and check that none of the other links are relative), or find some other solution.

PatrickMassot commented 11 months ago

I cannot reproduce that. Do you still see this issue?

robertylewis commented 10 months ago

Yes, I still see this issue. If you click on irrational_sqrt_two, or Irrational, or Real.sqrt, ... in the statement of item 1, it takes you to a nonexistent page.

PatrickMassot commented 10 months ago

Oh I didn't notice those links! I tried the blue ones at the bottom of each entry. I'll investigate.

PatrickMassot commented 10 months ago

Ok, it turns out it was left explicitly broken in #349 for some very mysterious reason since the fix was trivial. This is now fixed.