Maxime Dénès (Sep 13 2023 at 06:16): 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!
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.
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/
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
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
Karl Palmskog (Sep 13 2023 at 20:22):also it will block Docker image of 8.18.0
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
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.
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
Maxime Dénès (Sep 15 2023 at 16:16):Ok, I found the cause, fixing
Maxime Dénès (Sep 15 2023 at 16:18):Should be better now! @Karl Palmskog
Thanks for reporting!
Karl Palmskog (Sep 15 2023 at 16:24):thanks, I can confirm the key 8.18 packages are now out on released opam repo
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.
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/
Théo Zimmermann (Oct 02 2023 at 13:02):This was a temporary quirk, but this should be fixed now.
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 :)
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)
Jason Gross (Oct 02 2023 at 21:01):https://coq.inria.fr/stdlib/ is also a 404
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/
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:
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
Théo Zimmermann (Oct 03 2023 at 08:02):If someone opens the PR, I can merge it.
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.
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.
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
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
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
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?
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.
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.
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)
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:
Karl Palmskog (Oct 06 2023 at 08:57):it's going to happen in 80+ years? Mickey Mouse thing...
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"
Paolo Giarrusso (Oct 06 2023 at 09:35):(could grant agencies require that, maybe as part of the open science push?)
Théo Zimmermann (Oct 06 2023 at 09:50):I think some already do, actually.
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).
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:
Théo Zimmermann (Oct 09 2023 at 19:22):But this would require deploying multiple copies of the doc in several places...
Théo Zimmermann (Oct 09 2023 at 19:22):Up to discussion
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.
Paolo Giarrusso (Oct 09 2023 at 19:45):https://coq.inria.fr/modules/node/node.css is broken here?
Paolo Giarrusso (Oct 09 2023 at 19:46):Chrome's web console (from right-click->inspect) shows many 404s:
image.png
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"/>
(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)
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
Huỳnh Trần Khanh (Oct 10 2023 at 01:27):https://lea0.verou.me/2016/11/url-rewriting-with-github-pages/
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
Théo Zimmermann (Oct 10 2023 at 07:34):Thanks for the suggestions. I plan to raise the question of the licensing today.
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.
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.
Karl Palmskog (Oct 10 2023 at 17:08):I think what some people do is install another browser with caching turned completely off
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: Oct 13 2024 at 01:02 UTC