I plan to do a Coq Platform preview release for Coq 8.15 tomorrow. It currently is on math-comp 1.13. If you want me to update to 1.14, please leave a comment at (https://github.com/math-comp/math-comp/issues/843)

Michael Soegtrop said:

I plan to do a Coq Platform preview release for Coq 8.15 tomorrow. It currently is on math-comp 1.13. If you want me to update to 1.14, please leave a comment at (https://github.com/math-comp/math-comp/issues/843)

Thanks for the notification, we will discuss tomorrow at the mathcomp meeting.

Did you come to a conclusion? If this is controversial, I would suggest to go with 1.13 in the beta und switch to 1.14 for the final release schedules end of February.

Michael Soegtrop said:

Did you come to a conclusion? If this is controversial, I would suggest to go with 1.13 in the beta und switch to 1.14 for the final release schedules end of February.

Dear @Michael Soegtrop, I made a mistake, the mathcomp meeting is tomorrow morning. AFAIK, 1.14 was released especially for the Coq plateform and is a minor (yet with two possibly breaking changes), and it should work with every reverse dependency I know of, so it would be a shame not to include it in the beta.

Yes, we released .14 now so that all additions would available on coq 8.15 and its platform.

Fine, I will switch then. Could you please leave an official statement in (https://github.com/math-comp/math-comp/issues/843)?

from the MathComp userspace side, I think 1.14 has been the least trouble I've had when upgrading, but then it's a quite small increment from 1.13, which tended to be a bit of work...

Last updated: Feb 27 2024 at 22:02 UTC