Stream: math-comp users

Topic: MathComp 1.12.0 released


view this post on Zulip Cyril Cohen (Nov 26 2020 at 10:59):

MathComp 1.12.0 released

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:

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)

view this post on Zulip Cyril Cohen (Nov 26 2020 at 11:02):

Gaëtan Gilbert said:

no 8.13?

I can't tell, Coq 8.13 is not released

view this post on Zulip Cyril Cohen (Nov 26 2020 at 11:02):

but coq dev passes

view this post on Zulip Enrico Tassi (Nov 26 2020 at 11:10):

Cyril Cohen said:

I can't tell, Coq 8.13 is not released

yet

view this post on Zulip Enrico Tassi (Nov 26 2020 at 11:11):

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

view this post on Zulip Karl Palmskog (Nov 26 2020 at 11:17):

@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

view this post on Zulip Karl Palmskog (Nov 26 2020 at 11:24):

@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"))} ]

view this post on Zulip Karl Palmskog (Nov 26 2020 at 11:26):

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

view this post on Zulip Cyril Cohen (Nov 26 2020 at 11:29):

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

view this post on Zulip Karl Palmskog (Nov 26 2020 at 11:32):

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

view this post on Zulip Cyril Cohen (Nov 26 2020 at 11:32):

We'll update the opam repository when 8.13 becomes available

view this post on Zulip Cyril Cohen (Nov 26 2020 at 11:33):

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

view this post on Zulip Cyril Cohen (Nov 26 2020 at 11:33):

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

view this post on Zulip Cyril Cohen (Nov 26 2020 at 11:33):

I fixed master but not 1.12.0,

view this post on Zulip Cyril Cohen (Nov 26 2020 at 11:34):

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

view this post on Zulip Karl Palmskog (Nov 26 2020 at 11:34):

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

view this post on Zulip Karl Palmskog (Nov 26 2020 at 11:38):

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

view this post on Zulip Karl Palmskog (Nov 26 2020 at 11:39):

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?

view this post on Zulip Cyril Cohen (Nov 26 2020 at 11:41):

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)

view this post on Zulip Cyril Cohen (Nov 26 2020 at 11:42):

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

view this post on Zulip Cyril Cohen (Nov 26 2020 at 11:43):

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)

view this post on Zulip Karl Palmskog (Nov 26 2020 at 11:47):

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.

view this post on Zulip Cyril Cohen (Nov 26 2020 at 11:48):

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