This release is compatible with Coq 8.20 and Rocq 9.0 and 9.1.

The main changes are:

• multiple refinements of the algebraic hierarchies (this may lead to a few small breakages, in which case we recommend using Rocq 9.1 that should minimize such breakages in the future)
• package mathcomp-ssreflect got split into mathcomp-boot and mathcomp-order, if you weren't using the order.v file, replacing your mathcomp-ssreflect dependency by mathcomp-boot may save you some compilation time

See the CHANGELOG.md file for more details.

This release is compatible with Coq 8.19, 8.20 and Rocq 9.0.

There are five main changes:

• the implementation of potentially zero rings,
• the generalization of modules to semi-modules,
• the archimedean structure contains the ceil and floor functions,
• there is now a lightweight automation procedure for semi-decision of interval membership (see interval_inference.v),
• there is no more dependency in the standard library,

and many other improvements.

See the CHANGELOG.md file for more details.

This release is compatible with Coq 8.18 to 8.20.
From now on there will be no more 1.x version of mathcomp.

See the CHANGELOG.md file for more details.

This release is compatible with Coq 8.16 to 8.19.

See the CHANGELOG.md file for more details.

This release is compatible with Coq 8.16 to 8.19.

See the CHANGELOG.md file for more details.

This release is compatible with Coq versions 8.16, 8.17, and 8.18.

See the CHANGELOG.md file for more details.

This release is compatible with Coq 8.16, 8.17, and 8.18.

Thanks to the latest versions of Coq, coq-elpi, and Hierarchy-Builder, compilation requires less resources than MathComp 2.0.0. Memory consumption is below 1.5GB and compilation time has been almost halved. This remains slower than MathComp 1.17.0 (and the forthcoming MathComp 1.18.0).

See the CHANGELOG.md for the several additions (new mathematical structures, lemmas, etc.) to the library.

⚠️ 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. 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 [1] and wrote a little tutorial detailing the most commonly required steps.

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 are maintained by Érik Martin-Dorel.

See the CHANGELOG.md file for more details.

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] : 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.

This release is compatible with Coq 8.15, 8.16, and 8.17.

See the CHANGELOG.md file for more details.

This release is compatible with Coq 8.13, 8.14, 8.15, 8.16, and 8.17.

See the CHANGELOG.md file for more details.