Karl Palmskog (Jun 13 2020 at 03:28): Karl Palmskog (Jun 13 2020 at 03:28):Got an email about Inria's gforge getting shut down later this year. Currently, this will mean a mass death of Coq packages and their documentation, e.g., grepping in the released OPAM repo for gforge gives 119 hits, most of which are download URLs. Is it going to be up the community to deal with this issue, or is there any centrally planned solution?
Enrico Tassi (Jun 13 2020 at 08:49):Would you mind posting the list of affected packages? Also, I'm pretty sure at some point we were caching the tarballs (opam admin does that) so it should not stop working (unless we stopped caching)
Karl Palmskog (Jun 13 2020 at 09:36):no caching as far as I can see https://coq.inria.fr/opam/ --- I will post the list in an OPAM archive GitHub issue later today
Karl Palmskog (Jun 13 2020 at 14:43):we already have a new package submitted that lives on gforge, see https://github.com/coq/opam-coq-archive/pull/1297
I'm really on the fence whether new packages hosted at gforge should be allowed, with only 6 months to being killed off.
Enrico Tassi (Jun 13 2020 at 16:05):If we enable caching in opam admin, then I don't see a problem.
Théo Zimmermann (Jun 13 2020 at 16:07):From the e-mail, it is clear that there won't be any automated nor systematic migration.
Théo Zimmermann (Jun 13 2020 at 16:09):Caching sounds like a very good idea given that even if projects are migrated, people might forget to migrate and/or update some old releases.
Théo Zimmermann (Jun 13 2020 at 16:12):@Enrico Tassi if you don't have access to the server and know precisely what commands to run to activate caching, let me know.
Cyril Cohen (Jun 13 2020 at 16:14):I think this gforge enf-of-life without automated migration plan is not nice and should be escalated back to Inria
Karl Palmskog (Jun 13 2020 at 16:15):Enrico Tassi said:
If we enable caching in opam admin, then I don't see a problem.
I definitely see a problem, since we expect people to be able to consume packages via JSON and not just opam. I view caching as very different from the dedicated replication of tarballs I proposed in https://github.com/coq/opam-coq-archive/issues/1181
Enrico Tassi (Jun 13 2020 at 16:51):Indeed the caching would work out of the box for opam only but the tarballs could also be used by other tools. I suggested caching because it is transparent for the users (also of old versions). About recommending the package submitter to change hosting, I'm all in. About requiring a non-forge URL, I believe it's a bit too much since migrating your project may require time (and there may no be easy way to migrate old tarballs without also updating opam files).
The doc is here: https://opam.ocaml.org/doc/Manual.html I don't know exactly how it works (since opam 2) but I expect that if a url does not work and the repo file declares the cache, the opam client also looks there.
Enrico Tassi (Jun 13 2020 at 16:53):Apparently one has to run (systematically in the cronjob) opam admin cache and write something in /repo.
Enrico Tassi (Jun 13 2020 at 16:54):I won't be able to work on this for two weeks I'm afraid :-/
Karl Palmskog (Jun 13 2020 at 16:57):OK I will summarize all this (the facts about caching etc.) in the planned GitHub issue
Enrico Tassi (Jun 13 2020 at 16:59):But there is one problem with caching now that I think about it. At some point the website was moved from an artisanal crontab running git pull & make on the real server to something else. The migration was performed by @Vincent Laporte and @Maxime Dénès IIRC and at that point in time the cache was disabled (I believe there is a commit with the tarballs we had, but after that caching was off). I don't recall why, but I suspect we now host the site on some "space constrained" machine. Maxime or Vincent, could you please remind me how it works today? Can we enable caching to avoid breakage caused by the death of the forge?
Cyril Cohen (Jun 13 2020 at 17:08):@Karl Palmskog I found only 6 released packages:
$ grep -uri "gforge" released/**/opam | grep "src" | cut -d/ -f3 | sort -u
coq-coquelicot
coq-flocq
coq-gappa
coq-interval
coq-ppsimpl
coq-tlc
And in total mentionning gforge anywhere (homepage, dev-repo, src), 12, including coq...
$ grep -uri "gforge" . | cut -d/ -f4 | sort -u
coq
coq-color
coq-coqide
coq-coqprime
coq-coquelicot
coq-equations-fpred
coq-flocq
coq-gappa
coq-high-school-geometry
coq-interval
coq-ppsimpl
coq-tlc
each of those has many package versions, though
Cyril Cohen (Jun 13 2020 at 17:12):Karl Palmskog said:
each of those has many package versions, though
sure
Cyril Cohen (Jun 13 2020 at 17:14):I'd say Guillaume Melquind is responsible for many of the active packages listed above, and will port the source and all the releases anyway (that takes coquelicot, flocq, gappa and interval out)
Cyril Cohen (Jun 13 2020 at 17:17):For coq and coqide it's just a wrong dev-repo:
grep -ur "gforge" . | grep -e "packages/coq\(-coqide\|\)/"
./extra-dev/packages/coq-coqide/coq-coqide.8.6~beta1/opam:dev-repo: "git+https://scm.gforge.inria.fr/anonscm/git/coq/coq.git"
./core-dev/packages/coq/coq.8.7+beta2/opam:dev-repo: "git+https://scm.gforge.inria.fr/anonscm/git/coq/coq.git"
./core-dev/packages/coq/coq.8.7+beta1/opam:dev-repo: "git+https://scm.gforge.inria.fr/anonscm/git/coq/coq.git"
./core-dev/packages/coq/coq.8.6~beta1/opam:dev-repo: "git+https://scm.gforge.inria.fr/anonscm/git/coq/coq.git"
I guess it makes sense to notify the mainatainers of these packages. It may be the case that the cache thing is not needed. But if they don't react quickly the cache is the only thing I can think of.
Cyril Cohen (Jun 13 2020 at 17:26):Here is the list of potential maintainers for the problematic packages (i.e. the previous list, minus coq and coq-ide)
$ for p in $(cat packages); do grep -ur maintainer . | grep /$p/ | cut -d/ -f 4,6 | sort -u ; done
coq-color/opam:maintainer: "frederic.blanqui@inria.fr"
coq-color/opam:maintainer: "Matej Košík <matej.kosik@inria.fr>"
coq-coqprime/opam:maintainer: "thery@sophia.inria.fr"
coq-coquelicot/opam:maintainer: "guillaume.melquiond@inria.fr"
coq-coquelicot/opam:maintainer: "Matej Košík <matej.kosik@inria.fr>"
coq-equations-fpred/opam:maintainer: "matthieu.sozeau@inria.fr"
coq-flocq/opam:maintainer: "guillaume.melquiond@inria.fr"
coq-gappa/opam:maintainer: "guillaume.melquiond@inria.fr"
coq-high-school-geometry/opam:maintainer: "Hugo.Herbelin@inria.fr"
coq-high-school-geometry/opam:maintainer: "thery@sophia.inria.fr"
coq-interval/opam:maintainer: "guillaume.melquiond@inria.fr"
coq-ppsimpl/opam:maintainer: "frederic.besson@inria.fr"
coq-tlc/opam:maintainer: "arthur.chargueraud@inria.fr"
coq-tlc/opam:maintainer: "francois.pottier@inria.fr"
I think most of these people are reachable...
Maxime Dénès (Jun 13 2020 at 17:31):@Enrico Tassi I don't think we are space constrained so much
Maxime Dénès (Jun 13 2020 at 17:32):the only known problem of our current setup is that I pay the server from my pocket
Enrico Tassi (Jun 13 2020 at 17:36):Then I guess we can keep an exceptional run of opam admin cache + edit of /repo as plan B and someone takes care to notify the people above ASAP
Maxime Dénès (Jun 13 2020 at 17:53):Btw, it would be nice to advise this people to not migrate to the Inria gitlab, contrarily to what the internal message was saying.
Karl Palmskog (Jun 14 2020 at 14:27):posted issue now, let's continue there: https://github.com/coq/opam-coq-archive/issues/1298
Last updated: Dec 05 2023 at 04:01 UTC