Merge pull request #325 from CohenCyril/opam-2.0

switching to opam 2.0 format

13 files changed, 78 insertions, 70 deletions

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 <mathcomp-dev@sympa.inria.fr>"
-synopsis: "The Mathematical Components library"
 
-homepage: "https://math-comp.github.io/math-comp/"
-bug-reports: "Mathematical Components <mathcomp-dev@sympa.inria.fr>"
-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 <mathcomp-dev@sympa.inria.fr>"
-synopsis: "The Mathematical Components library"
 
-homepage: "https://math-comp.github.io/math-comp/"
-bug-reports: "Mathematical Components <mathcomp-dev@sympa.inria.fr>"
-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 <mathcomp-dev@sympa.inria.fr>"
-synopsis: "The Mathematical Components library"
 
-homepage: "https://math-comp.github.io/math-comp/"
-bug-reports: "Mathematical Components <mathcomp-dev@sympa.inria.fr>"
-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 <mathcomp-dev@sympa.inria.fr>"
-synopsis: "The Mathematical Components library"
 
-homepage: "https://math-comp.github.io/math-comp/"
-bug-reports: "Mathematical Components <mathcomp-dev@sympa.inria.fr>"
-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 <mathcomp-dev@sympa.inria.fr>"
-synopsis: "The Mathematical Components library"
 
-homepage: "https://math-comp.github.io/math-comp/"
-bug-reports: "Mathematical Components <mathcomp-dev@sympa.inria.fr>"
-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 <mathcomp-dev@sympa.inria.fr>"
-synopsis: "The Mathematical Components library"
 
-homepage: "https://math-comp.github.io/math-comp/"
-bug-reports: "Mathematical Components <mathcomp-dev@sympa.inria.fr>"
-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