search

coq / opam

Archive for all Coq related OPAM packages organized in various repositories
https://coq.inria.fr/opam/www/
GNU Lesser General Public License v2.1
121 stars 162 forks source link

Disappearing sources of packages when Inria gforge is shut down end 2020 #1298

Open palmskog opened 4 years ago

palmskog commented 4 years ago

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.

gares commented 4 years ago

CC @silene @charguer @fblanqui

fblanqui commented 4 years ago

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.

CohenCyril commented 4 years ago

CC @thery (coq-prime and coq-high-school-geometry), @herbelin (coq-high-school-geometry), @mattam82 (coq-equations-fpred), @fajb (coq-ppsimpl),

herbelin commented 4 years ago

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

JasonGross commented 4 years ago

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

thery commented 4 years ago

I moved gforge/coqprime to https://thery.gitlabpages.inria.fr/coqprime/

Zimmi48 commented 4 years ago

What is the difference between https://github.com/thery/coqprime and https://gitlab.inria.fr/thery/coqprime? They both have relatively recent commits.

thery commented 4 years ago

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.

Zimmi48 commented 4 years ago

OK thanks for the explanations.

CohenCyril commented 4 years ago

@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?

CohenCyril commented 4 years ago

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 commented 4 years ago

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

thery commented 4 years ago

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.

JasonGross commented 4 years ago

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 <laurent.thery@inria.fr>
Date:   Mon Jul 27 12:11:01 2020 +0200

    Add .gitlab-ci.yml

commit 5d7e17aa219a83e0c5df36d2715947c09045728d
Author: thery <Laurent.Thery@inria.fr>
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 git@github.com: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.

thery commented 4 years ago

@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

JasonGross commented 4 years ago

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.

thery commented 4 years ago

Ok I have created a release with the old versions of coqprime and remove all the references to gforge in the opam archive: #1407

Zimmi48 commented 4 years ago

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: end-inria-gforge@inria.fr. I don't plan on writing myself, but if @palmskog or someone else wish to prepare something, I can certainly forward to this Helpdesk.

palmskog commented 4 years ago

@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?

palmskog commented 3 years ago

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.

silene commented 3 years ago

The shutdown has been pushed back to summer 2021.