MathComp 2.0.0 released

Announcements
1

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

: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 (HB). 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 Release The Mathematical Components Library 2.0.0 · math-comp/math-comp · GitHub to download or see the CHANGELOG.md 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 a 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.

1 Like