.dockerignore

+*
+# Begin files referenced by symlinks
+!README.md
+!AUTHORS
+!INSTALL.md
+!CeCILL-B
+# End files referenced by symlinks
+!*.opam
+!plugin
+!mathcomp
+
+**/*.d
+**/*.vo
+**/*.vio
+**/*.cm*
+**/*~
+**/*.glob
+**/*.aux
+**/*.a
+**/*.o
+**/*#
+**/Make*.coq
+**/Make*.coq.bak
+**/Make*.coq.conf
+mathcomp/ssreflect/ssreflect.ml4
+mathcomp/ssreflect/ssrmatching.ml4
+mathcomp/ssreflect/ssrmatching.mli
+# mathcomp/ssreflect/ssrmatching.v
+mathcomp/ssreflect/ssreflect_plugin.mllib
+mathcomp/ssreflect/ssreflect_plugin.mlpack
+mathcomp/ssreflect.ml4
+mathcomp/ssrmatching.ml4
+mathcomp/ssrmatching.mli
+mathcomp/ssrmatching.v
+mathcomp/ssreflect_plugin.mllib
+mathcomp/ssreflect_plugin.mlpack

.travis.yml

@@ -15,8 +15,7 @@ addons:
 env:
   global:
   - NJOBS=2
-  # system is == 4.02.3
-  - COMPILER="system"
+  - COMPILER="4.05.0"
   # Main test targets
   matrix:
   - TEST_TARGET="v8.6"

CHANGELOG.md

