Michael Soegtrop (Mar 25 2022 at 12:50): Michael Soegtrop (Mar 25 2022 at 12:50):I discussed with @Guillaume Melquiond to do the following regarding the not compatible Flocq 3.x / Flocq 4.x versions:
The main reason I am doing this is to encourage users to use Flocq 4.X, which I think will be much easier this way.
Also it is a bit of a prototype for handling such situations in the future and likely worth the experience.
Michael Soegtrop (Mar 25 2022 at 14:22):@Karl Palmskog : what is your opinion on having the required opam packages (coq-flocq3, coq-compcert.3.10~flocq3 and a coq-vst patch to allow this compcert version) upstream?
You can have a look here: (https://github.com/coq/platform/tree/main/opam/opam-coq-archive/released/packages)
Karl Palmskog (Mar 25 2022 at 14:23):the main awkwardness I see is that there would be two CompCert version 3.10, with no obvious way to tell them apart for regular users.
Michael Soegtrop (Mar 25 2022 at 14:23):A nicer description?
Karl Palmskog (Mar 25 2022 at 14:25):my preference would be that the CompCert 3.10 that depends on the flocq3 package completely replaces the other one. But I guess not up to me in the end.
Michael Soegtrop (Mar 25 2022 at 14:25):Users which don't ask for explicitly would get coq-compcert.3.10 which then drags in coq-flocq3.x - rather than coq-flocq3.3.x.
Michael Soegtrop (Mar 25 2022 at 14:26):Removing the usual CompCetr package might impact users which verify C code containing Flocq3 FP stuff.
Michael Soegtrop (Mar 25 2022 at 14:27):Hmm well, not really - all they have to do would be to rename their requires as well.
Karl Palmskog (Mar 25 2022 at 14:27):so coq-flocq3.X and coq-flocq.3.X are not equivalent? That's even more confusing....
Michael Soegtrop (Mar 25 2022 at 14:28):They are equivalent, except that they install into different logical paths.
Michael Soegtrop (Mar 25 2022 at 14:29):That is Flocq3 vs Flocq - in the new world Flocq is reserved for Flocq 4.X
Michael Soegtrop (Mar 25 2022 at 14:30):I am open to chaging the existing flocq 3.X packages to install into Flocq3, but I found this a bit too agrressive - it might break a lot of code even it is trivial to fix by renaming requires.
Karl Palmskog (Mar 25 2022 at 14:31):I don't mind coq-flocq.3.X and coq-flocq3.X co-existing, the main big confusion is about having two CompCerts with the same version number, and only one of them supporting VST...
Michael Soegtrop (Mar 25 2022 at 14:32):@Guillaume Melquiond : what is your opinion on either:
Karl Palmskog (Mar 25 2022 at 14:32):so if you want my opinion, I'm not fond of this at all [two CompCert 3.10 + one supporting VST], but if the developers and packagers declare that they want this, it will be merged in the end...
Michael Soegtrop (Mar 25 2022 at 14:33):Both support the same VST - VST doesn't really mind where Flocq is
Michael Soegtrop (Mar 25 2022 at 14:34):So you would prefer to change the existing flocq packages?
Michael Soegtrop (Mar 25 2022 at 14:34):See VST
Karl Palmskog (Mar 25 2022 at 14:34):OK, so at least you made VST agnostic to the CompCert, I guess this is one good thing
Michael Soegtrop (Mar 25 2022 at 14:35):It might be possible to have only one CompCert package and make the patch dependent on if a coq-flocq3 package is there.
Michael Soegtrop (Mar 25 2022 at 14:35):I think I have seen such hackery in some packages (equations?)
Karl Palmskog (Mar 25 2022 at 14:36):that would be a much better solution in my view (using opam depopts?).
Michael Soegtrop (Mar 25 2022 at 14:36):Could you help me with this?
Michael Soegtrop (Mar 25 2022 at 14:38):I am AFK for an hour or so - let's continue later. But I agree that an "auto patch" CompCert package would be substantially more elegant.
Karl Palmskog (Mar 25 2022 at 14:38):I can take a look at other similar packages with depopts in the archive and recommend some idiom, but I can't drop things and jump to it just this minute, possibly late tonight
Michael Soegtrop (Mar 25 2022 at 14:38):No issue - if you don't do this every other day yourself, I can also look it up.
Karl Palmskog (Mar 25 2022 at 14:39):I know one package that does this: https://github.com/coq/opam-coq-archive/blob/master/released/packages/coq-relation-algebra/coq-relation-algebra.1.7.7/opam#L14
Karl Palmskog (Mar 25 2022 at 14:40):but I haven't seen how one can do conditional patching
Karl Palmskog (Mar 25 2022 at 14:41):another one: https://github.com/coq/opam-coq-archive/blob/master/released/packages/coq-graph-theory/coq-graph-theory.0.9/opam#L20
Karl Palmskog (Mar 25 2022 at 14:51):according to the manual, one should be able to conditionally apply patches:
Patches may be applied conditionally by adding filters.
So maybe something like:
patches: [ "0001-Rename-Flocq-to-Flocq3.patch" {coq-flocq3:installed} ]
given that you also have:
depopts: ["coq-flocq3"]
I might be missing something. But if we are talking about having patched versions of CompCert in the platform, why not just apply the patch that converts CompCert to Flocq 4? https://github.com/AbsInt/CompCert/pull/368 (Only the parts in the lib and extraction directories matter, since the point is to use an external Flocq.)
Karl Palmskog (Mar 25 2022 at 15:50):why not just apply the patch that converts CompCert to Flocq 4
This would also be a good solution in my book, if Xavier is fine with it.
Michael Soegtrop (Mar 25 2022 at 16:49):@Guillaume Melquiond : this would be against Coq Platform policy to publish as much as possible what the authors release. Changing the logical path in a require statement from Flocq to Flocq3 does not change functionality in any way. Changing Flocq3 with Flocq4 is (I guess) a non trivial change and should be approved and released by @Xavier Leroy.
Guillaume Melquiond (Mar 25 2022 at 16:53):But then, do not even bother using Flocq 3, just use the version of Flocq vendored with CompCert. That way, you do not even have to patch CompCert and it will be fully compatible with Flocq 4 (by not using it).
Michael Soegtrop (Mar 25 2022 at 16:59):That also doesn't work, because it would make the definitions of floats in CompCert incompatible with definitions of floats elsewhere, and we can't even control it via opam restrictions because we know nothing about it.
This is connected with the question if we should have a gappa for Flocq3 to prove properties of float C programs.
Michael Soegtrop (Mar 25 2022 at 16:59):My plan is to at least have a Flocq 3 compatible gappa, but not to install it by default, but I would like to hear your opinion on it.
Michael Soegtrop (Mar 25 2022 at 17:00):I had btw. in the past a lot of trouble with CompCert bundling Flocq and resulting version incompatibilities - more or less one of the reasons d'être of Coq Platform.
Guillaume Melquiond (Mar 25 2022 at 17:03):Michael Soegtrop said:
My plan is to at least have a Flocq 3 compatible gappa, but not to install it by default, but I would like to hear your opinion on it.
So, your plan is to patch Flocq, CompCert, and Gappa, so that they all use the logical path Flocq3. But you could also patch only Gappa so that it uses the logical path compcert.flocq. The latter feels a lot less invasive.
Michael Soegtrop (Mar 25 2022 at 17:04):Except that it is not just gappa using Flocq and requiring to be compatible with CompCert.
Guillaume Melquiond (Mar 25 2022 at 17:05):So, how many libraries do you intend to patch to make them use Flocq 3?
Michael Soegtrop (Mar 25 2022 at 17:05):Besides, I think you should define what version of Flocq is in Coq Platform and not Xavier.
Michael Soegtrop (Mar 25 2022 at 17:06):So, how many libraries do you intend to patch to make them use Flocq 3?
In Coq Platform only Gappa and CompCert - but I e.g. also have my own stuff. And the patch is quite trivial.
Guillaume Melquiond (Mar 25 2022 at 17:06):Yes, that is why I think the only version in the Platform should be Flocq 4, and CompCert should be using its vendored Flocq.
Michael Soegtrop (Mar 25 2022 at 17:08):That's more or less what I am doing, except that I can't have it that I have a Flocq in Coq Platform used by other packages and defined by CompCert. If Flocq would be completely internal to CompCert things would be different. But if several packages need to share a version of Flocq, Coq Platform needs to be aware / control what this version is.
Michael Soegtrop (Mar 25 2022 at 17:20):But as I said above - this is also partly an exercise / simpler test scenario to test if one can handle this in this way and how much effort it is.
Michael Soegtrop (Mar 25 2022 at 17:21):I am sure we will have similar issues in the future, and we should know upfront how to handle them.
Théo Zimmermann (Mar 25 2022 at 18:08):It would be good to hear from Xavier if the patch fixing compatibility with Flocq4 is OK with him and if he would approve then having an opam package compcert.3.10~flocq4 that applies it. That would really be the nicest solution since it would avoid having to distribute multiple versions of a given package (which is something that we should strive to avoid).
Michael Soegtrop (Mar 25 2022 at 19:02):Having a compcert.3.10~flocq4 would be slightly preferable, but not that much. With the depopt trick I discussed with Karl it is indeed possible to have only one coq-compcert.3.10 package, which needs either coq-flocq.3.x or cpq-flocq3.3.x and adjusts itself to which one is there. I find this reasonably elegant.
The advantage of compcert.3.10~flocq4 would of course be that we could get rid of Flocq3, but I see both paths as reasonable.
Michael Soegtrop (Mar 25 2022 at 19:03):As you say, @Xavier Leroy should decide this.
Michael Soegtrop (Mar 28 2022 at 08:42):In case someone want's to have a look, Coq Platform main now has Flocq3 / Flocq4 separation as discussed. There is only one CompCert version, which auto adjusts to the availability of coq-flocq3 and requires either coq-flocq with a 3.X version or coq-flocq3. Down stream packages like VST don't need changes this way (there is also a VST patch, but it is unrelated and already available in the upstream opam repo). I can live with this solution or we have a Flocq4 CompCert - as discussed only @Xavier Leroy can decide this. If there is no Flocq4 CompCert endorsed by him, I plan to go with the solution currently in main, unless someone has very good reasons against this.
@Guillaume Melquiond : I am still unsure what to do with gappa. I can personally live with a Flocq4 based gappa without any code changes even when verifying C code, but my applications of gappa might be a bit non standard. Do you think I should provide - at least optionally) a coq-gappa-flocq3 package?
Michael Soegtrop (Mar 28 2022 at 08:56):I didn't have time as yet to look into what the differences between Flocq3 and Flocq4 are as yet and I wonder if the part of Flocq used in the interface of gappa is the same in Flocq3 and Flocq4.
Michael Soegtrop (Mar 28 2022 at 09:01):Btw.: there is yet another option: not having Flocq4 at all in Coq Platform 2022.03 and delay this to 2022.09. This decision would be with @Guillaume Melquiond. I am open to this, but would personally prefer the current solution - otherwise I for sure wouldn't look into Flocq4 before 2022.09.
Théo Zimmermann (Mar 28 2022 at 09:02):Yet another solution: make a "preview package pick" with Flocq4 instead of Flocq3 and CompCert patched to use Flocq4.
Michael Soegtrop (Mar 28 2022 at 09:21):An interesting question is if VST would compile at all with a Flocq4 CompCert - I didn't try this but I think it is unlikely (not extremely unlikely, though). If VST compiles with a Flocq4 CompCert, a preview would indeed make sense.
The nice side about the current mix solution is that people can adjust their code gradually - part of it using Flocq3 and part of it using Flocq4. This is possible because frequently the interface between modules is based on R and not on Flocq. An example is coq-interval which uses Flocq internally but its interface is R. This is my main rationale behind the current mix solution.
Xavier Leroy (Mar 28 2022 at 09:38):As discussed with @Michael Soegtrop over email, I'd rather not apply the big Flocq4-compatibility patch to the CompCert 3.10 package. I'd prefer if the package keeps using Flocq3.
I plan to switch CompCert to Flocq4 in version 3.11, later this Spring.
Michael Soegtrop (Mar 28 2022 at 10:14):Thanks for the confirmation @Xavier Leroy.
So the remaining options are:
Michael Soegtrop (Mar 28 2022 at 10:14): Michael Soegtrop (Mar 28 2022 at 10:15): Michael Soegtrop (Mar 28 2022 at 10:15): Michael Soegtrop (Mar 28 2022 at 10:15): Michael Soegtrop (Mar 28 2022 at 10:16):Please vote on the individual points (they are separate messages).
Michael Soegtrop (Mar 28 2022 at 10:22):@Karl Palmskog : a technical question on the CompCert opam package. Is the depopts line (https://github.com/coq/platform/blob/77aba354c68b9534b496f666c55ee53e2a545d45/opam/opam-coq-archive/released/packages/coq-compcert/coq-compcert.3.10/opam#L40)
required? I guess
(https://github.com/coq/platform/blob/77aba354c68b9534b496f666c55ee53e2a545d45/opam/opam-coq-archive/released/packages/coq-compcert/coq-compcert.3.10/opam#L37)
is sufficient.
Karl Palmskog (Mar 28 2022 at 10:24):if you do it that way, sure, you can skip the depopt. But just remember to make coq-flocq and coq-flocq3 conflicting
Karl Palmskog (Mar 28 2022 at 10:25):otherwise, we can probably get some really weird behavior...
Michael Soegtrop (Mar 28 2022 at 10:26):Making coq-flocq and coq-flocq3 conflicting would be quite contrary to the point. The idea is to install both - usually coq-flocq.4, but I don't see why this would be required.
Michael Soegtrop (Mar 28 2022 at 10:27): Ali Caglayan (Mar 28 2022 at 10:27):How would you import flocq3 vs flocq4 in a .v file if they are both installed?
Michael Soegtrop (Mar 28 2022 at 10:28):coq-flocq3 installs to log path Flocq3 - that's the difference.
Michael Soegtrop (Mar 28 2022 at 10:29):In Coq Platform main, the coq-compcert package has a conditional patch on the Requires. If coq-flocq3 is there, they are patched to Flocq3, otherwise not.
Karl Palmskog (Mar 28 2022 at 10:29):in that case, it's not obvious to me that one would want to "prioritize" flocq3
Andrew Appel (Mar 28 2022 at 10:30):I am now a heavy user of Flocq, not only in VST but also as the maintainer of the vcfloat package, and right now I'm writing extensions to vcfloat/interval that depend heavily on the semantics of Flocq floating point. Today is the first time I've heard of Flocq4. I'm not sure which channel I should have been watching to find out about it. All of my packages (VST, VCfloat, etc.) will (presumably) require significant porting to flocq4. VST is in the Coq platform, VCfloat is not, so here I'm speaking as a user of the Platform as much as I'm speaking as a package provider.
The Coq 8.15 beta package pick had flocq3. Therefore the main release should have flocq3. It is inappropriate to switch major versions in between the beta and the main pick. I would be happy to see flocq4 in the package (named flocq4), so that users could experiment with it. In the next package release after this one I would be happy to see flocq4 named flocq, and flocq3 disappear.
Michael Soegtrop (Mar 28 2022 at 10:31):I would like to make coq-flocq3 conflicting with coq-flocq.3.x but I am not sure how one would do this.
Andrew Appel (Mar 28 2022 at 10:32):And by the way, my comments about "don't make incompatible changes between the beta and the release" also apply to Gappa and Interval. Please.
Karl Palmskog (Mar 28 2022 at 10:33):I think it should be possible to add a conflict clause with some filter to get coq-flocq3.X to not be installable together with coq-flocq.3.X. But as Michael points out, depending on packages evolve, we may or may not want to do this...
Michael Soegtrop (Mar 28 2022 at 10:34):@Andrew Appel : the main rationale behind introducing Flocq4 in log path Flocq was that it would be quite an effort to switch it later while this way Floqc3 would just phase out. It should be quite easy to patch the require statements in projects still requiring Flocq3.
Karl Palmskog (Mar 28 2022 at 10:34):we could also add a "virtual" package akin to coq-native to let people choose their Flocq package (conf-flocq3?)
Michael Soegtrop (Mar 28 2022 at 10:38):E.g. what it takes to adjust CompCert to this is:
https://github.com/coq/platform/blob/main/opam/opam-coq-archive/released/packages/coq-compcert/coq-compcert.3.10/files/0001-Rename-Flocq-to-Flocq3.patch
(which could also be done with sed as a conditional build step) and these two changes in opam:
https://github.com/coq/platform/blob/77aba354c68b9534b496f666c55ee53e2a545d45/opam/opam-coq-archive/released/packages/coq-compcert/coq-compcert.3.10/opam#L9
https://github.com/coq/platform/blob/77aba354c68b9534b496f666c55ee53e2a545d45/opam/opam-coq-archive/released/packages/coq-compcert/coq-compcert.3.10/opam#L37
Karl Palmskog (Mar 28 2022 at 10:38):as a general rule in the Coq opam archive, we don't remove packages, unless there is some technical problem. Adding and then removing coq-flocq3 could be a good approach in the Platform, but in my view it's not a good experience for general Coq opam archive users
Michael Soegtrop (Mar 28 2022 at 10:40):I don't say that the coq-flocq3 package has to be removed. I am just saying that people will stop using it. Which then indeed might be a hint that one wouldn't want to have it in the first place, but I don't see much of another option.
Karl Palmskog (Mar 28 2022 at 10:41):sure, but I was referring to Andrew's comment, specifically that he
would be happy to see flocq4 named flocq, and flocq3 disappear.
Karl Palmskog (Mar 28 2022 at 10:42):so I just double check that "disappearing" would probably mean "removed from Platform scripts" (and not necessarily from opam archive)
Andrew Appel (Mar 28 2022 at 10:53):Regarding the exact mechanism, I withdraw any technical suggestion. My main point is that it is not appropriate to make an incompatible change between the beta and the main release of a given Coq Platform, at the last minute.
Michael Soegtrop (Mar 28 2022 at 11:24):The question is how we do the move in the smoothest way. CompCert is planned to move to Flocq4 in the next release, so the next release of Coq Platform (around 2022.09) will have a Flocq4 based CompCert. The question is what can we do now to make this transition as smooth as possible. I don't think that just letting things happen is the best approach. I also don't think that a big bang switch would be the smoothest solution, but I am snot sure.
Michael Soegtrop (Mar 28 2022 at 11:26):I still think that the dual Flocq solution is a very good approach, and I also think that the effort of changing the requires statements is quite minor. The version of coq-interval and gappa are the same as in the beta, they are just using Flocq4. For coq-interval this should not make any difference for the user. For gappa it might (for me personally it doesn't) and if this is the case, I would suggest to also supply a Flocq3 based gappa. So the incompatibility is only in how modules are named in require statements - IMHO this should be OK between a beta and a release.
Michael Soegtrop (Mar 28 2022 at 11:27):if we do nothing now, things might get much harder in 6 months.
Michael Soegtrop (Mar 28 2022 at 11:28):Having a Flocq4 preview pick, which then also includes the patched CompCert, as suggested by @Théo Zimmermann is also a reasonable option. The main downside of it is that I don't think it could have a VST then.
Michael Soegtrop (Mar 28 2022 at 11:29):I personally can do much more with a mixed solution than with a Flocq4 preview which does not have VST.
Andrew Appel (Mar 28 2022 at 11:57):Technically, it's not quite true that "for coq-interval this should not make any difference for the user". Contained within the internals of coq-interval, exported through the Coq module system, is a nice theory of concrete interval arithmetic on the floating point numbers. I have started to use this, and I was planning to (soon) discuss with Guillaume the idea of documenting it as one of the external interfaces of coq-interval. I'm also using the internal reified-Tree structure of Interval, to allow vcfloat to hand proof goals to interval without reflecting and reifying. In summary: there's more to a Coq package than a single API.
Paolo Giarrusso (Mar 28 2022 at 11:58):but AFAICT, the main proposal fulfills both wishes?
Paolo Giarrusso (Mar 28 2022 at 11:58):@Andrew Appel wrote > I would be happy to see flocq4 in the package (named flocq4), so that users could experiment with it.
Paolo Giarrusso (Mar 28 2022 at 12:03):Nevermind: AFAICT, there's consensus that VST/CompCert should use Flocq3, and there's debate on what coq-interval should use.
Théo Zimmermann (Mar 28 2022 at 12:45):I think Andrew's point on not changing things in major ways between a beta and a final release should really be heard. Furthermore, last minute changes are quite likely to introduce unforeseen behavior. So, I'm now thinking that all the main packages should really be made to depend on Flocq3 in the main package pick (even in the case where its namespace is patched to be Flocq3). The preview release could be used to either propose a fully Flocq4-based platform, or a dual-Flocq platform in case the main package pick is purely Flocq3-based.
Karl Palmskog (Mar 28 2022 at 13:41):I'm fine with packaging changes, as long as they can be approved by their respective maintainers, and also live in the opam archive for the long term. In particular, I hope we can avoid having several "version variants" of the same package, e.g., coq-package.5.3 and coq-package.5.3~variant, which is the most confusing and hard to maintain. At least coq-flocq and coq-flocq3 are different packages.
Andrew Appel (Mar 28 2022 at 13:49):I am informed that Flocq 4 was released on 5 November 2021. So the problem is not caused by a last-minute proposal for Flocq 4, it is caused by a delay in porting CompCert to the latest version of Flocq. Therefore I withdraw my objection to including Flocq 4 as the default Flocq for the Coq Platform. The proposal for Require Flocq3 as the old flocq, and Flocq as the new flocq-4, seems OK.
Michael Soegtrop (Mar 28 2022 at 16:15):I guess the main issue here is communication on my side - I am in discussion with Guillaume since a while on how to do the Flocq3 / Flocq4 transition. I should have said earlier that there are plans to switch to Flocq 4, but that there are technical difficulties.
Michael Soegtrop (Mar 28 2022 at 16:20):I had a private communication with Andrew and he agreed that the current proposal is the most reasonable under the given circumstances. He also thinks that VST has some proofs that likely need adjustments to Flocq4, so that it is unlikely that VST would compile with a CompCert patched for Flocq4. I think this excludes a separate Flocq4 preview build.
Michael Soegtrop (Mar 28 2022 at 16:24):Regarding the Flocq3 + Flocq vs Flocq + Flocq4 question: yes from a release management point of view Flocq + Flocq4 would be nicer, but from a long term perspective the Flocq3 + Flocq solution is less work.
Michael Soegtrop (Mar 28 2022 at 16:28):I will add a coq-interval-flocq3 and also a coq-gappa-flocq3 for thos who need it (Andrew said he definitely will need coq-interval-flocq3).
Michael Soegtrop (Mar 28 2022 at 16:29):@Karl Palmskog : do you think I should keep all flocq3 packages local to Coq Platform or push them upstream? I had a private communication with Xavier and he would be fine with pushing the coq-compcert.3.10 as now in Coq Platform main upstream. This would obviously require the coq-flocq3 package. I am not so sure about the flocq3 variants of coq-interval and coq-gappa.
Karl Palmskog (Mar 28 2022 at 17:09):@Michael Soegtrop if we can have a single CompCert 3.10 package definition, then I think you should upstream the flocq3 package
Michael Soegtrop (Mar 29 2022 at 09:09):@Karl Palmskog : OK, will do. How about coq-interval-flocq3 and coq-gappa-flocq3? I am 50/50 here for keepin git local - it really pollutes the name space but I don't see much of a different option either. Maybe we can have a "legacy" subfolder for such things (packages/legacy/flocq3, ...) - I think opam would find it there.
Théo Zimmermann (Mar 29 2022 at 09:12):Isn't it possible to also do it with a single package like for CompCert?
Michael Soegtrop (Mar 29 2022 at 09:17):@Théo Zimmermann : you mean having something like packages\coq-flocq\legacy\coq-flocq3.3.x?
Théo Zimmermann (Mar 29 2022 at 09:19):No.
Théo Zimmermann (Mar 29 2022 at 09:19):I'm not buying your "legacy" suggestion.
Théo Zimmermann (Mar 29 2022 at 09:20):I was rather suggesting to do for coq-interval and coq-gappa the same trick that you did for CompCert (if applicable).
Théo Zimmermann (Mar 29 2022 at 09:20):Especially given that this seemed to be the condition on which Karl thought that it was acceptable to upstream flocq3.
Michael Soegtrop (Mar 29 2022 at 09:20):This won't work, because you need both.
Théo Zimmermann (Mar 29 2022 at 09:20):Oh, that's right!
Michael Soegtrop (Mar 29 2022 at 09:21):As far as I understood Karl he was mostly against coq-compcert.3.10~flocq3.
Michael Soegtrop (Mar 29 2022 at 09:23):If I treat coq-interval like compcert, we get very close to having Flocq4, but nobody is using it. My goal is to use Flocq4 as much as possible, only those who need legacy Flocq can do so by explicitly saying so.
Michael Soegtrop (Mar 29 2022 at 09:25):So how about the legacy suggestion?
Théo Zimmermann (Mar 29 2022 at 09:25):I don't know enough about opam but I don't see how this would work.
Michael Soegtrop (Mar 29 2022 at 09:28):As far as I know opam doesn't care that much about the folder structure - only the leaf folder name counts. So one could clean up the package folder tree a bit by doing a subfolder "legacy" and put legacy stuff there. All packages which install old versions under a different log path should go there.
Karl Palmskog (Mar 29 2022 at 09:33):my general reasoning on flocq-compcert packaging is something like:
coq-flocq and coq-flocq3, and they won't care about version numbering, since it will be installed as a dependency if at all Karl Palmskog (Mar 29 2022 at 09:36):I'm not sure I understand how you plan to fit Interval and Gappa into the mix, though (I guess that they also have depopt on coq-flocq3, as suggested by Michael above?)
It doesn't matter to me if the flocq3 Gappa and Interval only live in the Platform repo, but I don't think it's harmful if they are upstreamed
Karl Palmskog (Mar 29 2022 at 09:42):also: I don't think there should be a "legacy" marking in any opam repo. When packages outlive their usefulness, they can stay in the repo but with version ranges that prevent them from causing havoc, and no new package versions are added
Michael Soegtrop (Mar 29 2022 at 09:52):@Karl Palmskog : reagrding flocq and gappa I agree (although I would say there are many users who use Flocq directly, all those who reason about floating point numbers).
Regarding coq-interval/gappa: as I said one can't do the same trick as for CompCert, because one might need a coq-interval to reason about Flocq3 floats and another one to reasons about Flocq4 floats. The same applies to gappa. The default should be Flocq4, but if want's to reason about a CompCert float C program, one might need a Flocq3 based coq-interval and coq-gappa.
Regarding legacy: the special thing of these packages is that they install packages which just defer from another package in that they install stuff into a different log path (like Flocq3) and the only reason why one might want to do this is to install both the current and the legacy version together. I do think that such packages are kind of special. So I don't say that coq-flocq.3.4.3 should be marked as legacy, but that one should somehow state that coq-flocq3.3.4.3 only exists so that one can install coq-flocq.3.4.3 in parallel with coq-flocq.4.0.0.
Karl Palmskog (Mar 29 2022 at 09:54):OK, but then the best way to let people know about status of Flocq3, Gappa-Flocq3, etc., is in the synopses/descriptions of packages. If every version of Flocq3 has this, lower chance to miss by users
Karl Palmskog (Mar 29 2022 at 09:55):we could even display some post-install message
Michael Soegtrop (Mar 29 2022 at 10:05):Yes, I planned to put this in the synopsis / description. I think a post install message is not required.
So you don't think a separate folder for this makes sense and I should just add them as any other package?
Karl Palmskog (Mar 29 2022 at 10:06):just add as any other package, is my view
Michael Soegtrop (Mar 29 2022 at 10:10):OK, fine with me. We can anyway still change the folder structure later if it ever becomes too much of this. This won't change anything in opam's logic.
Xavier Leroy (Mar 29 2022 at 18:11):Andrew Appel said:
I am informed that Flocq 4 was released on 5 November 2021. So the problem is not caused by a last-minute proposal for Flocq 4, it is caused by a delay in porting CompCert to the latest version of Flocq. Therefore I withdraw my objection to including Flocq 4 as the default Flocq for the Coq Platform. The proposal for Require Flocq3 as the old flocq, and Flocq as the new flocq-4, seems OK.
To be fair, the latest release of CompCert (3.10) was on 19 november 2021, so I don't feel too guilty that Flocq 4 support was not included...
The question, I guess, is when VST and its uses for verifying floating-point codes can switch to Flocq 4? CompCert can switch very soon (in release 3.11) or wait some more, thanks to @Michael Soegtrop 's compatibility patches, so it's largely up to you.
Michael Soegtrop (Mar 29 2022 at 19:12):@Xavier Leroy : I don't think Andrew wanted to say that CompCert was slow in adopting Flocq. Andrew initially thought that Flocq4 was a last minute thing (say released last week) and that's the reason he said it is inappropriate to take it in this late in the release cycle. We then had a chat on this and I told him that Flocq4 was introduced a while ago and that the reason it was not yet in Coq Platform 8.15~beta1 are the difficulties with CompCert and VST. That doesn't mean that this is the fault of CompCert and/or VST. Such difficulties are in the nature of a project like Coq Platform. If there were no such difficulties, there would hardly be a need for Coq Platform.
Michael Soegtrop (Mar 30 2022 at 09:14):I added compatibility packages for coq-interval and coq-gappa (still in PR). Interval was trivial, but gappa took me an hour or two. I added some documentation about what needs to be patched for a plugin to make a legacy version. Things I forgot was e.g. to rename the plugin executable, so that I ended up with two plugins of the same name and coqc did choose to its liking.
Last updated: Apr 19 2024 at 23:02 UTC