Stream: Coq devs & plugin devs

Topic: Coq website migration


view this post on Zulip Maxime Dénès (Sep 13 2023 at 06:16):

Hi there,

I hope to be able to complete today the migration of the Coq website to GitHub Pages (before we get another payment incident). It should happen transparently, but in case you notice something unusual, please post here. Thanks!

view this post on Zulip Maxime Dénès (Sep 13 2023 at 08:42):

In fact, it is not going to be as transpartent as I thought w.r.t. to the URLs under /distrib. So I need to prepare some updates first.

view this post on Zulip Karl Palmskog (Sep 13 2023 at 20:17):

@Maxime Dénès it looks like the opam archive is not getting deployed to https://coq.inria.fr/opam/released/ properly. For example, https://github.com/coq/opam/tree/master/released/packages/coq-aac-tactics/coq-aac-tactics.8.18.0 is in Git but not in index.tar.gz or https://coq.inria.fr/opam/released/packages/coq-aac-tactics/

view this post on Zulip Karl Palmskog (Sep 13 2023 at 20:18):

unless this is fixed, only a quite small subset of packages can be installed for 8.18.0. For example, all MathComp 2.0 packages are blocked on 8.18.0 due to coq-elpi.1.19.0 not being in released

view this post on Zulip Karl Palmskog (Sep 13 2023 at 20:20):

from what I can see, index.tar.gz is updated, but only with an old/stale version of the repo

view this post on Zulip Karl Palmskog (Sep 13 2023 at 20:22):

also it will block Docker image of 8.18.0

view this post on Zulip Karl Palmskog (Sep 14 2023 at 16:54):

workaround for getting latest Coq opam packages via local opam repo described here: https://github.com/coq/opam/issues/2727

view this post on Zulip Maxime Dénès (Sep 15 2023 at 07:25):

It is strange, because I didn't perform the switch yet. Will have a look at the pb today.

view this post on Zulip Karl Palmskog (Sep 15 2023 at 11:15):

very strange, index.tar.gz seems to be deployed to https://coq.inria.fr/opam/released/ unchanged every few hours

view this post on Zulip Maxime Dénès (Sep 15 2023 at 16:16):

Ok, I found the cause, fixing

view this post on Zulip Maxime Dénès (Sep 15 2023 at 16:18):

Should be better now! @Karl Palmskog
Thanks for reporting!

view this post on Zulip Karl Palmskog (Sep 15 2023 at 16:24):

thanks, I can confirm the key 8.18 packages are now out on released opam repo

view this post on Zulip Maxime Dénès (Oct 02 2023 at 12:15):

I'm going to request the change of Coq's DNS records. The service will inevitably be disturbed a bit, we'll try to minimize the annoyance. If we don't do anything, the website will anyway be cut again today or tomorrow, most likely.

view this post on Zulip Karl Palmskog (Oct 02 2023 at 12:18):

looks like I get an infinite redirect from this URL, is this expected? https://coq.inria.fr/stdlib/

view this post on Zulip Théo Zimmermann (Oct 02 2023 at 13:02):

This was a temporary quirk, but this should be fixed now.

view this post on Zulip Maxime Dénès (Oct 02 2023 at 17:32):

The website is back up at the new location (modulo DNS propagation). Let's hope nothing catastrophic will happen :)

view this post on Zulip Jason Gross (Oct 02 2023 at 21:00):

https://coq.inria.fr/library/Coq.QArith.QArith_base.html gives a github 404 (link comes from google searching)

view this post on Zulip Jason Gross (Oct 02 2023 at 21:01):

https://coq.inria.fr/stdlib/ is also a 404

view this post on Zulip Karl Palmskog (Oct 03 2023 at 06:16):

looks like all locations of documentation moved, e.g., stdlib is now at https://coq.inria.fr/doc/current/stdlib/

view this post on Zulip Karl Palmskog (Oct 03 2023 at 06:18):

@Maxime Dénès you probably want to add additional forwards so the following old locations don't go to 404:

view this post on Zulip Maxime Dénès (Oct 03 2023 at 06:24):

