Please pick the version you prefer for Coq 8.14 in Coq Platform 2021.11 about reglang

[palmskog]

Here is the policy I propose we should use for the Coq Platform 2021.11 (please protest if you don't agree @chdoc):

• if 2021.11 is released with MathComp 1.12.0, go with coq-reglang.1.1.2 (we know this works with 8.14)
• if 2021.11 is released with the yet-to-appear MathComp 1.13.0, we will do a new release 1.1.3 guaranteed to work with 8.14 and 1.13.0 to go in the platform

[chdoc]

I basically agree. In particular, we expect mathcomp.1.13.0 to be released in time for 2021.11. I haven't yet tried to build reglang.1.1.2 against the current mathcomp master branch, but if that compiles, then I'm fairly certain that this will also be true for 1.13.0 as there are no more breaking changes planned. Looking at the commit log, there seem to be no changes to the code since the last release.

[MSoegtropIMC]

Just wanted to inform you that in Coq Platform 2021/09 I go with coq-reglang.1.1.2. I expect a new version of mathcomp in 2021/11.

[palmskog]

It was confirmed in coq/opam#1897 that coq-reglang.1.1.2 indeed works with MathComp 1.13.0. Hence, we can go with 1.1.2 for both the 8.13 and 8.14 Platform.

[MSoegtropIMC]

Thanks for the confirmation! I will close this issue then.