opam
opam copied to clipboard
coq
Disappearing sources of packages when Inria gforge is shut down end 2020
Inria recently announced that they will shut down gforge project hosting by the end of 2020. Everyone who uses gforge will have to take manual action to migrate their repositories elsewhere, since hosted files will simply disappear.
Quite a few packages in the archive will be affected by this, a full list can be obtained by running the following command in the root:
grep -uri "gforge" .
However, the number of projects affected are far fewer, and can be obtained with the following command (thanks @CohenCyril):
grep -uri "gforge" . | cut -d/ -f4 | sort -u
The output list is currently as follows:
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
coq-vst
We should try to work with the authors of these packages to make sure (1) that all files related to the projects and packages are preserved and (2) if necessary, projects become hosted permanently elsewhere.
Hi. The sources of coq-color are on https://github.com/fblanqui/color/ for some time now. However, the targz are on gforge. I will try to move them to github as well by the end of the year.
CC @thery (coq-prime and coq-high-school-geometry), @herbelin (coq-high-school-geometry), @mattam82 (coq-equations-fpred), @fajb (coq-ppsimpl),
Hi @CohenCyril, thanks for your message. The sources of coq-high-school-geometry have moved on https://github.com/coq-contribs/high-school-geometry for some time now (though, unfortunately, I renounced to adapt high-school-geometry to Coq 8.7: the IZR change in the representation of real constants was too difficult to manage).
Note that the coqprime dev sources live at https://github.com/thery/coqprime, so it should be possible to migrate the 8.5b tag to there, and to change the bugtracker and homepage links to the GitHub ones
What is the difference between https://github.com/thery/coqprime and https://gitlab.inria.fr/thery/coqprime? They both have relatively recent commits.
github is the current development. gitlab.inria.fr is just a reaction to the announcement that gforge is going down, so it is a frozen copy of the old version of the development that was on gforge.
@thery could you please advertise this in the readme of each repo, each one pointing to the other, and the frozen copy being flaged as such within <h1> tags, so as to make it obvious at first sight?
Subsidiary question: have the two repos diverged so much that they are irreconcilable? Could we have a simple automatic hook synchronizing them with github, so that inria's one is simply a mirror?
@thery could you please advertise this in the readme of each repo,
this is done in https://thery.gitlabpages.inria.fr/coqprime/ and https://github.com/thery/coqprime/blob/master/README.md.
Subsidiary question: have the two repos diverged so much that they are irreconcilable?
this was my initial mistake. Some one asked me to put a copy of coqprime on github and I did not do the transfer at that time. Now I don't recollect if I've manually transfered some commits and I don't feel comfortable enough with git to reconnect the pieces of the jigsaw, sorry.
The gitlab repo is missing tags for the files available at https://gforge.inria.fr/frs/?group_id=163 (in particular, there's a link to https://gforge.inria.fr/frs/download.php/file/35520/coqprime_8.5b.zip for coqprime.1.0.0 in
$ git grep -i gforge | grep coqprime
extra-dev/packages/coq-coqprime/coq-coqprime.dev/opam:homepage: "http://coqprime.gforge.inria.fr/"
extra-dev/packages/coq-coqprime/coq-coqprime.dev/opam:bug-reports: "http://coqprime.gforge.inria.fr/"
released/packages/coq-coqprime/coq-coqprime.1.0.0/opam:homepage: "http://coqprime.gforge.inria.fr/"
released/packages/coq-coqprime/coq-coqprime.1.0.0/opam:bug-reports: "https://gforge.inria.fr/tracker/?func=add&group_id=163&atid=733"
released/packages/coq-coqprime/coq-coqprime.1.0.0/opam: "https://gforge.inria.fr/frs/download.php/file/35520/coqprime_8.5b.zip"
released/packages/coq-coqprime/coq-coqprime.1.0.1/opam:homepage: "http://coqprime.gforge.inria.fr/"
released/packages/coq-coqprime/coq-coqprime.1.0.1/opam:bug-reports: "https://gforge.inria.fr/tracker/?func=add&group_id=163&atid=733"
released/packages/coq-coqprime/coq-coqprime.1.0.2/opam:homepage: "http://coqprime.gforge.inria.fr/"
released/packages/coq-coqprime/coq-coqprime.1.0.2/opam:bug-reports: "http://coqprime.gforge.inria.fr/"
released/packages/coq-coqprime/coq-coqprime.1.0.3/opam:homepage: "http://coqprime.gforge.inria.fr/"
released/packages/coq-coqprime/coq-coqprime.1.0.3/opam:bug-reports: "http://coqprime.gforge.inria.fr/"
released/packages/coq-coqprime/coq-coqprime.1.0.4/opam:homepage: "http://coqprime.gforge.inria.fr/"
released/packages/coq-coqprime/coq-coqprime.1.0.4/opam:bug-reports: "http://coqprime.gforge.inria.fr/"
released/packages/coq-coqprime/coq-coqprime.1.0.5/opam:homepage: "http://coqprime.gforge.inria.fr/"
released/packages/coq-coqprime/coq-coqprime.1.0.5/opam:bug-reports: "http://coqprime.gforge.inria.fr/"
)
As far as the repos go, I've pushed the gitlab master branch to https://github.com/JasonGross/coqprime/tree/gitlab/master, and while GitHub informs me that "[t]his branch is 149 commits ahead, 245 commits behind thery:master", when I rebase the GitLab master branch atop the GitHub master branch, the only commits remaining are
commit 18c33a4863e64813e19723eeb6e7ba4476943e3c (HEAD -> gitlab/master-rebased)
Author: THERY Laurent <[email protected]>
Date: Mon Jul 27 12:11:01 2020 +0200
Add .gitlab-ci.yml
commit 5d7e17aa219a83e0c5df36d2715947c09045728d
Author: thery <[email protected]>
Date: Mon Jul 27 12:09:33 2020 +0200
add html
There are a number of commits on the GitHub master branch that did not make it to the GitLab master branch. So I think it's safe to get rid of the GitLab one (though you may wish to make tags for the old versions?).
Btw, if you want to get the GitLab version on GitHub, you can run these commands:
git clone [email protected]:thery/coqprime.git coqprime-temp
cd coqprime-temp
git remote add gitlab https://gitlab.inria.fr/thery/coqprime.git
git remote update
git checkout -b gforge/master gitlab/master
git push origin gforge/master
git push origin --tags
This will not get rid of any history on the GitHub repo, but will just add a new branch gforge/master with the history from GitLab. But, again, probably not necessary, given that rebasing shows that only two commits are missing.
@JasonGross Thanks. My memory was wrong : github/coqprime contains all the history. For the tags in gitlab, I didn't find how to transfer them automatically from svn. So I have just added them to : https://gitlab.inria.fr/thery/coqprime/-/releases. Maybe we should just add them to github but I don't know how to do this
Maybe we should just add them to github but I don't know how to do this
If you go to https://github.com/thery/coqprime/releases/new you can select a particular commit to target the release at. Alternatively, in your local clone of the repo, you can run git tag -s <tagname> <commit sha1> (possibly adding -m <msg>), and then running git push origin --tags to propagate them from your clone to github.
Ok I have created a release with the old versions of coqprime and remove all the references to gforge in the opam archive: #1407
Inria is launching an "impact assessment" of the closure of the gforge (see the internal link: https://intranet.inria.fr/Actualite/Nouvelles-concernant-l-arret-de-la-gforge). To contribute, we can open a ticket on their Helpdesk service. There's also an e-mail address: [email protected]. I don't plan on writing myself, but if @palmskog or someone else wish to prepare something, I can certainly forward to this Helpdesk.
@fajb @vbgl the only package on the Coq opam archive using gforge that we have no confirmation about is ppsimpl. Even though the package may have been obsoleted by zify in recent Coq, there are still projects that depend on ppsimpl.
So, could you please move the repo (https://scm.gforge.inria.fr/anonscm/git/ppsimpl/ppsimpl.git) to a new canonical location, such as GitHub?
We now have confirmation from all relevant projects that they will move or have already moved to a new location. Let's follow up in late November again for final checkup.
