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.

:warning: Important :warning:

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.

This release is compatible with Coq 8.15 and 8.16. The major change of this version is to use Hierarchy Builder to generate algebraic hierarchy. Users of versions 1.0.0 can expect breaking changes. We do not recommend yet the adoption of this new release in production, but we make it available for early tests.

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

This release drops support for Coq 8.11 and 8.12, while it gains support for 8.16 (version 1.14.0 won't compile on Coq 8.16).

See the CHANGELOG.md file for more details.

This release is compatible with Coq 8.11, 8.12, 8.13, 8.14 and 8.15.

This release only includes minor changes.

See the CHANGELOG.md file for more details.