# MathComp 2.4.0 released

**URL:** <https://discourse.rocq-prover.org/t/mathcomp-2-4-0-released/2632>\
**Category:** Announcements\
**Tags:** ssreflect, mathcomp\
**Created:** [April 14, 2025, 3:45pm UTC](https://discourse.rocq-prover.org/t/mathcomp-2-4-0-released/2632 "2025-04-14T15:45:36Z")\
**Posts on this page:** 1\
**Page:** 1

<div class="post-metadata">

**Author:** ![CohenCyril](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/cohencyril/32/1165_2.png) [@CohenCyril](https://discourse.rocq-prover.org/u/CohenCyril)\
**Post date:** [April 14, 2025, 3:45pm UTC](https://discourse.rocq-prover.org/t/mathcomp-2-4-0-released/2632/1 "2025-04-14T15:45:36Z")

</div>

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/](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](https://github.com/math-comp/math-comp/releases/tag/mathcomp-2.4.0) to download or see the `CHANGELOG.md`.

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

Best regards,

The Mathematical Components team