+# Changelog
+All notable changes to this project will be documented in this file.
+
+Last releases: [[1.9.0] - 2019-05-22](#190---2019-05-22) and [[1.8.0] - 2019-04-08](#180---2019-04-08).
+
+The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.0.0/).
+
+## [1.9.0] - 2019-05-22
+
+MathComp 1.9.0 is compatible with Coq 8.7, 8.8, 8.9 and 8.10beta1.
+Minor releases will remain compatible with Coq 8.9 and 8.10; compatibility with earlier
+versions may be dropped.
+
+### Added
+
+- `nonPropType`, an interface for non-`Prop` types, and `{pred T}` and
+   `relpre f r`, all of which will be in the Coq 8.10 core SSreflect library.
+
+- `deprecate old_id new_id`, notation for `new_id` that prints a deprecation
+  warning for `old_id`; `Import Deprecation.Silent` turns off those warnings,
+  `Import Deprecation.Reject` raises errors instead of only warning.
+
+- `filter_nseq`, `count_nseq`, `mem_nseq`,
+  `rcons_inj`, `rcons_injl`, `rcons_injr`, `nthK`, `sumn_rot`.
+
+- some `perm_eq` lemmas: `perm_cat[lr]`, `perm_nilP`,
+  `perm_consP`, `perm_has`, `perm_flatten`, `perm_sumn`.
+
+- computing (efficiently) (item, multiplicity) tallies of sequences over an
+  `eqType`: `tally s`, `incr_tally bs x`, `bs \is a wf_tally`, `tally_seq bs`.
+
+### Changed
+
+- definition of `PredType` which now takes only a `P -> pred T` function;
+  definition of `simpl_rel` to improve simplification by `inE`. Both these
+  changes will be in the Coq 8.10 SSReflect core library.
+
+- definition of `permutations s` now uses an optimal algorithm (in space _and_
+  time) to generate all permutations of s back-to-front, using `tally s`.
+
+### Renamed
+
+- `perm_eqP` -> `permP` (`seq.permP` if `perm.v` is also imported)
+- `perm_eqlP` -> `permPl`
+- `perm_eqrP` -> `permPr`
+- `perm_eqlE` -> `permEl`
+- `perm_eq_refl` -> `perm_refl`
+- `perm_eq_sym` -> `perm_sym`
+- `perm_eq_trans` -> `perm_trans`
+- `perm_eq_size` -> `perm_size`
+- `perm_eq_mem` -> `perm_mem`
+- `perm_eq_uniq` -> `perm_uniq`
+- `perm_eq_rev` -> `perm_rev`
+- `perm_eq_flatten` -> `perm_flatten`
+- `perm_eq_all` -> `perm_all`
+- `perm_eq_small` -> `perm_small_eq`
+- `perm_eq_nilP` -> `perm_nilP`
+- `perm_eq_consP` -> `perm_consP`
+- `leq_size_perm` -> `uniq_min_size` (permuting conclusions)
+- `perm_uniq` -> `eq_uniq` (permuting assumptions)
+  --> beware `perm_uniq` now means `perm_eq_uniq`
+- `uniq_perm_eq` -> `uniq_perm`
+- `perm_eq_iotaP` -> `perm_iotaP`
+- `perm_undup_count` -> `perm_count_undup`
+- `tuple_perm_eqP` -> `tuple_permP`
+- `eq_big_perm` -> `perm_big`
+- `perm_eq_abelian_type` -> `abelian_type_pgroup`
+
+### Misc
+
+- removed Coq prelude hints `plus_n_O` `plus_n_Sm` `mult_n_O` `mult_n_Sm`,
+  to improve robustness of `by ...`; scripts may need to invoke
+  `addn0`, `addnS`, `muln0` or `mulnS`
+  explicitly where these hints were used accidentally.
+
+## [1.8.0] - 2019-04-08
+
+Drop compatibility with Coq 8.6 (OCaml plugin removed).
+MathComp 1.8.0 is compatible with Coq 8.7, 8.8 and 8.9.
+
+### Added
+
+- Companion matrix of a polynomial `companionmx p` and the
+  theorems: `companionmxK`, `map_mx_companion` and `companion_map_poly`
+
+- `homoW_in`, `inj_homo_in`, `mono_inj_in`, `anti_mono_in`,
+  `total_homo_mono_in`, `homoW`, `inj_homo`, `monoj`, `anti_mono`,
+  `total_homo_mono`
+
+- `sorted_lt_nth`, `ltn_index`, `sorted_le_nth`, `leq_index`.
+
+- `[arg minr_( i < n | P ) F]` and `[arg maxr_( i < n | P ) F]`
+  with all their variants, following the same convention as for `nat`
+
+- `contra_neqN`, `contra_neqF`, `contra_neqT`, `contra_neq_eq`, `contra_eq_neq`
+
+- `take_subseq`, `drop_subseq`
+
+- `big_imset_cond`,`big_map_id`, `big_image_cond`
+  `big_image`, `big_image_cond_id` and `big_image_id`
+
+- `foldrE`, `foldlE`, `foldl_idx` and `sumnE`
+  to turn "seq statements" into "bigop statements"
+
+- `all_iff` with notation `[<-> P0; P1; ..; Pn]` to talk about
+  circular implication `P0 -> P1 -> ... -> Pn -> P0`.
+  Related theorems are `all_iffLR` and `all_iffP`
+
+- support for casts in map comprehension notations, e.g.,
+  `[seq E : T | s <- s]`.
+
+- a predicate `all2`, a parallel double `seq` version of `all`.
+
+- some `perm_eq` lemmas: `perm_cat[lr]`, `perm_eq_nilP`,
+  `perm_eq_consP`, `perm_eq_flatten`.
+
+- a function `permutations` that computes a duplicate-free list
+  of all permutations of a given sequence `s` over an `eqType`, along
+  with its theory: `mem_permutations`, `size_permutations`,
+  `permutations_uniq`, `permutations_all_uniq`, `perm_permutations`.
+
+### Changed
+
+- Theory of `lersif` and intervals:
+  + Many `lersif` related lemmas are ported from `ssrnum`
+  + Changed: `prev_of_itv`, `itv_decompose`, and `itv_rewrite`
+  + New theory of intersections of intervals
+
+- Generalized `extremum_spec` and its theory, added `extremum` and
+  `extremumP`, generalizing `arg_min` for an arbitrary `eqType` with an
+  order relation on it (rather than `nat`). Redefined `arg_min` and
+  `arg_max` with it.
+
+- Reshuffled theorems inside files and packages:
+  + `countalg` goes from the field to the algebra package
+  + `finalg` inherits from countalg
+  + `closed_field` contains the construction of algebraic closure
+    for countable fields that used to be in the file `countalg`.
+
+- Maximal implicits applied to reflection, injectivity and cancellation
+  lemmas so that they are easier to pass to combinator lemmas such as
+  `sameP`, `inj_eq` or `canLR`.
+
+- Added `reindex_inj s` shorthand for reindexing a bigop with a
+  permutation `s`.
+
+- Added lemma `eqmxMunitP`: two matrices with the same shape
+  represent the same subspace iff they differ only by a change of
+  basis.
+
+- Corrected implicits and documentation of `MatrixGenField`.
+
+- Rewritten proof of quantifier elimination for closed field in a
+  monadic style.
+
+- Specialized `bool_irrelevance` so that the statement reflects
+  the name.
+
+- Changed the shape of the type of `FieldMixin` to allow one-line
+  in-proof definition of bespoke `fieldType` structure.
+
+- Refactored and extended Arguments directives to provide more
+  comprehensive signature information.
+
+- Generalized the notation `[seq E | i <- s, j <- t]` to the case
+  where `t` may depend on `i`. The notation is now primitive and
+  expressed using `flatten` and `map` (see documentation of seq).
+  `allpairs` now expands to this notation when fully applied.
+  + Added `allpairs_dep` and made it self-expanding as well.
+  + Generalized some lemmas in a backward compatible way.
+  + Some strictly more general lemmas now have suffix `_dep`.
+  + Replaced `allpairs_comp` with its converse `map_allpairs`.
+  + Added `allpairs` extensionality lemmas for the following cases:
+    non-localised (`eq_allpairs`), dependent localised
+    (`eq_in_allpairs_dep`) and non-dependent localised
+    (`eq_in_allpairs`); as per `eq_in_map`, the latter two are
+    equivalences.
+
+- Generalized `{ffun A -> R}` to handle dependent functions, and to be
+  structurally positive so it can be used in recursive inductive type
+  definitions.
+
+  Minor backward incompatibilities: `fgraph f` is no longer
+  a field accessor, and no longer equal to `val f` as `{ffun A -> R}` is no
+  longer a `subType`; some instances of `finfun`, `ffunE`, `ffunK` may not unify
+  with a generic non-dependent function type `A -> ?R` due to a bug in
+  Coq version 8.9 or below.
+
+- Renamed double `seq` induction lemma from `seq2_ind` to `seq_ind2`,
+  and weakened its induction hypothesis.
+
+- Replaced the `nosimpl` in `rev` with a `Arguments simpl never`
+  directive.
+
+- Many corrections in implicits declarations.
+
+- fixed missing joins in `ssralg`, `ssrnum`, `finalg` and `countalg`
+
+### Renamed
+
+Renamings also involve the `_in` suffix counterpart when applicable
+
+- `mono_inj` -> `incr_inj`
+- `nmono_inj` -> `decr_inj`
+- `leq_mono_inj` -> `incnr_inj`
+- `leq_nmono_inj` -> `decnr_inj`
+- `homo_inj_ltn_lt` -> `incnr_inj`
+- `nhomo_inj_ltn_lt` -> `decnr_inj`
+- `homo_inj_in_lt` -> `inj_homo_ltr_in`
+- `nhomo_inj_in_lt` -> `inj_nhomo_ltr_in`
+- `ltn_ltrW_homo` -> `ltnrW_homo`
+- `ltn_ltrW_nhomo` -> `ltnrW_nhomo`
+- `leq_lerW_mono` -> `lenrW_mono`
+- `leq_lerW_nmono` -> `lenrW_nmono`
+- `homo_leq_mono` -> `lenr_mono`
+- `nhomo_leq_mono` -> `lenr_nmono`
+- `homo_inj_lt` -> `inj_homo_ltr`
+- `nhomo_inj_lt` -> `inj_nhomo_ltr`
+- `homo_inj_ltn_lt` -> `inj_homo_ltnr`
+- `nhomo_inj_ltn_lt` -> `inj_nhomo_ltnr`
+- `homo_mono` -> `ler_mono`
+- `nhomo_mono` -> `ler_nmono`
+- `big_setIDdep` -> `big_setIDcond`
+- `sum_nat_dep_const` -> `sum_nat_cond_const`
+
+### Misc
+
+- Removed trailing `_ : Type` field from packed classes. This performance
+  optimization is not strictly necessary with modern Coq versions.
+
+- Removed duplicated definitions of `tag`, `tagged` and `Tagged`
+  from `eqtype.v`. They are already in `ssrfun.v`.
+
+- Miscellaneous improvements to proof scripts and file organisation.
+
+## [1.7.0] - 2018-04-24
+
+Compatibility with Coq 8.8 and lost compatibility with
+Coq <= 8.5. This release is compatible with Coq 8.6, 8.7 and 8.8.
+
+- Integration in Coq startng from version 8.7 of:
+  + OCaml plugin (plugin for 8.6 still in the archive for backward compatibility)
+  + `ssreflect.v`, `ssrbool.v`, `ssrfun.v` and `ssrtest/`
+
+- Cleaning up the github repository: the math-comp repository is
+  now dedicated to the released material (as in the present
+  release). For instance, directories `real-closed/` and `odd-order/` now
+  have their own repository.
+
+### Changed
+
+- Library refactoring: `algC` and `ssrnum`.
+  Library `ssrnum.v` provides an interface `numClosedFieldType`, which abstracts the
+  theory of algebraic numbers. In particular, `Re`, `Im`, `'i`,
+  `conjC`, `n.-root` and `sqrtC`, previously defined in library `algC.v`,
+  are now part of this generic interface. In case of ambiguity,
+  a cast to type `algC`, of complex algebraic numbers, can be used to
+  disambiguate via  typing constraints. Some theory was thus made
+  more generic, and the corresponding lemmas, previously defined in
+  library `algC.v` (e.g. `conjCK`) now feature an extra, non maximal
+  implicit, parameter of type `numClosedFieldType`. This could break
+  some proofs.
+  Every theorem from `ssrnum` that used to be in `algC` changed statement.
+
+- `ltngtP`, `contra_eq`, `contra_neq`, `odd_opp`, `nth_iota`
+
+### Added
+
+- `iter_in`, `finv_in`, `inv_f_in`, `finv_inj_in`, `fconnect_sym_in`, `iter_order_in`,
+  `iter_finv_in`, `cycle_orbit_in`, `fpath_finv_in`, `fpath_finv_f_in`, `fpath_f_finv_in`
+- `big_allpairs`
+- `uniqP, uniqPn`
+- `dec_factor_theorem`, `mul_bin_down`, `mul_bin_left`
+- `abstract_context` (`in ssreflect.v`, now merged in Coq proper)
+
+### Renamed
+
+- Lemma `dvdn_fact` was moved from library `prime.v` to library `div.v`
+- `mul_Sm_binm -> mul_bin_diag
+- `divn1` -> `divz1` (in intdiv)
+- `rootC` -> `nthroot`
+- `algRe` -> `Re`
+- `algIm` -> `Im`
+- `algCi` -> `imaginaryC`
+- `reshape_index_leq` -> `reshape_leq`
+
+## [1.6.0] - 2015-11-24 (ssreflect + mathcomp)
+
+Major reorganization of the archive.
+
+- Files split into sub-directories: `ssreflect/`, `algebra/`, `fingroup/`,
+  `solvable/`, `field/` and `character/`. In this way the user can decide
+  to compile only the subset of the Mathematical Components library
+  that is relevant to her. Note that this introduces a possible
+  incompatibility for users of the previous version. A replacement
+  scheme is suggested in the installation notes.
+
+- The archive is now open and based on git. Public mirror at:
+  https://github.com/math-comp/math-comp
+
+- Sources of the reference manual of the Ssreflect tactic language are
+  also open and available at: https://github.com/math-comp/ssr-manual
+  Pull requests improving the documentation are welcome.
+
+### Renamed
+- `conjC_closed` -> `cfConjC_closed`
+- `class_transr` -> `class_eqP`
+- `cfclass_transl` -> `cfclass_transr`
+- `nontrivial_ideal` -> `proper_ideal`
+- `zchar_orthonormalP` -> `vchar_orthonormalP`
+
+### Changed
+- `seq_sub`
+- `orbit_in_transl`, `orbit_sym`, `orbit_trans`, `orbit_transl`, `orbit_transr`,
+  `cfAut_char`, `cfConjC_char`, `invg_lcosets`, `lcoset_transl`, `lcoset_transr`,
+  `rcoset_transl`, `rcoset_transr`, `mem2_last`, `bind_unless`, `unless_contra`, `all_and2`,
+  `all_and3`, `all_and4`, `all_and5`, `ltr0_neq0`, `ltr_prod`, `Zisometry_of_iso`
+
+### Added
+- `adhoc_seq_sub_choiceMixin`, `adhoc_seq_sub_[choice|fin]Type`
+- `orbit_in_eqP`, `cards_draws`, `cfAut_lin_char`, `cfConjC_lin_char`,
+  `extend_cfConjC_subset`, `isometry_of_free`, `cfAutK`, `cfAutVK`,
+  `lcoset_eqP`, `rcoset_eqP`, `class_eqP`, `gFsub_trans`, `gFnorms`,
+  `gFchar_trans`, `gFnormal_trans`, `gFnorm_trans`, `mem2_seq1`,
+  `dvdn_fact`, `prime_above`, `subKr`, `subrI`, `subIr`, `subr0_eq`,
+  `divrI`, `divIr`, `divKr`, `divfI`, `divIf`, `divKf`, `impliesP`, `impliesPn`,
+  `unlessL`, `unlessR`, `unless_sym`, `unlessP` (coercion), `classicW`,
+  `ltr_prod_nat`
+- Notation `\unless C, P`
+
+## [1.5.0] - 2014-03-12 (ssreflect + mathcomp)
+
+Split the archive in SSReflect and MathComp
+
+- With this release "ssreflect" has been split into two packages.
+  The Ssreflect one contains the proof language (plugin for Coq) and a
+  small set of core theory libraries about boolean, natural numbers,
+  sequences, decidable equality  and finite types. The Mathematical
+  Components one contains advanced theory files covering a wider
+  spectrum of mathematics.
+
+- With respect to version 1.4 the proof language got a few new
+  features related to forward reasoning and some bug fixes. The
+  Mathematical Components library features 16 new theory files and in
+  particular: some field and Galois theory, advanced character theory
+  and a construction of algebraic numbers.
+
+## [1.4.0] - 2012-09-05 (ssreflect)
+
+- With this release the plugin code received many bug fixes and the
+  existing libraries relevant updates.  This release also includes
+  some new libraries on the following topics: rational numbers,
+  divisibility of integers, F-algebras, finite dimensional field
+  extensions and Euclidean division for polynomials over a ring.
+
+- The release includes a major code refactoring of the plugin for Coq
+  8.4.  In particular a documented ML API to access the pattern matching
+  facilities of Ssreflect from third party plugins has been introduced.
+
+## [1.3.0] - 2011-03-14 (ssreflect)
+
+- The tactic language has been extended with several new features, inspired by
+  the five years of intensive use in our project. However we have kept
+  the core of the language unchanged; the new library compiles with
+  Ssreflect 1.2.  Users of a Coq 8.2 toplevel statically linked with
+  Ssreflect 1.2 need to comment the Declare ML Module "ssreflect" line
+  in ssreflect.v to properly compile the 1.3 library.  We will continue
+  supporting new releases of Coq in due course.
+
+- The new library adds general linear algebra (matrix rank, subspaces)
+  and all of the advanced finite group that was developed in the
+  course of completing the Local Analysis part of the Odd Order Theorem,
+  starting from the Sylow and Hall theorems and including full structure
+  theorems for abelian, extremal and extraspecial groups, and general
+  (modular) linear representation theory.
+
+## [1.2.0] - 2009-08-14 (ssreflect)
+
+No change log
+
+## [1.1.0] - 2008-03-18 (ssreflect)
+
+First public release

CONTRIBUTING.md

@@ -76,3 +76,73 @@ This particular example can be problematic if matrix.v is imported because then,
   + Elements of another ring should be named `x`, `y`, `z`, `u`, `v`, `w`, ...
   + Polynomials should be named by lower case letter `p`, `q`, `r` ... (to avoid collision with properties named `P`, `Q`, ...)
   + Matrices should be named `A`, `B`, ..., `M`, `N`, ...
+
+### Naming conventions (Non exhaustive)
+#### Names in the library usually obey one of following the convention
+ - `(condition_)?mainSymbol_suffixes`
+ - `mainSymbol_suffixes(_condition)?`
+Or in the presence of a property denoted by a nary or unary predicate:
+ - `naryPredicate_mainSymbol+`
+ - `mainSymbol_unaryPredicate`
+#### Where :
+ - `mainSymbol` is the most meaningful part of the lemma. It generally is the head symbol of the right-hand side of an equation or the head symbol of a theorem. It can also simply be the main object ofstudy, head symbol or not. It is usually either
+  - one of the main symbols of the theory at hand. For example, it will be `opp`, `add`, `mul`, etc...
+  - or a special "canonical" operation, such as a ring morphism or a
+    subtype predicate. e.g. `linear`, `raddf`, `rmorph`, `rpred`, etc ...
+ - "condition" is used when the lemma applies under some hypothesis.
+ - "suffixes" are there to refine what shape and/or what other symbols  the lemma has. It can either be the name of a symbol ("add", "mul",  etc...), or the (short) name of a predicate ("`inj`" for "`injectivity`", "`id`" for "identity", ...) or an abbreviation.
+Abbreviations are in the header of the file which introduce them. We list here the main abbreviations.
+  - `A` -- associativity, as in `andbA : associative andb.`
+  - `AC` -- right commutativity.
+  - `ACA` -- self-interchange (inner commutativity), e.g., `orbACA : (a || b) || (c || d) = (a || c) || (b || d).`
+  - `b` -- a boolean argument, as in `andbb : idempotent andb.`
+  - `C` -- commutativity, as in `andbC : commutative andb`,
+        -- alternatively, predicate or set complement, as in `predC.`
+  - `CA` -- left commutativity.
+  - `D` -- predicate or set difference, as in `predD.`
+  - `E` -- elimination lemma, as in `negbFE : ~~ b = false -> b`.
+  - `F` or `f` -- boolean false, as in `andbF : b && false = false.`
+  - `g` -- a group argument
+  - `I` -- left/right injectivity, as in `addbI : right_injective addb` 
+        -- alternatively predicate or set intersection, as in `predI.`
+  - `l` -- a left-hand operation, as `andb_orl : left_distributive andb orb.`
+  - `N` or `n` -- boolean negation, as in `andbN : a && (~~ a) = false.`
+  - `n` -- alternatively, it is a natural number argument,
+  - `N` -- alternatively ring negation, as in `mulNr : (- x) * y = - (x * y).`
+  - `P` -- a characteristic property, often a reflection lemma, as in
+     `andP : reflect (a /\ b) (a && b)`.
+  - `r` -- a right-hand operation, as `orb_andr : right_distributive orb andb.`
+      -- alternatively, it is a ring argument
+  - `T` or `t` -- boolean truth, as in `andbT: right_id true andb.`
+        -- alternatively, total set
+  - `U` -- predicate or set union, as in `predU`.
+  - `W` -- weakening, as in `in1W : {in D, forall x, P} -> forall x, P.`
+  - `0` -- ring or nat 0, or empty set, as in `addr0 : x + 0 = x.`
+  - `1` -- ring; nat or group 1, as in `mulr1 : x * 1 = x.`
+  - `D` -- addition, as in `linearD : f (u + v) = f u + f v.`
+  - `B` -- subtraction, as in `opprB : - (x - y) = y - x.`
+  - `M` -- multiplication, as in `invfM : (x * y)^-1 = x^-1 * y^-1.`
+  - `Mn` -- ring nat multiplication, as in `raddfMn : f (x *+ n) = f x *+ n.`
+  - `V` -- multiplicative inverse, as in `mulVr : x^-1 * x = 1.`
+  - `X` -- exponentiation, as in `rmorphX : f (x ^+ n) = f x ^+ n.`
+  - `Z` -- (left) module scaling, as in `linearZ : f (a *: v)  = s *: f v.`
+  - `z` -- an int argument
+#### Typical search pattern
+`Search _ "prefix" "suffix"* (symbol|pattern)* in library.`
+
+## Doc style.
+### Header documentary comments
+We try to document types, definitions and notations precisely, but only describe
+the lemmas and theorems in general terms, because we don't want to discourage users
+from actually reading the documentation.
+There are some exceptions for some particularly important theorems.
+
+### Commenting source code
+The MathComp library uses exclusively block comments, with 80-character lines
+enclosed in the `(*` / `*)` delimiters, e.g.
+```
+(* Lorem ipsum dolor sit amet, consectetuer adipiscing elit.  Donec hendrerit *)
+(* tempor tellus.  Donec pretium posuere tellus.  Proin quam nisl, tincidunt  *)
+(* et, mattis eget, convallis nec, purus.                                     *)
+```
+Multiline comments are strictly limited to out-commented code.

ChangeLog

-24/04/2018 - compatibility with Coq 8.8 and several small fixes - version 1.7
-
-	* Added compatibility with Coq 8.8 and lost compatibility with
-	  Coq <= 8.5. This release is compatible with Coq 8.6, 8.7 and 8.8.
-
-	* Integration to Coq: ssrbool.v ssrfun.v and plugin.
-	  ssrtest also moved to Coq test suite.
-
-	* Cleaning up the github repository: the math-comp repository is
-	  now dedicated to the released material (as in the present
-	  release). For instance, directories real-closed and odd-order now
-	  have their own repository.
-
-	* Library refactoring: algC ssrnum: Library ssrnum.v now
-	  provides an interface numClosedFieldType, which abstracts the
-	  theory of algebraic numbers. In particular, Re, Im, 'i,
-	  conjC, n.-root and sqrtC, previously defined in library algC.v,
-	  are now part of this generic interface. In case of ambiguity,
-	  a cast to type algC, of complex algebraic numbers, can be used to
-	  disambiguate via  typing constraints. Some theory was thus made
-	  more generic, and the corresponding lemmas, previously defined in
-	  library algC.v (e.g. conjCK) now feature an extra, non maximal
-	  implicit, parameter of type numClosedFieldType. This could break
-	  some proofs.
-
-	* Lemma dvdn_fact was moved from library prime.v to library div.v
-
-	* Structures, changes in interfaces:
-	  numClosedFieldType
-
-	* New Theorems:
-	  iter_in, finv_in, inv_f_in, finv_inj_in, fconnect_sym_in,
-	  iter_order_in, iter_finv_in, cycle_orbit_in, fpath_finv_in,
-	  fpath_finv_f_in, fpath_f_finv_in
-	  big_allpairs
-	  uniqP, uniqPn
-	  dec_factor_theorem,
-	  mul_bin_down, mul_bin_left
-          abstract_context (now merged in Coq)
-
-	* Renamed/generalized:
-	  mul_Sm_binm -> mul_bin_diag
-	  divn1 -> divz1 (in intdiv)
-	  rootC -> nthroot
-	  algRe -> Re
-	  algIm -> Im
-	  algCi -> imaginaryC
-  	  reshape_index_leq -> reshape_leq
-	  Every theorem from ssrnum that used to be in algC
-
-	* Generalized or improved:
-	  ltngtP, contra_eq, contra_neq, odd_opp, nth_iota
-
-24/11/2015 - major reorganization of the archive - version 1.6
-
-	* Files split into sub-directories: ssreflect, algebra, fingroup,
-	  solvable, field and character. In this way the user can decide
-	  to compile only the subset of the Mathematical Components library
-	  that is relevant to her. Note that this introduces a possible
-	  incompatibility for users of the previous version. A replacement
-	  scheme is suggested in the installation notes.
-
-	* The archive is now open and based on git. Public mirror at:
-	         https://github.com/math-comp/math-comp
-
-	* Sources of the reference manual of the Ssreflect tactic language are
-	  also open and available at:
-		https://github.com/math-comp/ssr-manual
-	  Pull requests improving the documentation are welcome.
-
-	* Renaming or replacements:
-	  conjC_closed -> cfConjC_closed
-	  class_transr -> class_eqP
-	  cfclass_transl -> cfclass_transr
-	  nontrivial_ideal -> proper_ideal
-	  zchar_orthonormalP -> vchar_orthonormalP
-
-	* Definitions that changed:
-	  seq_sub
-
-	* Statements that changed:
-	  orbit_in_transl, orbit_sym, orbit_trans, orbit_transl, orbit_transr,
-	  cfAut_char, cfConjC_char, invg_lcosets, lcoset_transl,
-	  lcoset_transr, rcoset_transl, rcoset_transr, mem2_last,
-	  bind_unless, unless_contra, all_and2, all_and3, all_and4, all_and5,
-	  ltr0_neq0, ltr_prod, Zisometry_of_iso
-
-	* New definitions:
-	  adhoc_seq_sub_choiceMixin, adhoc_seq_sub_[choice|fin]Type
-
-	* New theorems:
-	  orbit_in_eqP, cards_draws, cfAut_lin_char, cfConjC_lin_char,
-	  extend_cfConjC_subset, isometry_of_free, cfAutK, cfAutVK,
-	  lcoset_eqP, rcoset_eqP, class_eqP, gFsub_trans, gFnorms,
-	  gFchar_trans, gFnormal_trans, gFnorm_trans, mem2_seq1,
-	  dvdn_fact, prime_above, subKr, subrI, subIr, subr0_eq,
-	  divrI, divIr, divKr, divfI, divIf, divKf, impliesP, impliesPn,
-	  unlessL, unlessR, unless_sym, unlessP (coercion), classicW,
-	  ltr_prod_nat
-
-	* New notation: "\unless C, P"
-
-12/03/2014 - split the archive in SSReflect and MathComp - version 1.5
-	* With this release "ssreflect" has been split into two packages.
-	  The Ssreflect one contains the proof language (plugin for Coq) and a
-	  small set of core theory libraries about boolean, natural numbers,
-	  sequences, decidable equality  and finite types. The Mathematical
-	  Components one contains advanced theory files covering a wider
-	  spectrum of mathematics.
-
-	* With respect to version 1.4 the proof language got a few new
-	  features related to forward reasoning and some bug fixes. The
-	  Mathematical Components library features 16 new theory files and in
-	  particular: some field and Galois theory, advanced character theory
-	  and a construction of algebraic numbers.
-
-05/09/2012 - ssreflect - version 1.4
-	* With this release the plugin code received many bug fixes and the
-	  existing libraries relevant updates.  This release also includes
-	  some new libraries on the following topics: rational numbers,
-	  divisibility of integers, F-algebras, finite dimensional field
-	  extensions and Euclidean division for polynomials over a ring.
-
-	* The release includes a major code refactoring of the plugin for Coq
-	  8.4.  In particular a documented ML API to access the pattern matching
-	  facilities of Ssreflect from third party plugins has been introduced.
-
-14/03/2011 - ssreflect - version 1.3
-	* The tactic language has been extended with several new features,
-	  inspired by the five years of intensive use in our project. However we
-	  have kept the core of the language unchanged; the new library compiles
-	  with Ssreflect 1.2.  Users of a Coq 8.2 toplevel statically linked
-	  with Ssreflect 1.2 need to comment the Declare ML Module "ssreflect"
-	  line in ssreflect.v to properly compile the 1.3 library.  We will
-	  continue supporting new releases of Coq in due course.
-
-	* The new library adds general linear algebra (matrix rank, subspaces)
-	  and all of the advanced finite group that was developed in the course
-	  of completing the Local Analysis part of the Odd Order Theorem,
-	  starting from the Sylow and Hall theorems and including full structure
-	  theorems for abelian, extremal and extraspecial groups, and general
-	  (modular) linear representation theory.
-
-14/08/2009 - ssreflect - version 1.2
-	* No change log
-
-18/03/2008 - ssreflect - version 1.1
-	* First public release

Dockerfile

+ARG coq_image="coqorg/coq:dev"
+FROM ${coq_image} as builder
+
+WORKDIR /home/coq/mathcomp
+
+COPY . .
+
+ARG compiler="base"
+# other possible value: "edge"
+
+RUN ["/bin/bash", "--login", "-c", "set -x \
+  && declare -A switch_table \
+  && switch_table=( [\"base\"]=\"${COMPILER}\" [\"edge\"]=\"${COMPILER_EDGE}\" ) \
+  && opam_switch=\"${switch_table[${compiler}]}\" \
+  && [ -n \"opam_switch\" ] \
+  && opam switch set ${opam_switch} \
+  && eval $(opam env) \
+  && unset \"switch_table[${compiler}]\" \
+  && for sw in \"${switch_table[@]}\"; do if [ -n \"$sw\" ]; then opam switch remove -y \"${sw}\"; fi; done \
+  && opam repository add --all-switches --set-default coq-extra-dev https://coq.inria.fr/opam/extra-dev \
+  && opam repository add --all-switches --set-default coq-core-dev https://coq.inria.fr/opam/core-dev \
+  && opam update -y \
+  && opam config list && opam repo list && opam list && coqc --version \
+  && sudo chown -R coq:coq /home/coq/mathcomp \
+  && opam pin add -n -k path coq-mathcomp-ssreflect . \
+  && opam pin add -n -k path coq-mathcomp-fingroup . \
+  && opam pin add -n -k path coq-mathcomp-algebra . \
+  && opam pin add -n -k path coq-mathcomp-solvable . \
+  && opam pin add -n -k path coq-mathcomp-field . \
+  && opam pin add -n -k path coq-mathcomp-character . \
+  && opam install -y -v -j ${NJOBS} coq-mathcomp-character \
+  && opam clean -a -s --logs"]
+
+FROM coqorg/base:bare
+
+ENV MATHCOMP_VERSION="dev"
+ENV MATHCOMP_PACKAGE="coq-mathcomp-character"
+
+COPY --from=builder --chown=coq:coq /home/coq/.opam /home/coq/.opam
+COPY --from=builder --chown=coq:coq /home/coq/.profile /home/coq/.profile

Dockerfile.make

+ARG coq_image="coqorg/coq:dev"
+FROM ${coq_image}
+
+WORKDIR /home/coq/mathcomp
+
+COPY . .
+
+ARG compiler="base"
+# other possible value: "edge"
+
+RUN ["/bin/bash", "--login", "-c", "set -x \
+  && declare -A switch_table \
+  && switch_table=( [\"base\"]=\"${COMPILER}\" [\"edge\"]=\"${COMPILER_EDGE}\" ) \
+  && opam_switch=\"${switch_table[${compiler}]}\" \
+  && [ -n \"opam_switch\" ] \
+  && opam switch set ${opam_switch} \
+  && eval $(opam env) \
+  && unset \"switch_table[${compiler}]\" \
+  && for sw in \"${switch_table[@]}\"; do [ -n \"$sw\" ] && opam switch remove -y \"${sw}\"; done \
+  && opam repository add --all-switches --set-default coq-extra-dev https://coq.inria.fr/opam/extra-dev \
+  && opam repository add --all-switches --set-default coq-core-dev https://coq.inria.fr/opam/core-dev \
+  && opam update -y \
+  && opam config list && opam repo list && opam list && coqc --version \
+  && opam clean -a -s --logs \
+  && sudo chown -R coq:coq /home/coq/mathcomp \
+  && cd mathcomp \
+  && make Makefile.coq \
+  && make -f Makefile.coq -j ${NJOBS} all \
+  && make -f Makefile.coq install"]

INSTALL.md

@@ -4,15 +4,15 @@ The library is divided into packages which group together related
 files. Each package defines a distribution and compilation unit.
 
 Packages can be compiled using the traditional make utility or
-the more recent OPAM one. The released and current dev versions are
+the more recent OPAM one (version 2). The released and current dev versions are
 also available as OPAM packages.
 
 ## Compilation and installation of released and current dev version with OPAM
-If you just installed OPAM you may have to do the following. You may also want
-to read [OPAM user manual](https://opam.ocaml.org/doc/Usage.html) first. 
+If you just installed OPAM version 2 you should proceed as follows: 
 ```
