search

coq / coq.github.io

Source files of the coq.inria.fr website
https://coq.inria.fr/
Other
15 stars 37 forks source link

Old links to library docs are broken #230

Closed RalfJung closed 11 months ago

RalfJung commented 12 months ago

Google search results are full of links like https://coq.inria.fr/library/Coq.Lists.List.html that currently no longer work. It'd be great to get proper redirects for these as right now, finding the right docs can be quite painful.

Zimmi48 commented 12 months ago

Indeed. As discussed on Zulip, the issue is that GitHub Pages do not support HTTP redirects and it is not realistic to add HTML redirects for every sub-path. A JS-based solution in a 404 might be possible. Otherwise, the remaining options are to re-migrate to a static page provider that supports HTTP redirects (such as GitLab Pages), to leave these links broken, or to deploy the documentation in a library repository (similarly to what was done for refman).

Note that for the refman, the current state of things is that https://coq.inria.fr/distrib/.../index.html redirects to https://coq.inria.fr/doc/.../refman/index.html (but not for other sub-paths), including for current which redirects to the current version of the refman, but https://coq.inria.fr/refman uses a second deployment (second copy) of the refman hosted at https://github.com/coq/refman. The same could possibly be done for library (this is what I meant above as the last option).

Zimmi48 commented 12 months ago

Let's migrate this issue to the proper repository.

Zimmi48 commented 12 months ago

For future reference: if we do fix this issue in a reliable way (including for /distrib links), we could revert coq/coq#18108.

Zimmi48 commented 11 months ago

This was fixed in #232. I'll open a new issue with the list of things remaining to do. If you find more broken links, please contribute to it.