From 6a2e6d2f6a1aeec7255a4a874dece7f3664bb469 Mon Sep 17 00:00:00 2001 From: Cyril Cohen Date: Thu, 19 Oct 2017 20:40:10 +0200 Subject: new script to create opam meta packages - the opam files in the branch where the script is launched should be correct - if not, the second argument to the script should be a branch in which the opam files are correct --- etc/utils/packager | 74 +++++++++++++++++++++++++++++++++++++++--------------- 1 file changed, 54 insertions(+), 20 deletions(-) diff --git a/etc/utils/packager b/etc/utils/packager index f0c1d5b..af3c777 100755 --- a/etc/utils/packager +++ b/etc/utils/packager @@ -1,28 +1,62 @@ #!/bin/bash +# usage : packager VERSION [BRANCH] +# VERSION is the version number of the package to create, we expect +# there is a tag named mathcomp-$VERSION which archive we can +# download from github +# BRANCH is the name of a branch where we can find accurate local opam +# files. Actually, this may only matter for the Coq version dependencies +# located in the ssreflect package. set -e set -x -for pkg in ssreflect fingroup algebra field solvable character real_closed odd_order -do -pkgdir="$(git root)/opam/extra-dev/packages/coq-mathcomp-$pkg/coq-mathcomp-$pkg.dev" -mkdir -p $pkgdir -cp $(git root)/mathcomp/$pkg/opam $pkgdir/opam -cp $(git root)/mathcomp/$pkg/descr $pkgdir/descr -sed -r "/^(build|install)/s?make?make \"-C\" \"mathcomp/$pkg\"?" -i $pkgdir/opam -echo "git: \"https://github.com/math-comp/math-comp.git\"" > $pkgdir/url -done +if [ -z $2 ] +then BRANCH="mathcomp-$1" +else BRANCH=$2 +fi +# shows $BRANCH for debugging, fails if the branch does not exist +git show $BRANCH -for pkg in ssreflect fingroup algebra field solvable character odd_order -do -pkgdir="$(git root)/opam/released/packages/coq-mathcomp-$pkg/coq-mathcomp-$pkg.1.6" -mkdir -p $pkgdir -cp $(git root)/mathcomp/$pkg/opam $pkgdir/opam -cp $(git root)/mathcomp/$pkg/descr $pkgdir/descr -sed -r "/^version/s?dev?1.6?" -i $pkgdir/opam -sed -r "/^depends.*coq-mathcomp.*/s?dev?1.6?" -i $pkgdir/opam -sed -r "/^(build|install)/s?make?make \"-C\" \"mathcomp/$pkg\"?" -i $pkgdir/opam -echo "http: \"http://github.com/math-comp/math-comp/archive/mathcomp-1.6.tar.gz\"" > $pkgdir/url -echo "checksum: \"038ba80c0d6b430428726ae4d00affcf\"" >> $pkgdir/url +# we build the url file content and the list of packages, and where to put them +if [ $1 == "dev" ] +then +# variables useful for package construction + URLLINE="git: \"https://github.com/math-comp/math-comp.git\"" + PKGS=$(sed -r "s/.*mathcomp\.([^\.]*)*.*/\1/" $(git root)/mathcomp/all/all.v \ + | paste -sd " " -) + PKGPREFIX="$(git root)/opam/extra-dev/packages" +else + ARCHIVE=$(mktemp) + wget -O $ARCHIVE "http://github.com/math-comp/math-comp/archive/mathcomp-$1.tar.gz" + SUM=$(md5sum $ARCHIVE | cut -d " " -f 1) + EXTRACTED=$(mktemp -d) + tar -C $EXTRACTED -zxvf $ARCHIVE +# variables useful for package construction + URLLINE="http: \"http://github.com/math-comp/math-comp/archive/mathcomp-$1.tar.gz\"" + CHECKSUMLINE="checksum: \"$SUM\"" + PKGS=$(ls -fs -d -1 $EXTRACTED/*/mathcomp/*/ \ + | sed -r "s?.*mathcomp/([^/]+)/?\1?" \ + | paste -sd " " -) + PKGPREFIX="$(git root)/opam/released/packages" +fi +# for each package, we pick the corresponding opam and descr file and +# rewrite them to adapt them to single package construction and +# version numbers +for pkg in $PKGS +do pkgdir="$PKGPREFIX/coq-mathcomp-$pkg/coq-mathcomp-$pkg.$1" + mkdir -p $pkgdir + if [ $1 == "dev" ] + then cp $(git root)/mathcomp/$pkg/opam $pkgdir/opam + cp $(git root)/mathcomp/$pkg/descr $pkgdir/descr + else git show "$BRANCH:mathcomp/$pkg/opam" > $pkgdir/opam + git show "$BRANCH:mathcomp/$pkg/descr" > $pkgdir/descr + sed -r "/^version/s?dev?$1?" -i $pkgdir/opam + sed -r "/^depends.*coq-mathcomp.*/s?dev?$1?" -i $pkgdir/opam + fi + sed -r "/^(build|install)/s?make?make \"-C\" \"mathcomp/$pkg\"?" -i $pkgdir/opam + echo $URLLINE > $pkgdir/url + if [ $1 != "dev" ] + then echo $CHECKSUMLINE >> $pkgdir/url + fi done -- cgit v1.2.3 From 0d6e09de16de8a349dafe570ef9f87377630c6a3 Mon Sep 17 00:00:00 2001 From: Cyril Cohen Date: Thu, 19 Oct 2017 20:50:24 +0200 Subject: fix coq version --- mathcomp/ssreflect/opam | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/mathcomp/ssreflect/opam b/mathcomp/ssreflect/opam index 398d385..440dc08 100644 --- a/mathcomp/ssreflect/opam +++ b/mathcomp/ssreflect/opam @@ -10,7 +10,7 @@ license: "CeCILL-B" build: [ make "-j" "%{jobs}%" ] install: [ make "install" ] remove: [ "sh" "-c" "rm -rf '%{lib}%/coq/user-contrib/mathcomp'" ] -depends: [ "coq" { ((>= "8.4pl4" & < "8.5~") | (>= "8.5" & < "8.8~") | (= "dev"))} ] +depends: [ "coq" { ((>= "8.4pl4" & < "8.8~") | (= "dev"))} ] tags: [ "keyword:small scale reflection" "keyword:mathematical components" "keyword:odd order theorem" ] authors: [ "Jeremy Avigad <>" "Andrea Asperti <>" "Stephane Le Roux <>" "Yves Bertot <>" "Laurence Rideau <>" "Enrico Tassi <>" "Ioana Pasca <>" "Georges Gonthier <>" "Sidi Ould Biha <>" "Cyril Cohen <>" "Francois Garillot <>" "Alexey Solovyev <>" "Russell O'Connor <>" "Laurent Théry <>" "Assia Mahboubi <>" ] -- cgit v1.2.3 From 42da1892c314e8faa545ce4657ec8633501eccd7 Mon Sep 17 00:00:00 2001 From: Cyril Cohen Date: Thu, 19 Oct 2017 22:17:14 +0200 Subject: fixed homepage --- mathcomp/algebra/opam | 2 +- mathcomp/character/opam | 2 +- mathcomp/field/opam | 2 +- mathcomp/fingroup/opam | 2 +- mathcomp/odd_order/opam | 2 +- mathcomp/real_closed/opam | 2 +- mathcomp/solvable/opam | 2 +- mathcomp/ssreflect/opam | 2 +- 8 files changed, 8 insertions(+), 8 deletions(-) diff --git a/mathcomp/algebra/opam b/mathcomp/algebra/opam index a94d17b..59dd47d 100644 --- a/mathcomp/algebra/opam +++ b/mathcomp/algebra/opam @@ -3,7 +3,7 @@ name: "coq-mathcomp-algebra" version: "dev" maintainer: "Mathematical Components " -homepage: "http://ssr.msr-inria.inria.fr/" +homepage: "http://math-comp.github.io/math-comp/" bug-reports: "Mathematical Components " license: "CeCILL-B" diff --git a/mathcomp/character/opam b/mathcomp/character/opam index e7dd3fb..3c94411 100644 --- a/mathcomp/character/opam +++ b/mathcomp/character/opam @@ -3,7 +3,7 @@ name: "coq-mathcomp-character" version: "dev" maintainer: "Mathematical Components " -homepage: "http://ssr.msr-inria.inria.fr/" +homepage: "http://math-comp.github.io/math-comp/" bug-reports: "Mathematical Components " license: "CeCILL-B" diff --git a/mathcomp/field/opam b/mathcomp/field/opam index 912eded..cd09358 100644 --- a/mathcomp/field/opam +++ b/mathcomp/field/opam @@ -3,7 +3,7 @@ name: "coq-mathcomp-field" version: "dev" maintainer: "Mathematical Components " -homepage: "http://ssr.msr-inria.inria.fr/" +homepage: "http://math-comp.github.io/math-comp/" bug-reports: "Mathematical Components " license: "CeCILL-B" diff --git a/mathcomp/fingroup/opam b/mathcomp/fingroup/opam index d378e83..a651a0e 100644 --- a/mathcomp/fingroup/opam +++ b/mathcomp/fingroup/opam @@ -3,7 +3,7 @@ name: "coq-mathcomp-fingroup" version: "dev" maintainer: "Mathematical Components " -homepage: "http://ssr.msr-inria.inria.fr/" +homepage: "http://math-comp.github.io/math-comp/" bug-reports: "Mathematical Components " license: "CeCILL-B" diff --git a/mathcomp/odd_order/opam b/mathcomp/odd_order/opam index 5150001..f745e77 100644 --- a/mathcomp/odd_order/opam +++ b/mathcomp/odd_order/opam @@ -3,7 +3,7 @@ name: "coq-mathcomp-odd_order" version: "dev" maintainer: "Mathematical Components " -homepage: "http://ssr.msr-inria.inria.fr/" +homepage: "http://math-comp.github.io/math-comp/" bug-reports: "Mathematical Components " license: "CeCILL-B" diff --git a/mathcomp/real_closed/opam b/mathcomp/real_closed/opam index d06f2e7..52d18b2 100644 --- a/mathcomp/real_closed/opam +++ b/mathcomp/real_closed/opam @@ -3,7 +3,7 @@ name: "coq-mathcomp-real_closed" version: "dev" maintainer: "Mathematical Components " -homepage: "http://ssr.msr-inria.inria.fr/" +homepage: "http://math-comp.github.io/math-comp/" bug-reports: "Mathematical Components " license: "CeCILL-B" diff --git a/mathcomp/solvable/opam b/mathcomp/solvable/opam index 3e8537c..d978d1c 100644 --- a/mathcomp/solvable/opam +++ b/mathcomp/solvable/opam @@ -3,7 +3,7 @@ name: "coq-mathcomp-solvable" version: "dev" maintainer: "Mathematical Components " -homepage: "http://ssr.msr-inria.inria.fr/" +homepage: "http://math-comp.github.io/math-comp/" bug-reports: "Mathematical Components " license: "CeCILL-B" diff --git a/mathcomp/ssreflect/opam b/mathcomp/ssreflect/opam index 440dc08..7e1b09c 100644 --- a/mathcomp/ssreflect/opam +++ b/mathcomp/ssreflect/opam @@ -3,7 +3,7 @@ name: "coq-mathcomp-ssreflect" version: "dev" maintainer: "Mathematical Components " -homepage: "http://ssr.msr-inria.inria.fr/" +homepage: "http://math-comp.github.io/math-comp/" bug-reports: "Mathematical Components " license: "CeCILL-B" -- cgit v1.2.3 From 7d28da695934872303302799c7779c600f981da5 Mon Sep 17 00:00:00 2001 From: Cyril Cohen Date: Fri, 20 Oct 2017 02:00:05 +0200 Subject: improved package generator --- etc/utils/packager | 61 ++++++++++++++++++++++++++++++++++++------------------ 1 file changed, 41 insertions(+), 20 deletions(-) diff --git a/etc/utils/packager b/etc/utils/packager index af3c777..daee789 100755 --- a/etc/utils/packager +++ b/etc/utils/packager @@ -1,24 +1,45 @@ #!/bin/bash -# usage : packager VERSION [BRANCH] -# VERSION is the version number of the package to create, we expect -# there is a tag named mathcomp-$VERSION which archive we can -# download from github -# BRANCH is the name of a branch where we can find accurate local opam -# files. Actually, this may only matter for the Coq version dependencies -# located in the ssreflect package. - set -e set -x +if [ -z $1 ] || [ $1 == "--help" ] || [ $1 == "-h" ] +then cat < $pkgdir/opam git show "$BRANCH:mathcomp/$pkg/descr" > $pkgdir/descr - sed -r "/^version/s?dev?$1?" -i $pkgdir/opam - sed -r "/^depends.*coq-mathcomp.*/s?dev?$1?" -i $pkgdir/opam + sed -r "/^version/s?dev?$VERSION?" -i $pkgdir/opam + sed -r "/^depends.*coq-mathcomp.*/s?dev?$VERSION?" -i $pkgdir/opam fi sed -r "/^(build|install)/s?make?make \"-C\" \"mathcomp/$pkg\"?" -i $pkgdir/opam echo $URLLINE > $pkgdir/url - if [ $1 != "dev" ] + if [ $VERSION != "dev" ] then echo $CHECKSUMLINE >> $pkgdir/url fi done -- cgit v1.2.3 From 33477fadfd9533fac08f888527c7ad3083899af2 Mon Sep 17 00:00:00 2001 From: Cyril Cohen Date: Fri, 20 Oct 2017 02:42:37 +0200 Subject: reproduce github archive locally rather than downloading, much faster --- etc/utils/packager | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) diff --git a/etc/utils/packager b/etc/utils/packager index daee789..d0c4b17 100755 --- a/etc/utils/packager +++ b/etc/utils/packager @@ -48,7 +48,8 @@ then PKGPREFIX="$(git root)/opam/extra-dev/packages" else ARCHIVE=$(mktemp) - wget -O $ARCHIVE $ARCHIVEURL + git archive --format=tgz --output=$ARCHIVE \ + --prefix=math-comp-$TAG/ $TAG # reproduce github archive SUM=$(md5sum $ARCHIVE | cut -d " " -f 1) EXTRACTED=$(mktemp -d) tar -C $EXTRACTED -zxvf $ARCHIVE @@ -81,3 +82,6 @@ do pkgdir="$PKGPREFIX/coq-mathcomp-$pkg/coq-mathcomp-$pkg.$VERSION" then echo $CHECKSUMLINE >> $pkgdir/url fi done + +# finally test the existence of the archive +wget --spider $ARCHIVEURL -- cgit v1.2.3