I'm afraid I won't have time to do it this week (did the migration in emergency just so that the website wouldn't be cut), but the good thing is anybody can do by submitting a PR to https://github.com/coq/coq.github.io. A model of a redirection can be seen at https://github.com/coq/coq.github.io/blob/master/pages/distrib/current/refman/index.html

view this post on Zulip Théo Zimmermann (Oct 03 2023 at 08:02):

If someone opens the PR, I can merge it.

view this post on Zulip Karl Palmskog (Oct 03 2023 at 08:15):

as reported by Gaëtan, the CSS for the Stdlib is also broken, that may take more than redirects to fix.

view this post on Zulip Théo Zimmermann (Oct 03 2023 at 08:16):

Yes. I have a less clear idea of how to fix this, but it may also be considered slightly less urgent than the broken URLs.

view this post on Zulip Huỳnh Trần Khanh (Oct 05 2023 at 14:19):

anybody can do by submitting a PR

I just found out the website repo doesn't have a license, so this means only Inria personnel can legally touch it

view this post on Zulip Karl Palmskog (Oct 05 2023 at 14:23):

it's unfortunate that there's indeed not any license, but many people who have rights to touch it are not employed by Inria

view this post on Zulip Enrico Tassi (Oct 05 2023 at 20:54):

I frankly don't know what having a website under, say, MIT means and if it is even desirable

view this post on Zulip Paolo Giarrusso (Oct 05 2023 at 20:59):

Because you want to prevent impersonation? Doing that while allowing local testing might be complicated. Maybe you'd want a different license for logos, hopefully there's already one?

view this post on Zulip Karl Palmskog (Oct 05 2023 at 21:22):

the website repo is full of code of various kinds, like code that generates stuff from yaml. A permissive code license would make sense to me.

view this post on Zulip Théo Zimmermann (Oct 06 2023 at 08:54):

Enrico Tassi said:

I frankly don't know what having a website under, say, MIT means and if it is even desirable

It means that people can reuse the contents. It doesn't mean that they can pretend that they are the official Coq website. It is absolutely desirable and a shame that we didn't notice that there was no license thus far.

view this post on Zulip Karl Palmskog (Oct 06 2023 at 08:55):

unfortunately, lack of license is seemingly a recurring theme among researchers (I wasn't aware until recently that Coq until version 7 had no license)

view this post on Zulip Théo Zimmermann (Oct 06 2023 at 08:56):

I wish the law was changed so that "no license" on publicly available code meant something else. But that's not gonna happen :stuck_out_tongue:

view this post on Zulip Karl Palmskog (Oct 06 2023 at 08:57):

it's going to happen in 80+ years? Mickey Mouse thing...

view this post on Zulip Karl Palmskog (Oct 06 2023 at 09:00):

I wish there was something like a license engineer position at universities and big public orgs that at least lobbies for people to choose a license. Doesn't mean everything has to be open source, but "no license" is sometimes even worse than "restrictive license"

view this post on Zulip Paolo Giarrusso (Oct 06 2023 at 09:35):

(could grant agencies require that, maybe as part of the open science push?)

view this post on Zulip Théo Zimmermann (Oct 06 2023 at 09:50):

I think some already do, actually.

view this post on Zulip Théo Zimmermann (Oct 09 2023 at 19:20):

Karl Palmskog said:

Maxime Dénès you probably want to add additional forwards so the following old locations don't go to 404:

For the record, I have just added HTML redirections for these two links. Unfortunately, this won't work for sub-paths. To be able to preserve working sub-paths, we would have to adopt a solution similar to the one that was chosen for the refman, i.e., when you go to coq.inria.fr/refman, you get a copy that was deployed at https://github.com/coq/refman, while when you go to coq.inria.fr/distrib/current/refman, you get a redirection to coq.inria.fr/doc/VX.Y.Z/refman (which doesn't work for sub-paths).

view this post on Zulip Théo Zimmermann (Oct 09 2023 at 19:22):

So, if we wanted to preserve the most possible valid historical links, we could create repositories:

view this post on Zulip Théo Zimmermann (Oct 09 2023 at 19:22):

But this would require deploying multiple copies of the doc in several places...

view this post on Zulip Théo Zimmermann (Oct 09 2023 at 19:22):

Up to discussion

view this post on Zulip Théo Zimmermann (Oct 09 2023 at 19:27):

I don't understand the CSS error however. There doesn't seem to be any broken link.

view this post on Zulip Paolo Giarrusso (Oct 09 2023 at 19:45):

https://coq.inria.fr/modules/node/node.css is broken here?

view this post on Zulip Paolo Giarrusso (Oct 09 2023 at 19:46):

Chrome's web console (from right-click->inspect) shows many 404s:
image.png

view this post on Zulip Paolo Giarrusso (Oct 09 2023 at 19:47):

roughly all of these broke, possibly because of missing redirections:

        <link type="text/css" rel="stylesheet" media="all" href="//coq.inria.fr/modules/node/node.css"/>
        <link type="text/css" rel="stylesheet" media="all" href="//coq.inria.fr/modules/system/defaults.css"/>
        <link type="text/css" rel="stylesheet" media="all" href="//coq.inria.fr/modules/system/system.css"/>
        <link type="text/css" rel="stylesheet" media="all" href="//coq.inria.fr/modules/user/user.css"/>
        <link type="text/css" rel="stylesheet" media="all" href="//coq.inria.fr/sites/all/themes/coq/style.css"/>
        <link type="text/css" rel="stylesheet" media="all" href="//coq.inria.fr/sites/all/themes/coq/coqdoc.css"/>

view this post on Zulip Paolo Giarrusso (Oct 09 2023 at 19:48):

(that's from https://coq.inria.fr/doc/v8.9/stdlib/Coq.Init.Specif.html, but https://coq.inria.fr/doc/V8.17.1/stdlib/ seems similar)

view this post on Zulip Huỳnh Trần Khanh (Oct 10 2023 at 01:26):

since the repository is all rights reserved I can't make a fix. but here's the general direction. to add redirects for arbitrary subpaths you just need to create a 404.html file then do some JavaScript

view this post on Zulip Huỳnh Trần Khanh (Oct 10 2023 at 01:27):

https://lea0.verou.me/2016/11/url-rewriting-with-github-pages/

view this post on Zulip Huỳnh Trần Khanh (Oct 10 2023 at 01:33):

if you want a proper HTTP 302 then deploy the site on Netlify, it's quick. if your website already works on GitHub Pages then migrating to Netlify is a simple job

view this post on Zulip Théo Zimmermann (Oct 10 2023 at 07:34):

Thanks for the suggestions. I plan to raise the question of the licensing today.

view this post on Zulip Théo Zimmermann (Oct 10 2023 at 07:35):

Paolo Giarrusso said:

roughly all of these broke, possibly because of missing redirections:

        <link type="text/css" rel="stylesheet" media="all" href="//coq.inria.fr/modules/node/node.css"/>
        <link type="text/css" rel="stylesheet" media="all" href="//coq.inria.fr/modules/system/defaults.css"/>
        <link type="text/css" rel="stylesheet" media="all" href="//coq.inria.fr/modules/system/system.css"/>
        <link type="text/css" rel="stylesheet" media="all" href="//coq.inria.fr/modules/user/user.css"/>
        <link type="text/css" rel="stylesheet" media="all" href="//coq.inria.fr/sites/all/themes/coq/style.css"/>
        <link type="text/css" rel="stylesheet" media="all" href="//coq.inria.fr/sites/all/themes/coq/coqdoc.css"/>

OK, so in fact, I was still being tricked by the caching mechanism of my browser console, I guess? These links are broken for me too when browsing them directly, but not when I navigate to them by clicking from the webpage source.

view this post on Zulip Paolo Giarrusso (Oct 10 2023 at 17:00):

I'm no webdev unlike @Huỳnh Trần Khanh but I had to shift-reload at some point to get consistent results.

view this post on Zulip Karl Palmskog (Oct 10 2023 at 17:08):

I think what some people do is install another browser with caching turned completely off

view this post on Zulip Théo Zimmermann (Oct 11 2023 at 10:57):

@Huỳnh Trần Khanh The website now has a license (CC-0, like the Coq wiki). If you have suggestions to fix part of the issues that we are encountering since the website migration, your PRs would be very welcome. (We are considering switching to GitLab Pages instead of GitHub Pages to benefit from HTTP redirects, but this won't happen for a while.)


Last updated: May 24 2024 at 22:02 UTC