The Coq mailing list

[Pierre Roux <Pierre.Roux AT onera.fr>]

We are proud to announce the immediate availability of the
Mathematical Components library version 2.0.0.

### Important

MathComp 2.x is not immediately compatible with version 1.17.0, i.e.,
porting your development to this new version may require more effort
than usual. On the positive side, the entire hierarchy of structures
and morphisms has been rewritten using the Hierarchy Builder tool (HB)
[1]. This greatly simplifies the development of the hierarchy of
structures and will make it possible to extend it without breaking
user developments.

MathComp 1.x will continue to be maintained and ported to new versions
of Coq for the foreseeable future. Still we expect most of the
development to happen on top of 2.0.0 and we encourage users to port
their developments to the new version. We ported many developments
ourselves [2] and wrote a little tutorial detailing the most commonly
required steps [3].

# MathComp 2.0.0

This release is compatible with Coq 8.16 and 8.17.
This release requires HB version 1.4 (on Coq-Elpi 1.16).

The hierarchy of structures and morphisms is now based on HB and
features 63 new structures, among which the ones for semigroups and
semi rings as well as the ones for morphisms on order structures.

The contributors to this version are: Anton Trunov, Cyril Cohen,
Enrico Tassi, Kazuhiko Sakaguchi, Laurent Théry, Marie Kerjean, Pierre
Roux, Quentin Canu, Reynald Affeldt, Thomas Portet, Xavier Allamigeon,
Yves Bertot.

The Docker images [4] are maintained by Érik Martin-Dorel.

See https://github.com/math-comp/math-comp/releases/tag/mathcomp-2.0.0
to download or see the CHANGELOG.md [5] file for more details.

Packages for opam and docker images are available while Nix packages
are in preparation.

## Known annoyances

While we believe MathComp 2.0.0 is in a usable state for the majority
of our users, we are also aware of few annoyances which we plan to fix
in future releases:

* The 2.0.0 release requires substantial resources to compile: some
  huge files (e.g., order.v) require 2.5G of memory to compile (or
  4.5G with Coq 8.17), and the full compilation is four times longer
  than it was with 1.17.0 (about 15 minutes on recent laptops).
* Canonical instances have longer, generated, names than in 1.17.0,
  hence they may clutter your goal more than they used to (e.g., if
  you used to see `bool_eqType` you will now see
  `Datatypes_bool__canonical__eqtype_Equality`). Usually the `/=` flag
  helps tyding goals up. Note that one should not rely on these
  generated names. Since Coq 8.16 one can use type casts to input them
  (e.g. `bool : eqType`).
* Rewriting with theorems from the predicate hierarchies (`rpredD`,
  etc.) may leave subgoals which require an extra simplification step
  (i.e. use `rpredD/=`).
* The output of `HB.about`, `HB.howto`, and `HB.instance` is quite
  useful already but still subpar to our taste.
* The output of coqdoc is missing the `HB.mixin` and `HB.factory`
  commands as well as the `HB.builders` sections. Links to generated
  definitions are also broken.

[1] https://github.com/math-comp/hierarchy-builder/
[2] Our CI is currently green on the following developments: abel,
addition-chains, mathcomp-analysis, autosubst, bigenough,
category-theory, mathcomp-classical, coqeal, coq-bits, finmap,
fourcolor, gaia, graph-theory, interval, multinomials, odd-order,
QuickChick, real-closed, reglang, relation-algebra, tarjan, Verdi,
comp-dec-modal.
We will open a PR on your repo soon, if we did not already.
[3] 
https://github.com/math-comp/math-comp/blob/master/etc/porting_to_mathcomp2/porting.pdf
[4] https://hub.docker.com/r/mathcomp/mathcomp/tags?name=2.0.0
[5] https://github.com/math-comp/math-comp/blob/master/CHANGELOG.md