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?

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)

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

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.

If we enable caching in opam admin, then I don't see a problem.

From the e-mail, it is clear that there won't be any automated nor systematic migration.

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.

@Enrico Tassi if you don't have access to the server and know precisely what commands to run to activate caching, let me know.

I think this gforge enf-of-life without automated migration plan is not nice and should be escalated back to Inria

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

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.

Apparently one has to run (systematically in the cronjob) `opam admin cache`

and write something in `/repo`

.

I won't be able to work on this for two weeks I'm afraid :-/

OK I will summarize all this (the facts about caching etc.) in the planned GitHub issue

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?

@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

Karl Palmskog said:

each of those has many package versions, though

sure

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)

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.

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...

@Enrico Tassi I don't think we are space constrained so much

the only known problem of our current setup is that I pay the server from my pocket

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

Btw, it would be nice to advise this people to not migrate to the Inria gitlab, contrarily to what the internal message was saying.

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