Stream: math-comp devs

Topic: real-closed for MC 2.0


view this post on Zulip Karl Palmskog (Aug 21 2023 at 14:36):

is there any chance of a release of real-closed for MC 2.0? Recall that this will be needed for the Platform, so if we do this "sooner" there will be less work "later".

view this post on Zulip Pierre Roux (Aug 21 2023 at 14:47):

AFAIR the master branch is ready and a release is all I'm waiting to release CoqEAL. But I guess this was mostly forgotten, @Cyril Cohen ?

view this post on Zulip Karl Palmskog (Aug 21 2023 at 14:50):

in the meantime, I can at least increase the upper Coq bound for multinomials 2.0.0 to include 8.18

view this post on Zulip Karl Palmskog (Aug 28 2023 at 11:24):

a small bump here since Cyril confirmed this was simply forgotten about, I can do the packaging if someone does the tag

view this post on Zulip Cyril Cohen (Aug 28 2023 at 13:02):

The only "problem" is that the CI is completely broken right now. I am still on vacation and will not be able to perform any test until Friday. But if anyone can swear that master works fine within a certain range of Coq/mathcomp version, I'm ok with tagging blindly.

view this post on Zulip Karl Palmskog (Aug 28 2023 at 13:04):

unless someone beats me to it, I will check with 8.16 to 8.18 and MC 2.0.0 tonight and report here

view this post on Zulip Pierre Roux (Aug 28 2023 at 13:40):

I try to update the CI there https://github.com/math-comp/real-closed/pull/56 let's see what happens

view this post on Zulip Pierre Roux (Aug 28 2023 at 14:20):

So CI shows it compiles fine with 8.16, 8.17 and master with MC 2.0.0, but doesn't test 8.18+rc1 currently.

view this post on Zulip Karl Palmskog (Aug 28 2023 at 14:27):

I can confirm current real-closed master (ec11936) works on 8.18+rc with MC 2.0.0 and coq-mathcomp-bigenough.1.0.1

view this post on Zulip Karl Palmskog (Sep 01 2023 at 12:31):

@Cyril Cohen just a reminder that if you (possibly blindly) tag real-closed ec11936 I will take care of packaging

view this post on Zulip Cyril Cohen (Sep 01 2023 at 14:16):

tagged!
Sorry for the delay and thanks!


Last updated: Nov 29 2023 at 22:01 UTC