MathComp 2.4.0 released

Announcements
,
1

We are proud to announce the immediate availability of the Mathematical Components library version 2.4.0.
The webpage, and documentation, are available at https://math-comp.github.io/.

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.

The contributors to this version are:
Alessandro Bruni, Cyril Cohen, Enrico Tassi, Erik Martin-Dorel, Kazuhiko Sakaguchi, Kimaya Bedarkar, Laurent Théry, Pierre Pomeret-Coquot, Pierre Roux, Quentin Vermande, Reynald Affeldt, Mitsuharu Yamamoto, and Yves Bertot.

See Release The Mathematical Components Library 2.4.0 · math-comp/math-comp · GitHub to download or see the CHANGELOG.md.

Packages for opam, nix, and docker are in preparation.

Best regards,

The Mathematical Components team