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".
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 ?
in the meantime, I can at least increase the upper Coq bound for multinomials 2.0.0 to include 8.18
a small bump here since Cyril confirmed this was simply forgotten about, I can do the packaging if someone does the tag
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.
unless someone beats me to it, I will check with 8.16 to 8.18 and MC 2.0.0 tonight and report here
I try to update the CI there https://github.com/math-comp/real-closed/pull/56 let's see what happens
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.
I can confirm current real-closed
ec11936) works on 8.18+rc with MC 2.0.0 and
@Cyril Cohen just a reminder that if you (possibly blindly) tag real-closed
ec11936 I will take care of packaging
Sorry for the delay and thanks!
Last updated: Nov 29 2023 at 22:01 UTC