Invisibly redirect some pages to https://coq.github.io/doc?

[Zimmi48]

Since the plan has moved from relying on GH pages for everything to using a new hosting service, but we deploy documentation to https://coq.github.io/doc/, it would be good if https://coq.inria.fr/doc/ could become an alias (invisible redirection) to https://coq.github.io/doc.

I would also suggest that from now on, https://coq.inria.fr/refman and https://coq.inria.fr/stdlib should redirect visibly (so that people stop putting URLs without a version number in their papers) to a URL like https://coq.inria.fr/doc/V8.9.1/refman/ (which would then invisibly redirect to https://coq.github.io/doc/V8.9.1/refman/).

Since we already define the current stable release tag in the website sources, the website infrastructure should use this information to set up this redirection: this would be one less manual step for the RM when preparing a new release. A CI test should however ensure that the webpage has already been deployed before this tag can be updated on the website.

[maximedenes]

I would also suggest that from now on, https://coq.inria.fr/refman and https://coq.inria.fr/stdlib should redirect visibly (so that people stop putting URLs without a version number in their papers) to a URL like https://coq.inria.fr/doc/V8.9.1/refman/ (which would then invisibly redirect to https://coq.github.io/doc/V8.9.1/refman/).

I think this is a bit dangerous, since browser caching is typically very aggressive w.r.t. these redirections.

[Zimmi48]

To be more specific, I suggest following the model of Zenodo (and probably other archives such as HAL), where there is a fixed URL (e.g. https://doi.org/10.5281/zenodo.1003420) that redirects to the latest version of the resource (e.g. https://zenodo.org/record/2554024) and if you go to an earlier version of the resource (e.g. https://zenodo.org/record/1219885, because you have bookmarked it), then it displays a banner saying that there is a new version available.

But anyway, that this redirection is visible or invisible is not the most important part of my message. This could be debated separately.

[maximedenes]

to https://coq.github.io/doc

@Zimmi48 I was having a look at how to implement such a reverse proxy (I assume that's what you meant, not sure what an "invisible redirection" is concretely).

But I now realized this page is completely raw (unthemed, etc). We should probably first improve it so that it integrates reasonably well with the website, shouldn't we?

[Zimmi48]

Oh that's interesting, I didn't even realize we had such an index page!
And for sure, that would be a first step.

[Zimmi48]

There is something weird now, which is that https://coq.inria.fr/distrib/current/refman/ and https://coq.inria.fr/distrib/current/stdlib/ exist (and I suppose they both correspond to version 8.9.1, although only the refman displays the version), but https://coq.inria.fr/distrib/current/ only contains a files/ sub-folder which corresponds to the V8.9.0 one. Can we remove https://coq.inria.fr/distrib/current/ altogether?

[Zimmi48]

Can we remove https://coq.inria.fr/distrib/current/ altogether?

Now done.

[Zimmi48]

As a temporary solution to rocq-prover/rocq#10619, I have set up the necessary reverse proxies so that:

• https://coq.inria.fr/distrib/V8.XXX/{stdlib,refman,api}/* are defined, and redirect to https://coq.github.io/doc/V8.XXX/... if XXX is 9.1 or starts with a 1 followed by another digit. So this includes in particular:
• https://coq.inria.fr/distrib/V8.9.1/refman/
• https://coq.inria.fr/distrib/V8.10+beta1/refman/
• https://coq.inria.fr/distrib/V8.10+beta2/refman/
• https://coq.inria.fr/distrib/V8.10+beta3/refman/
• https://coq.inria.fr/distrib/V8.10.0/refman/
• https://coq.inria.fr/distrib/V8.10.1/refman/

But also versions that do not yet exist (and will lead to a 404 page until they do) like:

• https://coq.inria.fr/distrib/V8.10.2/refman/
• https://coq.inria.fr/distrib/V8.11+beta1/refman/
• etc.

The way of implementing this is with these rules:

ProxyPass /distrib/current/refman/ https://coq.github.io/doc/V8.10.1/refman/

ProxyPass /distrib/current/stdlib/ https://coq.github.io/doc/V8.10.1/stdlib/

ProxyPass /distrib/V8.9.1/refman/ https://coq.github.io/doc/V8.9.1/refman/

ProxyPass /distrib/V8.9.1/stdlib/ https://coq.github.io/doc/V8.9.1/stdlib/

ProxyPassMatch ^/distrib/(V8\.1[0-9].*)/(refman|stdlib|api)/(.*) https://coq.github.io/doc/$1/$2/$3

However, there is still an issue when typing these URLs without the trailing slash. The behavior that can be currently observed is surprising because I don't remember changing anything that should provoke it, but I probably accidentally did such an edition, and because these Apache configuration files are not versioned (cf. #131), I didn't realize it and couldn't revert it. The issue is that without the trailing slash, the web server looks for the requested files inside the static/ sub-folder. E.g. https://coq.inria.fr/refman displays the error message:

The requested URL /static/distrib/current/refman was not found on this server.

This may be related to the code here:

https://github.com/coq/www/blob/66474cb8474c0f4042d5388c6341d74750f81a64/aliases.footer.conf#L4-L11

[Zimmi48]

As a future solution, I think we should aim for something alike what I was suggesting initially, i.e. to have the documentation reside at https://coq.inria.fr/doc/${version}/{refman,stdlib,api}. It would be much easier to reverse proxy the entire https://coq.inria.fr/doc in https://coq.github.io/doc. Furthermore, it would avoid issues such as someone starting from the URL https://coq.inria.fr/distrib/V8.10.1/refman, removing the latter parts of the URL to discover the existence of https://coq.inria.fr/distrib, and then wondering why listed versions stop at V8.9.0.

[Zimmi48]

Mostly fixed since the GitHub Pages migration, although some questions remain to debate in a new issue.