Stream: Coq users

Topic: Changing version of refman without losing page


view this post on Zulip Ali Caglayan (Oct 05 2021 at 09:51):

Is it difficult to match pages between the versions of the refman? I very often want to look at more recent documentation when googling stuff, but this always brings me to the homepage. Is it possible to keep the page?

view this post on Zulip Théo Zimmermann (Oct 05 2021 at 09:54):

The widget was introduced by @Clément Pit-Claudel. I haven't dug into how it works. However, matching pages across versions should be easy. Especially given that when pages were renamed / split, we've introduced redirections for old links to continue to work (except the anchors).

view this post on Zulip Théo Zimmermann (Oct 05 2021 at 09:55):

For instance, https://coq.inria.fr/refman/language/gallina-specification-language.html redirects to https://coq.inria.fr/refman/language/core/index.html or https://coq.inria.fr/refman/addendum/canonical-structures.html redirects to https://coq.inria.fr/refman/language/extensions/canonical.html.

view this post on Zulip Ali Caglayan (Oct 05 2021 at 09:55):

Right, but what about pages which get moved/deleted

view this post on Zulip Ali Caglayan (Oct 05 2021 at 09:56):

I guess we could always fallback on the home page

view this post on Zulip Théo Zimmermann (Oct 05 2021 at 09:57):

There is always an appropriate fallback. In the first example I gave, the two pages do not match exactly. The first one was split into multiple pages. So it redirects to the most appropriate fallback.

view this post on Zulip Théo Zimmermann (Oct 05 2021 at 09:57):

But yeah, in the end the ultimate fallback is the home page

view this post on Zulip Ali Caglayan (Oct 05 2021 at 09:57):

Do we have to specify all the "links" by hand?

view this post on Zulip Théo Zimmermann (Oct 05 2021 at 09:58):

I have no idea how this widget works, but if someone knows and I just have to provide a list of renamed pages, I am ready to do this work.

view this post on Zulip Théo Zimmermann (Oct 05 2021 at 09:58):

It wouldn't take me so long, as I know what has changed quite well.

view this post on Zulip Ali Caglayan (Oct 05 2021 at 09:58):

OK I'll create an issue on github so we can work on it soon


Last updated: Feb 01 2023 at 13:03 UTC