HTML redirects are cached by the browser.

[Zimmi48]

This is a serious issue in the case of:

• https://coq.inria.fr/distrib/current/refman/
• https://coq.inria.fr/distrib/current/stdlib/
• https://coq.inria.fr/distrib/current/refman/changes.html

The redirection is supposed to be to the current version of the doc, but after updating the HTML redirects (which happened automatically when merging #222), users that had previously clicked on this link can still be redirected to the previous version.

Unfortunately, I do not see any solution to this issue besides:

• switching to a service that supports HTTP redirects, like GitLab Pages (was discussed in yesterday's Coq Call)
• redirecting these pages to a moving copy of the documentation (like coq.inria.fr/refman).

cc @maximedenes FYI

[maximedenes]

Isn't there a way to control the browsers' cache policy?

[Zimmi48]

This Stack Overflow answer from 13 years ago suggests adding:

<META HTTP-EQUIV="CACHE-CONTROL" CONTENT="NO-CACHE">
<META HTTP-EQUIV="PRAGMA" CONTENT="NO-CACHE">
<META HTTP-EQUIV="Expires" CONTENT="-1"> 

[jp-diegidio]

A no caching should actually be solved on the server side with response headers, not in the HTML. See this answer for a more up-to date perspective: https://stackoverflow.com/a/2068407/22862809

So (if I understand what you referring to, I have just skimmed through the code) caching should be disabled for all things under the distrib/current folder.

That said, there are also potentially issues with how the redirects are performed in those pages: the best again would be the server directly issuing the redirect, in this case maybe with an HTTP status code of 303: https://developer.mozilla.org/en-US/docs/Web/HTTP/Status/303

Alternatively, a redirect from JS, similar to how it happens in 404.html, while the page is showing something like "You are being redirected in 5 secs: click this link if that does not happen..." is also a common solution.

[Zimmi48]

Thanks for the feedback! Unfortunately, GitHub Pages doesn't provide the option for server-side configuration. However, if I understand you correctly, the JS-based redirection that was implemented in #232 is not subject to the same caching issue?

[jp-diegidio]

I thought I had seen some nginx configuration somewhere...? But as said I have just skimmed the repo.

No, the redirects under distrib/current are not robust (but it's not easy to give you references here), but I meant that as a separate issue: which might be contributing to the caching issue on some client platforms, but not necessarily.

[jp-diegidio]

Anyway, I mean redirects from HTML headers are "not robust" just as much as it is not robust or even hardly supported anymore to set no caching from HTML headers.

[Zimmi48]

I thought I had seen some nginx configuration somewhere...? But as said I have just skimmed the repo.

There used to be an Apache server (before migrating to GitHub Pages, cf. #233), so it's possible that some remains of (unused) Apache configuration can be found in the repo.