Stream: math-comp users

Topic: Coq Platform 2021.11 preparation


view this post on Zulip Michael Soegtrop (Nov 15 2021 at 10:43):

It is part of the Coq Platform concept to agree with package authors on which version to include in each version of Coq Platform, so I create issues for each included packages to discuss this. For a few mathcomp extension packages - apparently all by @Cyril Cohen - I don't have a feedback as yet if the latest version is fine or of there might be a new release soon (as is the case for mathcomp-analysis for example).

The corresponding packages and issues are:

Since all packages compile fine with 8.14 this is just a formality - if I don't hear back I will simply use the latest version - but I still would like to put my "agreed with author stamp" on these packages.

view this post on Zulip Karl Palmskog (Nov 15 2021 at 10:46):

I would probably read this merged PR as defining the versions of those packages that are 1.13 and 8.14 approved: https://github.com/coq/opam-coq-archive/pull/1891/files

view this post on Zulip Michael Soegtrop (Nov 15 2021 at 10:51):

@Karl Palmskog : as far as I can see this PR is about the main mathcomp packages - which all have the same version numbers - and does not include the 3 extension packages I mentioned above.

view this post on Zulip Karl Palmskog (Nov 15 2021 at 10:52):

the PR includes updates to both finmap.1.5.1 and real-closed.1.1.2

bigenough has not received updates in ages.

view this post on Zulip Cyril Cohen (Nov 15 2021 at 13:03):

Dear @Michael Soegtrop, none of these package evolved since their last release, only the meta data, CI and local opam files have been changed. If the plateform is compiling with the current versions, then all is fine. I'm very sorry for my latency and I hope everything else is going fine.

view this post on Zulip Michael Soegtrop (Nov 15 2021 at 13:16):

Dear @Cyril Cohen : thanks and no issue at all!


Last updated: Feb 08 2023 at 07:02 UTC