Pierre-Marie Pédrot (Apr 27 2022 at 20:37): Pierre-Marie Pédrot (Apr 27 2022 at 20:37):Do we both need Flocq3 and Flocq4 to be installed?
Gaëtan Gilbert (Apr 27 2022 at 20:51):we're already installing flocq3
Gaëtan Gilbert (Apr 27 2022 at 20:51):it just calls itself flocq
Pierre-Marie Pédrot (Apr 27 2022 at 20:51):Why doesn't it find it then?
Pierre-Marie Pédrot (Apr 27 2022 at 20:52):Ah but that's the whole flocq3 vs flocq4 split then
Michael Soegtrop (Apr 28 2022 at 07:03):I fear the Flocq3 opam package lives in Coq Platform only for now - we didn't finally discuss if we want it in public opam afair.
See https://github.com/coq/platform/tree/main/opam/opam-coq-archive/released/packages.
@Karl Palmskog : should I push it upstream?
Michael Soegtrop (Apr 28 2022 at 07:04):I think what I should do is to push upstream coq-flocq3 but not the flocq3 variants of coq-interval and coq-gappa.
Karl Palmskog (Apr 28 2022 at 07:09):@Michael Soegtrop I think I've said before that it's fine to put it in the Coq opam archive (assuming it's fine with Guillaume).
Karl Palmskog (Apr 28 2022 at 07:10):generally, I think it's good to have Platform packages also available in the general archives, unless there is technical reason not to
Guillaume Melquiond (Apr 28 2022 at 07:22):Just to be clear, that will not solve the CI issue at all, since the CI does not depend on the Opam packages.
Michael Soegtrop (Apr 28 2022 at 07:26):@Guillaume Melquiond : can you please have a quick look at (https://github.com/coq/platform/tree/main/opam/opam-coq-archive/released/packages) and decide which of the flocq3 packages you want to have in the Coq main opam repo?
IMO coq-flocq3 should definitely be there, but I am not so sure about the flocq3 variants of coq-interval and coq-gappa. Afaik the user base which requires a CompCert compatible coq-interval and coq-gappa is not that large and likely uses Coq Platform. And I find it slightly polluting to put all these packages there for a temporary work around.
Michael Soegtrop (Apr 28 2022 at 07:28):On the other hand I would have to keep them in Coq Platform forever otherwise - since the plan is to not drop any release package pick for quite some time.
Guillaume Melquiond (Apr 28 2022 at 07:36):In my opinion, none of these packages have their place in the main repository. What would be the benefit for a user of the main repository (rather than a user of the platform) to install coq-flocq3 instead of coq-flocq=3? Sure, it means they can install both coq-flocq3 and coq-flocq. But why would they want to do that?
Guillaume Melquiond (Apr 28 2022 at 07:37):(In particular, what makes Flocq different from other packages?)
Karl Palmskog (Apr 28 2022 at 07:39):I thought the argument was that people would be able to use VST+Flocq3 for one project, while using Flocq.4 in another (in the same switch)
Guillaume Melquiond (Apr 28 2022 at 07:41):Sure, but why would they want to use Flocq 4 in that case? It means that they need a feature of Flocq that is part of Flocq 4 but not of Flocq 3. So, tell me, which feature is it? I honestly do not know.
Michael Soegtrop (Apr 28 2022 at 07:46):The main reason this was done - and it was actually suggested by you - is to encourage people to move their own stuff to Flocq4 while they are using CompCert + VST.
I e.g. do have quite a bit of Flocq code which is independent of whatever Flocq is used in CompCert, because its interface is via R. This code already used Flocq4, while I am using a Flocq3 based CompCert - all in a single development.
Michael Soegtrop (Apr 28 2022 at 07:48):Interestingly I am using both, a Flocq4 and a Flocq3 based coq-gappa in the same development. I am mostly using the Flocq4 based one, because I reason about R stuff with it, but in some rare cases I also reason about CompCert floats and then I am using the Flocq3 based gappa.
Michael Soegtrop (Apr 28 2022 at 07:49):But again, I expect that the handful of people up to such things is using Coq Platform.
Michael Soegtrop (Apr 28 2022 at 07:52):If in hindsight it wouldn't have been smarter to wait for the CompCert port is a different story.
As mentioned a few times, I also did this to prototype this - we will have such situations in the future where waiting might not be a viable alternative. And all the effects are not so easy to foresee - I think it was worthwhile to see how this works out and to have exactly those discussions we are having right now - before we are in a situation where we really need a solution.
Guillaume Melquiond (Apr 28 2022 at 07:52):Michael Soegtrop said:
Interestingly I am using both, a Flocq4 and a Flocq3 based coq-gappa in the same development. I am mostly using the Flocq4 based one, because I reason about R stuff with it, but in some rare cases I also reason about CompCert floats and then I am using the Flocq3 based gappa.
But why? There is absolutely no difference between Gappa compiled with Flocq 3 and Gappa compiled with Flocq 4. (And I really mean "absolutely". If there was a way to disassemble .vo files, you would actually get the same thing. Gappa does not use the single file of Flocq that broke during the switch from Flocq 3 to Flocq 4.)
Michael Soegtrop (Apr 28 2022 at 07:55):Because this application of gappa interfaces with my own Flocq code, which is not Flocq3 / Flocq4 agnostic - although it likely would be easy to do.
But I didn't know upfront that from a user point of view the difference between Flocq3 and Flocq4 are trivial. The versioning doesn't suggest this and you also didn't mention this when we discussed this a while back (last year via email).
Guillaume Melquiond (Apr 28 2022 at 07:56):Michael Soegtrop said:
The main reason this was done - and it was actually suggested by you - is to encourage people to move their own stuff to Flocq4 while they are using CompCert + VST.
Sorry, I do not remember ever suggesting that. Here is the very last email I sent on the subject:
I have no idea what the platform installer looks like, so perhaps I will be writing some nonsensical things. But I assume that it does not install everything and let the users select what components they want. If so, would it be possible to propose both Flocq 3 and Flocq 4, both installed as plain Flocq? Obviously, they would be mutually exclusive, and selecting Flocq 4 would prevent installing CompCert (or make it use its vendored version of Flocq instead).
In that email, I do not suggest the name Flocq3. Quite the contrary.
Michael Soegtrop (Apr 28 2022 at 07:57):Hmm - let me search my emails ...
Michael Soegtrop (Apr 28 2022 at 08:05):In the same Email (the lines above) you wrote:
By the way, an additional drawback of mechanism 1 is that it might actually slow down the switch. Indeed, developments that start to use "From Flocq4 Require" will not be portable, so users might prefer to stick to the original Flocq. Perhaps it would be better to rename Flocq 3 instead.
I answered the same day:
Indeed it might be the better option to rename legacy Flocq to Flocq3 - I guess the amount of work is about the same since not so many developments directly import flocq (mine e.g. mostly do so via including coq-interval of coq-gappa).
I also mentioned that your assumption that the installers allow to choose - a prerequisite for your other suggestion - does not apply to MacOS and Snap, so I can't follow it.
Guillaume Melquiond (Apr 28 2022 at 08:59):Michael Soegtrop said:
In the same Email (the lines above) you wrote:
By the way, an additional drawback of mechanism 1 is that it might actually slow down the switch. Indeed, developments that start to use "From Flocq4 Require" will not be portable, so users might prefer to stick to the original Flocq. Perhaps it would be better to rename Flocq 3 instead.
Sure. But you are the one who suggested to rename Flocq to something else (namely, Flocq 4 to Flocq4). I never suggested any renaming in the first place. I just wrote that, if there shall be a renaming, it should be Flocq 3. That does not mean I thought renaming was a good idea. Till the very end, I kept suggesting solutions that would not involve any renaming. It is unfortunate you interpreted this email exchange as an agreement with a renaming.
Michael Soegtrop (Apr 28 2022 at 09:10):Well the other suggestions were not viable as I explained in the answer (they would require installers which allow to select between Flocq3 and Flocq4). For MacOS one could have made a Flocq3/Flocq4 selection with quite some effort, but for snap that is entirely impossible (afaik). I think I made this clear in my answer. I am not aware of any better option to deliver Flocq4 and CompCert in the 8.15.1 release.
We probably should have more discussed the option to simply delay delivery of Flocq4 - when we discussed this back then you didn't emphasize as much as you do today that there is from a user point of view very little difference between Flocq3 and Flocq4.
Anyway, things are now as they are, so please let's concentrate on the opam discussion. I am fine with keeping these packages in Coq Platform, since they can be considered as a Coq Platform specific solution.
Michael Soegtrop (Apr 28 2022 at 09:10):I am not so sure what Coq CI needs. If there are issues with testing VST in Coq CI, it might be possible to fix these in other ways.
Pierre-Marie Pédrot (Apr 28 2022 at 10:28):Regardless of the solution, the RM would like to kindly remind the whole audience that we're 2 weeks away from the branching of the 8.16. It'd be nice if we had a green CI on master by then...
Michael Soegtrop (Apr 28 2022 at 11:28):I can take care of the VST issue.
Michael Soegtrop (Apr 28 2022 at 11:33):What is the final conclusion on having coq-flocq3 + flocq3 patched CompCert / VST in the main opam repo (not the flocq3 variants of interval and gappa)? Please use up vote (put it in main opam) or downvote (don't put it in main opam).
The VST issues are transitional (Flocq3/Flocq4 porting) and will eventually go away but might be not that easy to fix meanwhile, but I didn't have a deeper look. I will discuss it with Andrew.
@Guillaume Melquiond @Karl Palmskog
Karl Palmskog (Apr 28 2022 at 11:35):my final conclusion is that the coq-flocq3 is welcome to be hosted in the Coq opam released repository, if someone submits it. But, we generally don't want to host packages against the will of the project maintainer. So if Guillaume says final "no" I think that's the end of it.
Karl Palmskog (Apr 28 2022 at 11:40):on the other hand, if Guillaume isn't actively against it, I would treat a coq-flocq3 PR as just another package PR and merge it when CI passes
Michael Soegtrop (Apr 29 2022 at 06:37):I am in discussions with Andrew on fixing the CI issues.
To conclude this discussion I would say we wait for pushing the packages upstream until someone says (s)he wants them. Since the packages are there and tested in Coq Platform this can be done very quickly.
Théo Zimmermann (Apr 29 2022 at 08:14):Just some piece of advice: next time such Platform packaging discussions need to take place, hold them on a public channel (GitHub issues or Zulip for instance) instead of through private email. Having more people able to be involved in the full discussion would give more chances to take into account every aspect of the problem in the discussion.
Last updated: Oct 08 2024 at 15:02 UTC