We are proud to announce the immediate availability of the Mathematical Components library version 2.5.0.
The webpage, and documentation, are available at https://math-comp.github.io/.
This release is compatible with Coq 8.20, 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
The contributors to this version are: Reynald Affeldt, Arthur Azevedo de Amorim, Alessandro Bruni, Cyril Cohen, Georges Gonthier, Florent Hivert, Enrico Tassi, Laurent Théry, Pierre Roux, Takafumi Saikawa, Kazuhiko Sakaguchi, Lynda Bentoucha, Quentin Vermande
We also wish to thank all the reviewers of the various contributions.
See Release The Mathematical Components Library 2.5.0 · math-comp/math-comp · GitHub
to download or see the CHANGELOG.md.
Packages for nix and opam are available.
Best regards,
–
The Mathematical Components team