Remaining things to fix after GitHub Pages migration.

[Zimmi48]

A lot of links were broken with the migration to GitHub Pages because it doesn't support HTTP redirects. A solution based on Javascript on a 404 page was proposed by @huynhtrankhanh in #232 and it has allowed resolving the most pressing broken link issues. It can be extended to fix other broken links that need to be fixed.

We can live with this for a couple of weeks to see if we are satisfied with this solution, or if we prefer to migrate to an infrastructure that supports HTTP redirects, like @silene said he could explore.

I'm opening this issue to make the list of remaining things to fix after #232 (already fixed issues are #230, as well as the long-standing issues #196, #188, #131, #111, #110).

Tasks

Beta Give feedback

1. CSS is broken on standard library documentation #228
   +0
2. Decide whether to ditch the HTML redirects under pages/{distrib,stdlib,library} for index and change pages.
3. HTML redirects are cached by the browser. #231 (does this issue also apply to the 404.html redirects or would it be fixed by ditching the HTML redirects mentioned just above?)
4. Decide what to do with the https://github.com/coq/refman repository. Currently, it contains a copy of the documentation also present in the https://github.com/coq/doc repository under the current version. We could remove it and redirect to the current version of the refman just like it is done for the stdlib.
5. Possibly add the old versions of the documentation to the https://github.com/coq/doc repository so that their links are not broken either.
6. Revert or partially revert Update doc URLs coq#18108.
7. List the remaining broken links based on what used to be in the Apache configuration files.
8. Add redirects for Nix links.
9. Add redirects for coq-workshop links.
10. Add redirects for tutorial links.
11. Add redirects for opam links.
12. Add redirect for related-tools.
13. Add redirects for wiki links.
14. Add redirects for Bugzilla links.

Regarding point 4 above, removing the https://github.com/coq/refman repository means that we would no longer provide a "moving target" refman version, and maybe that's a good thing (I was already suggesting this in #111). People could still craft "moving target" URLs based on our redirection mechanism. This would also make the release process simpler (one manual step to remove).

[Zimmi48]

Here are relevant parts of the Apache conf:

From alias.conf:

# Nix shell for the coq-nix-toolbox
RewriteRule ^nix/toolbox(|/)$ https://github.com/coq-community/coq-nix-toolbox/archive/master.tar.gz [R,L]
# Nix shell for math-comp
RewriteRule ^nix/math-comp(|/)$ https://github.com/math-comp/math-comp-nix/archive/v2.tar.gz [R,L]
# Main page of Coq Workshop has moved to external website
RewriteRule ^coq-workshop(|/)$ https://coq-workshop.gitlab.io/ [R=301,L]
# Mike Nahas's tutorial is not hosted on the Coq website anymore
RewriteRule ^tutorial-nahas(|.html|/)$ https://mdnahas.github.io/doc/nahas_tutorial [R=301,L]
RewriteRule ^files/nahas_tutorial.v$ https://mdnahas.github.io/doc/nahas_tutorial.v [R=301,L]
# opam/www/using.html and co. moved to opam-using early 2019
RewriteRule ^opam/www/(layout|packaging|using).html$ opam-$1.html [R=301,L]
# Awesome Coq tools section replaced related-tools page mid 2021
RewriteRule ^related-tools(|.html|/)$ https://github.com/coq-community/awesome-coq#tools [NE,R=301,L]

From main.conf:

  RewriteRule ^coq-workshop/files/(.*) files/$1 [L]
  RewriteRule ^coq-workshop/2009/cfp$ /news/69.html [L]

  RewriteRule ^library-eng.html$  /stdlib [L,R=301]
  RewriteRule ^doc-eng.html$      /refman [L,R=301]
  Redirect /cocorico https://github.com/coq/coq/wiki
  Redirect /faq https://github.com/coq/coq/wiki/The-Coq-FAQ

  ## Pierre : redirect old bugs to github issues

  ## First, special rules for bug numbers that changed during the transition
  Include /etc/apache2/bugzilla-compat.conf

  ## When the bug number is the same, a generic rule is enough
  RewriteCond %{QUERY_STRING} ^id=([0-9]+)
  RewriteRule ^bugs/show_bug.cgi$ https://github.com/coq/coq/issues/%1? [L,R=301]

  ## Pierre : shortcut bug/1234 -> https://github/com/coq/coq/issues/1234

  RewriteRule ^bug/([0-9]+)$ https://github.com/coq/coq/issues/$1 [L,R=301]

The bugzilla-compat.conf matches the renumbered issue table that is available in https://github.com/coq/coq/blob/master/dev/bugzilla2github_stripped.csv.

[Zimmi48]

Possibly add the old versions of the documentation to the https://github.com/coq/doc repository so that their links are not broken either.

@vbgl FYI, I've proceeded to do that for the latest versions of each release between V8.0 and V8.8, so you might want to add these to the doc index page.

Decide whether to ditch the HTML redirects under pages/{distrib,stdlib,library} for index and change pages.

On this aspect, I think I will proceed with the removal if there is no opposition.

Decide what to do with the https://github.com/coq/refman repository. Currently, it contains a copy of the documentation also present in the https://github.com/coq/doc repository under the current version. We could remove it and redirect to the current version of the refman just like it is done for the stdlib.

On this aspect as well, I think I will proceed with the removal if there is no opposition (and an additional redirection to replace it). cc @maximedenes FYI

[Zimmi48]

Regarding this:

Add redirects for Nix links.

I've done it now, but unfortunately, since these links were for use with Nix and not a web browser, an HTML redirection doesn't help. So we'll have to fix these links and use the real links behind in the documentation that used them. (At least as long as we do not migrate to a web hosting that supports HTTP redirects.)

cc @CohenCyril @palmskog FYI

[palmskog]

@Zimmi48 but I thought we agreed to move all Nix stuff to coq-community.org/nix? And just update all references to the original links.

[Zimmi48]

Ah right, I completely forgot that this was our conclusion.

For now, I have updated the references in https://github.com/math-comp/math-comp/wiki/Using-nix and https://github.com/coq-community/coq-nix-toolbox/blob/master/README.md (documentation) and I have opened a PR at coq-community/templates#122 for the templates.

For the templates, I feel like having the raw link is no big deal.

For the rest, we can indeed consider the coq-community.org/nix solution, although one issue would be that this would require hosting up-to-date tarballs in a git branch in a coq-community/nix repo (which would change every time the Coq Nix Toolbox is updated, which often happens). I don't know if that would be reasonable in terms of repository size or if there is a solution that would not require updating the repository as often.

[Zimmi48]

Following the 8.19 release, we have decided with @SkySkimmer to not update the refman repository that provided a moving target URL for the refman (this repository could now be deleted as it serves no purpose anymore) and instead redirect https://coq.inria.fr/refman to a fixed version of the refman corresponding to the current version like what was already the case for https://coq.inria.fr/distrib/current/refman and https://coq.inria.fr/stdlib.

I also propose to resolve another item in the list above by ditching the HTML redirects and keeping only the 404 Javascript redirects.

[Zimmi48]

this repository could now be deleted as it serves no purpose anymore

done