Cyril Cohen (Nov 26 2020 at 10:59): Cyril Cohen (Nov 26 2020 at 10:59):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)
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
Cyril Cohen (Nov 26 2020 at 11:02):but coq dev passes
Enrico Tassi (Nov 26 2020 at 11:10):Cyril Cohen said:
I can't tell, Coq 8.13 is not released
yet
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 ?
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
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"))} ]
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
Cyril Cohen (Nov 26 2020 at 11:29):We can indeed commit to remove "dev" when it stops working
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
Cyril Cohen (Nov 26 2020 at 11:32):We'll update the opam repository when 8.13 becomes available
Cyril Cohen (Nov 26 2020 at 11:33):it does not really matterto me that the .opam files in the tgz are accurate
Cyril Cohen (Nov 26 2020 at 11:33):(btw a mistake got in, since we have >= 8.7 instead of >= 8.10)
Cyril Cohen (Nov 26 2020 at 11:33):I fixed master but not 1.12.0,
Cyril Cohen (Nov 26 2020 at 11:34):not sure a 1.12.1 is needed to fix that...
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]
Karl Palmskog (Nov 26 2020 at 11:38):so I don't think a 1.12.1 is needed for that reason
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?
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)
Cyril Cohen (Nov 26 2020 at 11:42):(and maybe a few other exceptions that I expect not to occur very often)
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)
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.
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