*(cross-posted to Coq users, please followup to math-comp users (here))*

We are proud to announce the immediate availability of the

Mathematical Components library version 1.11.0.

This release is compatible with Coq 8.7, 8.8, 8.9, 8.10, 8.11.

The main improvement introduced by this release is the introduction of

order structures. The change should mostly be visible by users of ssrnum.

Version 1.11.0 fixes a problem of 1.11+beta1 so that we allow again

min and max to work a partial order instead of a total order.

The contributors to this version are: Antonio Nikishaev, Anton Trunov,

Assia Mahboubi, Christian Doczkal, Cyril Cohen, Enrico Tassi, Erik

Martin-Dorel, Florent Hivert, Kazuhiko Sakaguchi, Pierre-Marie Pédrot,

Pierre-Yves Strub, Reynald Affeldt, Simon Boulier, Yves Bertot.

We also wish to thank all the reviewers of the various contributions.

See https://github.com/math-comp/math-comp/releases/tag/mathcomp-1.11.0

to download or see the `CHANGELOG.md`

.

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

Best regards,

--

The Mathematical Components team

All the mathcomp 1.11.0 packages are now out on OPAM (after running `opam update`

), e.g., `coq-mathcomp-ssreflect.1.11.0`

, `coq-mathcomp-algebra.1.11.0`

, etc.

Now would be a good time to to update all OPAM packages that use mathcomp in some way and are compatible with 1.11.0 to use correct/latest version requirements. Sadly we don't have that kind of automation yet.

Last updated: Jul 15 2024 at 20:02 UTC