make the opam package meta data

10 files changed, 48 insertions, 2 deletions

diff --git a/etc/utils/packager b/etc/utils/packager
index 5a8138d..fc645cb 100755
--- a/etc/utils/packager
+++ b/etc/utils/packager
@@ -5,9 +5,10 @@ set -x
 
 for pkg in algebra basic field character fingroup odd_order real_closed solvable ssreflect
 do
-pkgdir="$(git root)/extra-dev/packages/coq:mathcomp:$pkg/coq:mathcomp:$pkg.dev"
+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
-done
 
+done
diff --git a/mathcomp/algebra/descr b/mathcomp/algebra/descr
new file mode 100644
index 0000000..cab419f
--- /dev/null
+++ b/mathcomp/algebra/descr
@@ -0,0 +1,6 @@
+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/basic/descr b/mathcomp/basic/descr
new file mode 100644
index 0000000..8bbc61e
--- /dev/null
+++ b/mathcomp/basic/descr
@@ -0,0 +1,5 @@
+Mathematical Components Library, basic restults
+
+This library contains definitions and theorems about finite types,
+finite sets, finite functions, finite graphs, basic arithmetics and
+prime numbers, big operators...
\ No newline at end of file
diff --git a/mathcomp/character/descr b/mathcomp/character/descr
new file mode 100644
index 0000000..e7400ea
--- /dev/null
+++ b/mathcomp/character/descr
@@ -0,0 +1,4 @@
+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
new file mode 100644
index 0000000..ca46f64
--- /dev/null
+++ b/mathcomp/field/descr
@@ -0,0 +1,4 @@
+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
new file mode 100644
index 0000000..1917e3c
--- /dev/null
+++ b/mathcomp/fingroup/descr
@@ -0,0 +1,4 @@
+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/odd_order/descr b/mathcomp/odd_order/descr
new file mode 100644
index 0000000..ee393a9
--- /dev/null
+++ b/mathcomp/odd_order/descr
@@ -0,0 +1,6 @@
+Odd Order Theorem
+
+This library contains the complete formal proof of the Odd Order
+Theorem (aka Feit Thompson Theorem).
+The file stripped_odd_order_theorem.v contains a proof of a self
+contained statement of the odd order.
\ No newline at end of file
diff --git a/mathcomp/real_closed/descr b/mathcomp/real_closed/descr
new file mode 100644
index 0000000..b51ecf9
--- /dev/null
+++ b/mathcomp/real_closed/descr
@@ -0,0 +1,7 @@
+Mathematical Components Library on real closed fields
+
+This library contains definitions and theorems about real closed
+fields, with a construction of the real closure and the algebraic
+closure (including a proof of the fundamental theorem of algebra). It
+also contains a proof of decidability of the first order theory of
+real closed field, through quantifier elimination.
diff --git a/mathcomp/solvable/descr b/mathcomp/solvable/descr
new file mode 100644
index 0000000..e9791a8
--- /dev/null
+++ b/mathcomp/solvable/descr
@@ -0,0 +1,3 @@
+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
new file mode 100644
index 0000000..7621878
--- /dev/null
+++ b/mathcomp/ssreflect/descr
@@ -0,0 +1,6 @@
+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.