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

The webpage, and documentation, are available at https://math-comp.github.io/.

This release is compatible with Coq 8.10, Coq 8.11, and Coq 8.12.

The main changes are:

- support for Coq 8.7, 8.8, and 8.9 have been dropped,
- a change of implementation of intervals and the updated theory,
- the addition of kernel lemmas for matrices,
- generalized many lemmas for path and sorted,
- several lemma additions, name changes and bug fixes.

The contributors to this version are: Anton Trunov, Christian Doczkal, Cyril Cohen, Enrico Tassi, Erik Martin-Dorel, Jasper Hugunin, Kazuhiko Sakaguchi, Laurent Théry, Reynald Affeldt, and 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.12.0

to download or see the `CHANGELOG.md`

.

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

Best regards,

--

The Mathematical Components team

This message was cross posted to the streams #math-comp users and #Coq users , please follow up on #math-comp users (here)

Gaëtan Gilbert said:

no 8.13?

I can't tell, Coq 8.13 is not released

but coq dev passes

Cyril Cohen said:

I can't tell, Coq 8.13 is not released

yet

It should work. I don't think we already have a docker image tracking v8.13 for CI, do we @Erik Martin-Dorel ?

@Enrico Tassi see discussion about this here: https://coq.zulipchat.com/#narrow/stream/237656-Coq-devs.20.26.20plugin.20devs/topic/8.2E13.20release.20thread/near/217471240

@Cyril Cohen can you commit to monitor that `1.12.0`

builds with Coq `master`

over time and change the opam package when it stops doing so? I'm thinking of the following in the OPAM package:

```
depends: [ "coq" { ((>= "8.7" & < "8.13~") | (= "dev"))} ]
```

since `released`

is supposed to be self-contained, `dev`

is essentially a black box where anyone can insert anything, but I guess it's fine if you have CI stuff running

We can indeed commit to remove "dev" when it stops working

by the way, there is a `8.13.dev`

package in `core-dev`

, so you can apply the same principle and have `< "8.14~"`

if you want

We'll update the opam repository when 8.13 becomes available

it does not really matterto me that the .opam files in the tgz are accurate

(btw a mistake got in, since we have >= 8.7 instead of >= 8.10)

I fixed master but not 1.12.0,

not sure a 1.12.1 is needed to fix that...

yeah, from opam archive side we don't care about those [accuracy of the opam data in the tgz]

so I don't think a 1.12.1 is needed for that reason

are there any ideas about how backwards-compatible 1.12 is? Will everything break or should we try to check packages that use 1.11 if they work?

Everything is supposed to work as before, with a few exceptions (use of the internals of `interval.v`

and a few constants that were buggy before and thus got fixed without deprecation step)

(and maybe a few other exceptions that I expect not to occur very often)

of course, if you depend on more than mathcomp, you have to wait for (or contribute to) your dependencies to be released. (knowing that all the ones in our CI pass and could be released as such)

my point was something like: "third-party" packages like `coq-reglang`

might work out-of-the box with 1.12, so all one might need to do is to change the bound in the opam package for the latest release.

probably, unless you already did that the last time, and you used deprecated symbols from 1.10.0 that just got removed :wink:

Last updated: Feb 08 2023 at 04:04 UTC