-opam init
-eval `opam config env`
+opam --version # should print 2.x.y
+opam init -n --comp=ocaml-base-compiler.4.05.0
+eval $(opam config env)
 ```
 Once your OPAM environment is configured
 you can install any math-comp package via
@@ -20,21 +20,37 @@ you can install any math-comp package via
 opam repo add coq-released https://coq.inria.fr/opam/released
 opam pin add -n coq -k version 8.8.0
 opam install coq -j3
-opam install coq-mathcomp-ssreflect.1.7.0 -j3
+opam install coq-mathcomp-ssreflect -j3
 ```
 Replace `ssreflect` here by the package you want, the dependencies will be
 installed automatically. We recommend pinning a particular version of Coq
-(here `8.8.0`).
+(we give `8.8.0` as an example, see `CHANGELOG.md` for the supported versions).
 To get the latest development version you need to execute the following:
 ```
 opam repo add coq-extra-dev https://coq.inria.fr/opam/extra-dev
 opam install coq-mathcomp-ssreflect.dev -j3
 ```
+You can learn more about OPAM by reading its [user manual](https://opam.ocaml.org/doc/Usage.html).
+
+## Compilation and installation in a dedicated OPAM root
+
+If you want to install the library in a dedicated environment
+(let's name it `MC`) which will remain independent from your
+current OPAM setup you can run the following commands:
+```
+opam init --root=$PWD/MC
+eval $(opam config env --root=$PWD/MC`)
+```
+After that the installations instructions above apply.
+
+Coq and the library are installed in the `$PWD/MC` directory
+(called an OPAM root). To discard the OPAM root, simply delete
+the directory.
 
 ## Compilation and installation with make
 
 The instructions assume you are in the `mathcomp` directory and that
-you have a supported version of Coq: 8.6, 8.7 or 8.8.
+you have a supported version of Coq (listed in `CHANGLOG.md`).
 
 If `coqc` is in your `PATH`, then you are good to go.  Alternatively, you
 can export the `COQBIN` variable to tell `make` where the `coqc` binary is:
@@ -58,22 +74,28 @@ To install the compiled library, just execute `make install`.
 
 ## Compilation and installation of a custom version using OPAM
 
-The instructions assume you are in the `mathcomp` directory
-and that you have OPAM installed and configured with the
-standard Coq repositories.
+The instructions assume you are in the parent directory (that contains
+this file `INSTALL.md`) and that you have OPAM installed and
+configured with the standard Coq repositories.
 
-For each package, pin the `opam` file:
+First, we recommend pinning a particular version of Coq
+(e.g. `8.8.0`):
 ```
-opam pin -n add ssreflect
+opam pin add -n coq -k version 8.8.0
 ```
+
+Then for each math-comp package, pin the `opam` file:
+```
+opam pin add -n -k path coq-mathcomp-ssreflect .
+```
+
 This can be achieved in one go as follows:
 ```
-for P in */opam; do opam pin -n add ${P%%/opam}; done
+for P in *.opam; do opam pin add -n -k path ${P%.opam} .; done
 ```
 
 Then you can use `opam install` to compile and install any package.
 For example:
 ```
-opam install coq.8.8.0 coq-mathcomp-ssreflect
+opam install coq-mathcomp-character -j3
 ```
-

README.md

-[![Build Status](https://travis-ci.org/math-comp/math-comp.svg?branch=master)](https://travis-ci.org/math-comp/math-comp)
+[![pipeline status](https://gitlab.com/math-comp/math-comp/badges/master/pipeline.svg)](https://gitlab.com/math-comp/math-comp/commits/master)
+[![Join the chat at https://gitter.im/math-comp/](https://badges.gitter.im/math-comp.svg)](https://gitter.im/math-comp?utm_source=badge&utm_medium=badge&utm_campaign=pr-badge&utm_content=badge)
 
 # The Mathematical Components repository
 
 The Mathematical Components Library is an extensive and coherent
 repository of formalized mathematical theories. It is based on
 the [Coq](http://coq.inria.fr) proof assistant, powered with the
-[Coq/SSReflect](https://coq.inria.fr/distrib/current/refman/ssreflect.html)
+[Coq/SSReflect](https://coq.inria.fr/distrib/current/refman/proof-engine/ssreflect-proof-language.html)
 language.
 
 These formal theories cover a wide spectrum of topics, ranging from the formal theory of general purpose data structures like [lists](mathcomp/ssreflect/seq.v), [prime numbers](mathcomp/ssreflect/prime.v) or [finite graphs](mathcomp/ssreflect/fingraph.v), to advanced topics in algebra. The repository includes the foundation of formal theories used in a [formal proof](https://www.ams.org/notices/200811/tx081101382p.pdf) of the [Four Colour Theorem](https://en.wikipedia.org/wiki/Four_color_theorem) (Appel - Haken, 1976) and a [mechanization](https://hal.archives-ouvertes.fr/hal-00816699/) of the [Odd Order Theorem](https://en.wikipedia.org/wiki/Feit%E2%80%93Thompson_theorem) (Feit - Thompson, 1963), a landmark result of finite group theory, which utilizes the library extensively.
 
 ## Installation
 
-If you already have OPAM installed:
+If you already have OPAM installed (a fresh or up to date version of opam 2 is required):
 
 ```
 opam repo add coq-released https://coq.inria.fr/opam/released
@@ -25,6 +26,8 @@ installation instructions in other scenarios.
 
 ## How to get help
 
+- The [website](http://math-comp.github.io/math-comp/) of the MathComp library
+  contains links to the HTML documentation of each file.
 - The [ssreflect mailing
   list](https://sympa.inria.fr/sympa/info/ssreflect) is the primary
   venue for help and questions about the library.

mathcomp/algebra/opam → coq-mathcomp-algebra.opam

-opam-version: "1.2"
+opam-version: "2.0"
 name: "coq-mathcomp-algebra"
 version: "dev"
 maintainer: "Mathematical Components <mathcomp-dev@sympa.inria.fr>"
 
-homepage: "http://math-comp.github.io/math-comp/"
-bug-reports: "Mathematical Components <mathcomp-dev@sympa.inria.fr>"
+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 "-j" "%{jobs}%" ]
-install: [ make "install" ]
+build: [ make "-C" "mathcomp/algebra" "-j" "%{jobs}%" ]
+install: [ make "-C" "mathcomp/algebra" "install" ]
 remove: [ "sh" "-c" "rm -rf '%{lib}%/coq/user-contrib/mathcomp/algebra'" ]
 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...
+"""

mathcomp/character/opam → coq-mathcomp-character.opam

-opam-version: "1.2"
+opam-version: "2.0"
 name: "coq-mathcomp-character"
 version: "dev"
 maintainer: "Mathematical Components <mathcomp-dev@sympa.inria.fr>"
 
-homepage: "http://math-comp.github.io/math-comp/"
-bug-reports: "Mathematical Components <mathcomp-dev@sympa.inria.fr>"
+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 "-j" "%{jobs}%" ]
-install: [ make "install" ]
+build: [ make "-C" "mathcomp/character" "-j" "%{jobs}%" ]
+install: [ make "-C" "mathcomp/character" "install" ]
 remove: [ "sh" "-c" "rm -rf '%{lib}%/coq/user-contrib/mathcomp/character'" ]
 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.
+"""

mathcomp/field/opam → coq-mathcomp-field.opam

-opam-version: "1.2"
+opam-version: "2.0"
 name: "coq-mathcomp-field"
 version: "dev"
 maintainer: "Mathematical Components <mathcomp-dev@sympa.inria.fr>"
 
-homepage: "http://math-comp.github.io/math-comp/"
-bug-reports: "Mathematical Components <mathcomp-dev@sympa.inria.fr>"
+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 "-j" "%{jobs}%" ]
-install: [ make "install" ]
+build: [ make "-C" "mathcomp/field" "-j" "%{jobs}%" ]
+install: [ make "-C" "mathcomp/field" "install" ]
 remove: [ "sh" "-c" "rm -rf '%{lib}%/coq/user-contrib/mathcomp/field'" ]
 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...
+"""

mathcomp/fingroup/opam → coq-mathcomp-fingroup.opam

-opam-version: "1.2"
+opam-version: "2.0"
 name: "coq-mathcomp-fingroup"
 version: "dev"
 maintainer: "Mathematical Components <mathcomp-dev@sympa.inria.fr>"
 
-homepage: "http://math-comp.github.io/math-comp/"
-bug-reports: "Mathematical Components <mathcomp-dev@sympa.inria.fr>"
+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 "-j" "%{jobs}%" ]
-install: [ make "install" ]
+build: [ make "-C" "mathcomp/fingroup" "-j" "%{jobs}%" ]
+install: [ make "-C" "mathcomp/fingroup" "install" ]
 remove: [ "sh" "-c" "rm -rf '%{lib}%/coq/user-contrib/mathcomp/fingroup'" ]
 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...
+"""

mathcomp/solvable/opam → coq-mathcomp-solvable.opam

-opam-version: "1.2"
+opam-version: "2.0"
 name: "coq-mathcomp-solvable"
 version: "dev"
 maintainer: "Mathematical Components <mathcomp-dev@sympa.inria.fr>"
 
-homepage: "http://math-comp.github.io/math-comp/"
-bug-reports: "Mathematical Components <mathcomp-dev@sympa.inria.fr>"
+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 "-j" "%{jobs}%" ]
-install: [ make "install" ]
+build: [ make "-C" "mathcomp/solvable" "-j" "%{jobs}%" ]
+install: [ make "-C" "mathcomp/solvable"  "install" ]
 remove: [ "sh" "-c" "rm -rf '%{lib}%/coq/user-contrib/mathcomp/solvable'" ]
 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.
