Will it be possible to have a Coq Platform 2022.04.2 with:
My own main motivation for wanting this is that the Flocq3 hack has turned out to be a major hassle, for reasons I could explain if anyone is interested.
At the same time, I want to mention that with VST 2.10, the VST master branch will now be based on "ordinary Flocq" (meaning Flocq 4.1), so whatever hacks (if any) the Coq development team had to add to their VST-as-a-test-case CI scripts, might need to be put back the way it was.
I think CompCert 3.11 is not out yet either? Based on previous discussions, I believe these kinds of version upgrades (CompCert 3.10 -> 3.11, VST 2.9 -> 2.10) would normally go in the next Platform release (slated for September/October?)
but we would need input from @Michael Soegtrop on whether my intuition is correct: a 20XY.Z.(n+1) release would normally be as close as possible in package versions to 20XY.Z.n, to not break compatibility
@Andrew Appel : this would more be the 2022.09 beta picks for 8.16 and 8.15. These are expected 1..2 weeks after a 8.16 release of mathcomp (afaik there was a meeting today to discuss when this happens - it is expected in the next days).
Is there a good reason you can't use the 2022.09 beta picks?
Of course I would be interested to learn about your experience with the Flocq3 hack - one of the motivations of doing this was to learn how we can handle such situations.
Why the Flocq3 hack turned out to be a big hassle:
By the way, within a few months I will be proposing a new addition to the Coq Platform:
VCFloat2: Floating-point Error Analysis in Coq, by Andrew W. Appel and Ariel E. Kellison.
might be good to open an issue about VCFloat2 addition early, if you want it to be part of the fall Platform release (with 8.16.0). If it's OK to wait until later than the fall Platform, then no rush.
(One example of a proposal of new package.)
@Andrew Appel : thanks for the summary. I guess a big part of the problem was that there was some misunderstanding between @Guillaume Melquiond and me on if we do this or not, which had the effect that I did it, but the respective opam packages were only available in Coq Platform and not in the main opam repo. If we ever do such a thing again, it definitely must be better aligned between all stake holders and we either do it globally or not at all.
Regarding VCFloat2, there's no rush to get it into the Fall 2022 Platform.
About mathcomp, I shoul work on a release tomorrow.
The tag is out, I'll make opam packages this afternoon
I try to do a first 2022.09 beta early next week, but I am currently moving homes and can't promise
In the end, did you manage to prepare the script to inform package maintainers when dependencies are compatible? If not, maybe now is a good time to open the standard issues (to give a chance to maintainers to say whether they recommend a specific version or want to make a new compatibility release).
I started this, but it was hard to test as long as mathcomp had no release. Let's see how it looks now.
@Enrico Tassi can we merge the mathcomp package PR?
sure, I was waiting for ci
Last updated: Jan 30 2023 at 10:03 UTC