From 78b4d07568d5df23bd684e4b21ba63e9920debaa Mon Sep 17 00:00:00 2001 From: Cyril Cohen Date: Mon, 8 Apr 2019 17:45:16 +0200 Subject: switching to opam 2.0 format --- coq-mathcomp-algebra.opam | 17 ++++++++++++----- coq-mathcomp-character.opam | 15 ++++++++++----- coq-mathcomp-field.opam | 15 ++++++++++----- coq-mathcomp-fingroup.opam | 15 ++++++++++----- coq-mathcomp-solvable.opam | 15 ++++++++++----- coq-mathcomp-ssreflect.opam | 21 +++++++++++++++------ etc/utils/packager | 21 +++++++++++---------- mathcomp/algebra/descr | 6 ------ mathcomp/character/descr | 4 ---- mathcomp/field/descr | 4 ---- mathcomp/fingroup/descr | 4 ---- mathcomp/solvable/descr | 3 --- mathcomp/ssreflect/descr | 8 -------- 13 files changed, 78 insertions(+), 70 deletions(-) delete mode 100644 mathcomp/algebra/descr delete mode 100644 mathcomp/character/descr delete mode 100644 mathcomp/field/descr delete mode 100644 mathcomp/fingroup/descr delete mode 100644 mathcomp/solvable/descr delete mode 100644 mathcomp/ssreflect/descr diff --git a/coq-mathcomp-algebra.opam b/coq-mathcomp-algebra.opam index 7cc4946..6fa40cc 100644 --- a/coq-mathcomp-algebra.opam +++ b/coq-mathcomp-algebra.opam @@ -1,12 +1,11 @@ -opam-version: "1.2" +opam-version: "2.0" name: "coq-mathcomp-algebra" version: "dev" maintainer: "Mathematical Components " -synopsis: "The Mathematical Components library" -homepage: "https://math-comp.github.io/math-comp/" -bug-reports: "Mathematical Components " -dev-repo: "https://github.com/math-comp/math-comp.git" +homepage: "https://math-comp.github.io/" +bug-reports: "https://github.com/math-comp/math-comp/issues" +dev-repo: "git+https://github.com/math-comp/math-comp.git" license: "CeCILL-B" build: [ make "-C" "mathcomp/algebra" "-j" "%{jobs}%" ] @@ -16,3 +15,11 @@ depends: [ "coq-mathcomp-fingroup" { = "dev" } ] tags: [ "keyword:algebra" "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 <>" ] + +synopsis: "Mathematical Components Library on Algebra" +description: """ +This library contains definitions and theorems about discrete +(i.e. with decidable equality) algebraic structures : ring, fields, +ordered fields, real fields, modules, algebras, integers, rational +numbers, polynomials, matrices, vector spaces... +""" diff --git a/coq-mathcomp-character.opam b/coq-mathcomp-character.opam index 47c72a7..a5eb54b 100644 --- a/coq-mathcomp-character.opam +++ b/coq-mathcomp-character.opam @@ -1,12 +1,11 @@ -opam-version: "1.2" +opam-version: "2.0" name: "coq-mathcomp-character" version: "dev" maintainer: "Mathematical Components " -synopsis: "The Mathematical Components library" -homepage: "https://math-comp.github.io/math-comp/" -bug-reports: "Mathematical Components " -dev-repo: "https://github.com/math-comp/math-comp.git" +homepage: "https://math-comp.github.io/" +bug-reports: "https://github.com/math-comp/math-comp/issues" +dev-repo: "git+https://github.com/math-comp/math-comp.git" license: "CeCILL-B" build: [ make "-C" "mathcomp/character" "-j" "%{jobs}%" ] @@ -16,3 +15,9 @@ depends: [ "coq-mathcomp-field" { = "dev" } ] tags: [ "keyword:algebra" "keyword:character" "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 <>" ] + +synopsis: "Mathematical Components Library on character theory" +description:""" +This library contains definitions and theorems about group +representations, characters and class functions. +""" diff --git a/coq-mathcomp-field.opam b/coq-mathcomp-field.opam index e823f93..a72eeb2 100644 --- a/coq-mathcomp-field.opam +++ b/coq-mathcomp-field.opam @@ -1,12 +1,11 @@ -opam-version: "1.2" +opam-version: "2.0" name: "coq-mathcomp-field" version: "dev" maintainer: "Mathematical Components " -synopsis: "The Mathematical Components library" -homepage: "https://math-comp.github.io/math-comp/" -bug-reports: "Mathematical Components " -dev-repo: "https://github.com/math-comp/math-comp.git" +homepage: "https://math-comp.github.io/" +bug-reports: "https://github.com/math-comp/math-comp/issues" +dev-repo: "git+https://github.com/math-comp/math-comp.git" license: "CeCILL-B" build: [ make "-C" "mathcomp/field" "-j" "%{jobs}%" ] @@ -16,3 +15,9 @@ depends: [ "coq-mathcomp-solvable" { = "dev" } ] tags: [ "keyword:algebra" "keyword:field" "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 <>" ] + +synopsis: "Mathematical Components Library on Fields" +description:""" +This library contains definitions and theorems about field extensions, +galois theory, algebraic numbers, cyclotomic polynomials... +""" diff --git a/coq-mathcomp-fingroup.opam b/coq-mathcomp-fingroup.opam index 57d3a95..2a215d0 100644 --- a/coq-mathcomp-fingroup.opam +++ b/coq-mathcomp-fingroup.opam @@ -1,12 +1,11 @@ -opam-version: "1.2" +opam-version: "2.0" name: "coq-mathcomp-fingroup" version: "dev" maintainer: "Mathematical Components " -synopsis: "The Mathematical Components library" -homepage: "https://math-comp.github.io/math-comp/" -bug-reports: "Mathematical Components " -dev-repo: "https://github.com/math-comp/math-comp.git" +homepage: "https://math-comp.github.io/" +bug-reports: "https://github.com/math-comp/math-comp/issues" +dev-repo: "git+https://github.com/math-comp/math-comp.git" license: "CeCILL-B" build: [ make "-C" "mathcomp/fingroup" "-j" "%{jobs}%" ] @@ -16,3 +15,9 @@ depends: [ "coq-mathcomp-ssreflect" { = "dev" } ] tags: [ "keyword:finite groups" "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 <>" ] + +synopsis: "Mathematical Components Library on finite groups" +description: """ +This library contains definitions and theorems about finite groups, +group quotients, group morphisms, group presentation, group action... +""" diff --git a/coq-mathcomp-solvable.opam b/coq-mathcomp-solvable.opam index f238333..68fcea8 100644 --- a/coq-mathcomp-solvable.opam +++ b/coq-mathcomp-solvable.opam @@ -1,12 +1,11 @@ -opam-version: "1.2" +opam-version: "2.0" name: "coq-mathcomp-solvable" version: "dev" maintainer: "Mathematical Components " -synopsis: "The Mathematical Components library" -homepage: "https://math-comp.github.io/math-comp/" -bug-reports: "Mathematical Components " -dev-repo: "https://github.com/math-comp/math-comp.git" +homepage: "https://math-comp.github.io/" +bug-reports: "https://github.com/math-comp/math-comp/issues" +dev-repo: "git+https://github.com/math-comp/math-comp.git" license: "CeCILL-B" build: [ make "-C" "mathcomp/solvable" "-j" "%{jobs}%" ] @@ -16,3 +15,9 @@ depends: [ "coq-mathcomp-algebra" { = "dev" } ] tags: [ "keyword:finite groups" "keyword:Feit Thompson theorem" "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 <>" ] + +synopsis: "Mathematical Components Library on finite groups (II)" + +description:""" +This library contains more definitions and theorems about finite groups. +""" diff --git a/coq-mathcomp-ssreflect.opam b/coq-mathcomp-ssreflect.opam index a018a3e..8068c6e 100644 --- a/coq-mathcomp-ssreflect.opam +++ b/coq-mathcomp-ssreflect.opam @@ -1,18 +1,27 @@ -opam-version: "1.2" +opam-version: "2.0" name: "coq-mathcomp-ssreflect" version: "dev" maintainer: "Mathematical Components " -synopsis: "The Mathematical Components library" -homepage: "https://math-comp.github.io/math-comp/" -bug-reports: "Mathematical Components " -dev-repo: "https://github.com/math-comp/math-comp.git" +homepage: "https://math-comp.github.io/" +bug-reports: "https://github.com/math-comp/math-comp/issues" +dev-repo: "git+https://github.com/math-comp/math-comp.git" license: "CeCILL-B" build: [ make "-C" "mathcomp/ssreflect" "-j" "%{jobs}%" ] install: [ make "-C" "mathcomp/ssreflect" "install" ] remove: [ "sh" "-c" "rm -rf '%{lib}%/coq/user-contrib/mathcomp'" ] -depends: [ "coq" { ((>= "8.6" & < "8.10~") | (= "dev"))} ] +depends: [ "coq" { ((>= "8.7" & < "8.10~") | (= "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 <>" ] + +synopsis: "Small Scale Reflection" +description: """ +This library includes the small scale reflection proof language +extension and the minimal set of libraries to take advantage of it. +This includes libraries on lists (seq), boolean and boolean +predicates, natural numbers and types with decidable equality, +finite types, finite sets, finite functions, finite graphs, basic arithmetics +and prime numbers, big operators +""" diff --git a/etc/utils/packager b/etc/utils/packager index 34cf3ec..408172c 100755 --- a/etc/utils/packager +++ b/etc/utils/packager @@ -43,7 +43,7 @@ GITROOT=$(git rev-parse --show-toplevel) if [ $VERSION == "dev" ] then # variables useful for package construction - URLLINE="git: \"https://github.com/math-comp/math-comp.git\"" + URLLINE="src: \"git+https://github.com/math-comp/math-comp.git\"" PKGS=$(sed -r "s/.*mathcomp\.([^\.]*)*.*/\1/" $GITROOT/mathcomp/all/all.v \ | paste -sd " " -) PKGPREFIX="$GITROOT/opam/extra-dev/packages" @@ -51,14 +51,14 @@ else ARCHIVE=$(mktemp) git archive --format=tgz --output=$ARCHIVE \ --prefix=math-comp-$TAG/ $TAG # reproduce github archive - SUM=$(md5sum $ARCHIVE | cut -d " " -f 1) + SUM=$(sha256sum $ARCHIVE | cut -d " " -f 1) EXTRACTED=$(mktemp -d) tar -C $EXTRACTED -zxvf $ARCHIVE # variables useful for package construction - URLLINE="http: \"$ARCHIVEURL\"" - CHECKSUMLINE="checksum: \"$SUM\"" - PKGS=$(ls -fs -d -1 $EXTRACTED/*/mathcomp/*/opam \ - | sed -r "s?.*mathcomp/([^/]+)/opam?\1?" \ + URLLINE="src: \"$ARCHIVEURL\"" + CHECKSUMLINE="checksum: \"sha256=$SUM\"" + PKGS=$(ls -fs -d -1 $EXTRACTED/*/*.opam \ + | sed -r "s?.*coq-mathcomp-([^/]+).opam?\1?" \ | paste -sd " " -) PKGPREFIX="$GITROOT/opam/released/packages" fi @@ -71,16 +71,17 @@ do pkgdir="$PKGPREFIX/coq-mathcomp-$pkg/coq-mathcomp-$pkg.$VERSION" mkdir -p $pkgdir if [ $VERSION == "dev" ] then cp $GITROOT/coq-mathcomp-$pkg.opam $pkgdir/opam - cp $GITROOT/mathcomp/$pkg/descr $pkgdir/descr else git show "$BRANCH:coq-mathcomp-$pkg.opam" > $pkgdir/opam - git show "$BRANCH:mathcomp/$pkg/descr" > $pkgdir/descr sed -r "/^version/s?dev?$VERSION?" -i $pkgdir/opam sed -r "/^depends.*coq-mathcomp.*/s?dev?$VERSION?" -i $pkgdir/opam fi - echo $URLLINE > $pkgdir/url + echo "" >> $pkgdir/opam + echo "url {" >> $pkgdir/opam + echo $URLLINE >> $pkgdir/opam if [ $VERSION != "dev" ] - then echo $CHECKSUMLINE >> $pkgdir/url + then echo $CHECKSUMLINE >> $pkgdir/opam fi + echo "}" >> $pkgdir/opam done # finally test the existence of the archive diff --git a/mathcomp/algebra/descr b/mathcomp/algebra/descr deleted file mode 100644 index cab419f..0000000 --- a/mathcomp/algebra/descr +++ /dev/null @@ -1,6 +0,0 @@ -Mathematical Components Library on Algebra - -This library contains definitions and theorems about discrete -(i.e. with decidable equality) algebraic structures : ring, fields, -ordered fields, real fields, modules, algebras, integers, rational -numbers, polynomials, matrices, vector spaces... \ No newline at end of file diff --git a/mathcomp/character/descr b/mathcomp/character/descr deleted file mode 100644 index e7400ea..0000000 --- a/mathcomp/character/descr +++ /dev/null @@ -1,4 +0,0 @@ -Mathematical Components Library on character theory - -This library contains definitions and theorems about group -representations, characters and class functions. \ No newline at end of file diff --git a/mathcomp/field/descr b/mathcomp/field/descr deleted file mode 100644 index ca46f64..0000000 --- a/mathcomp/field/descr +++ /dev/null @@ -1,4 +0,0 @@ -Mathematical Components Library on Fields - -This library contains definitions and theorems about field extensions, -galois theory, algebraic numbers, cyclotomic polynomials... \ No newline at end of file diff --git a/mathcomp/fingroup/descr b/mathcomp/fingroup/descr deleted file mode 100644 index 1917e3c..0000000 --- a/mathcomp/fingroup/descr +++ /dev/null @@ -1,4 +0,0 @@ -Mathematical Components Library on finite groups - -This library contains definitions and theorems about finite groups, -group quotients, group morphisms, group presentation, group action... \ No newline at end of file diff --git a/mathcomp/solvable/descr b/mathcomp/solvable/descr deleted file mode 100644 index e9791a8..0000000 --- a/mathcomp/solvable/descr +++ /dev/null @@ -1,3 +0,0 @@ -Mathematical Components Library on finite groups (II) - -This library contains more definitions and theorems about finite groups. \ No newline at end of file diff --git a/mathcomp/ssreflect/descr b/mathcomp/ssreflect/descr deleted file mode 100644 index f3aeba5..0000000 --- a/mathcomp/ssreflect/descr +++ /dev/null @@ -1,8 +0,0 @@ -Small Scale Reflection - -This library includes the small scale reflection proof language -extension and the minimal set of libraries to take advantage of it. -This includes libraries on lists (seq), boolean and boolean -predicates, natural numbers and types with decidable equality, -finite types, finite sets, finite functions, finite graphs, basic arithmetics -and prime numbers, big operators -- cgit v1.2.3