+"""

mathcomp/ssreflect/opam → coq-mathcomp-ssreflect.opam

-opam-version: "1.2"
+opam-version: "2.0"
 name: "coq-mathcomp-ssreflect"
 version: "dev"
 maintainer: "Mathematical Components <mathcomp-dev@sympa.inria.fr>"
 
-homepage: "http://math-comp.github.io/math-comp/"
-bug-reports: "Mathematical Components <mathcomp-dev@sympa.inria.fr>"
+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 "-j" "%{jobs}%" ]
-install: [ make "install" ]
+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.5" & < "8.8~") | (= "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
+"""

debian/changelog

+ssreflect (1.9.0+dfsg-1) unstable; urgency=medium
+
+  * New upstream release.
+    Repack upstream (remove docs/htmldoc/js/ and docs/javascripts/).
+  * Build-depends: minimal coq version 8.7, according to opam file.
+  * Standards-Version 4.4.0 (no change)
+  * debian/libssreflect-coq.docs: ChangeLog => CHANGELOG.md
+
+ -- Ralf Treinen <treinen@debian.org>  Tue, 20 Aug 2019 09:47:51 +0200
+
 ssreflect (1.7.0+dfsg-1) unstable; urgency=medium
 
   * New upstream version. This fixes a FTBFS with coq 8.9.0 (closes: #919461)

debian/control

@@ -6,8 +6,8 @@ Uploaders: Stéphane Glondu <glondu@debian.org>,
  Ralf Treinen <treinen@debian.org>
 Build-Depends:
  debhelper-compat (= 12),
- coq (>= 8.6)
-Standards-Version: 4.3.0
+ coq (>= 8.7)
+Standards-Version: 4.4.0
 Section: math
 Homepage: https://math-comp.github.io/math-comp/
 Vcs-Browser: https://salsa.debian.org/ocaml-team/ssreflect

debian/libssreflect-coq.docs

-ChangeLog
+CHANGELOG.md
 README.md
 docs/htmldoc/