Stream: Coq Platform devs & users

Topic: 2022.04.2

view this post on Zulip Andrew Appel (Jun 29 2022 at 17:21):

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.

view this post on Zulip Karl Palmskog (Jun 29 2022 at 17:40):

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?)

view this post on Zulip Karl Palmskog (Jun 29 2022 at 17:42):

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

view this post on Zulip Michael Soegtrop (Jun 29 2022 at 17:48):

@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).

view this post on Zulip Michael Soegtrop (Jun 29 2022 at 17:48):

Is there a good reason you can't use the 2022.09 beta picks?

view this post on Zulip Michael Soegtrop (Jun 29 2022 at 17:51):

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.

view this post on Zulip Andrew Appel (Jun 29 2022 at 18:05):

Why the Flocq3 hack turned out to be a big hassle:

  1. I have a new research project in formally verified numerical methods, with two new repositories that heavily use Flocq and Interval and VST. The new repos could have used Flocq3 or Flocq4, except that they must also be compatible with VST, which in turn must be compatible with CompCert; so they had to use Flocq3. When we submitted the paper for publication, one of the referees complained about difficulty building our Coq development; I'm suspect it was related to the Flocq3 hack.
  2. In day-to-day development of VST, based on master branch of CompCert. Since I'm not an opam wizard, I have no idea what trickery was used in order to get CompCert to build on top of Flocq3 in Coq Platform 2022.04. So I configured VST to build on top of a specially hacked external CompCert where Flocq3 was named explicitly. This worked, and we even got VST's CI to work on top of standard 2022.04 CompCert 3.10. But then when other contributors to VST wanted to build the master branch, we had to explain all this to them.
    So I will be very glad to leave Flocq3 behind, and build my repositories (VST, vcfloat, VerifiedLeapfrog) on top of a standard Coq platform of some sort.

view this post on Zulip Andrew Appel (Jun 29 2022 at 18:07):

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.
https://github.com/VeriNum/vcfloat/raw/master/doc/vcfloat2.pdf

view this post on Zulip Karl Palmskog (Jun 29 2022 at 18:17):

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.)

view this post on Zulip Michael Soegtrop (Jun 29 2022 at 18:25):

@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.

view this post on Zulip Andrew Appel (Jun 29 2022 at 18:32):

Regarding VCFloat2, there's no rush to get it into the Fall 2022 Platform.

view this post on Zulip Enrico Tassi (Jun 29 2022 at 19:38):

About mathcomp, I shoul work on a release tomorrow.

view this post on Zulip Enrico Tassi (Jun 30 2022 at 09:37):

The tag is out, I'll make opam packages this afternoon

view this post on Zulip Michael Soegtrop (Jun 30 2022 at 10:43):

I try to do a first 2022.09 beta early next week, but I am currently moving homes and can't promise

view this post on Zulip Théo Zimmermann (Jun 30 2022 at 14:32):

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).

view this post on Zulip Michael Soegtrop (Jun 30 2022 at 17:22):

I started this, but it was hard to test as long as mathcomp had no release. Let's see how it looks now.

view this post on Zulip Karl Palmskog (Jun 30 2022 at 17:23):

@Enrico Tassi can we merge the mathcomp package PR?

view this post on Zulip Enrico Tassi (Jun 30 2022 at 20:12):

sure, I was waiting for ci

Last updated: Jun 03 2023 at 03:01 UTC