Michael Soegtrop (Oct 02 2021 at 15:41): Michael Soegtrop (Oct 02 2021 at 15:41):As mentioned a few times I wanted to add picks for Coq 8.9 to 8..1 to Coq Platform. There is only one issue: the picks we used for the installers back then where frequently done in a hurry and include a lot of dirty stuff like arbitrary commits.
I wonder if I should follow what has been done in the installers back then, or if I should do opam picks which are reasonable from today's point of view?
Théo Zimmermann (Oct 02 2021 at 16:09):No, you should absolutely not consider the old installers as giving any mandate to what the platform should do today.
Théo Zimmermann (Oct 02 2021 at 16:10):On the contrary, I would recommend selecting the latest compatible version or some package versions that are compatible across a broad range of Coq versions.
Michael Soegtrop (Oct 02 2021 at 16:15):@Théo Zimmermann : I am not sure the latest compatible package would be the best choice - I thought about using the one which was released after the Coq release. The main reason for having the old picks is that it should be likely that projects done at that time will compile with at most minor changes. Using versions which didn't exist back then might not help this.
Of course one could have an "original" and a "latest" pick - as we have for 8.13 now. Not sure if this wouldn't be over the top, though.
What is your reasoning behind bundling the latest packages?
Théo Zimmermann (Oct 02 2021 at 16:17):My reasoning is that it is easier to port stuff when not everything changes at once. So if you can provide a package version that is compatible with a broad range of Coq versions, it helps porting to new Coq versions stepwise.
Michael Soegtrop (Oct 02 2021 at 19:13):Hmm, I am not convinced. When I port something I take a CoqIDE of both versions and step through the code and compare. This implies that the code works out of the box in the old version. When it doesn't what do you do then?
Paolo Giarrusso (Oct 02 2021 at 23:53):If both Coq and dependencies change, one might need three installs:
Paolo Giarrusso (Oct 02 2021 at 23:55): Paolo Giarrusso (Oct 02 2021 at 23:56):So I guess your proposals skip either 1 or 2?
Michael Soegtrop (Oct 03 2021 at 07:42):@Paolo Giarrusso : this assumes that one does the porting step by step, say exchange Coq and then exchange one dependency after another. This is at least not as I work, since I think it is more work, since one might have to got through the proofs several times.
What I prefer is to have a setup where the to be ported code works as is and the target setup. I don't understand the need for anything in between. So my suggestion was to pick something which represents what has been used in a certain time frame.
Paolo Giarrusso (Oct 03 2021 at 08:11):Skipping that step does make sense, but I wonder how likely that is to help. EDIT: That guess is only very likely to work if the original code was never updated.
Paolo Giarrusso (Oct 03 2021 at 08:14):When you update a project, whether you update only Coq or also your deps is likely to be idiosyncratic…
Paolo Giarrusso (Oct 03 2021 at 08:17):OTOH, I’m not sure what the goal of these releases should be. If the goal is to help current packages support older Coq versions, Théo’s idea might make more sense. If the goal is software archeology, Michael’s idea might make more sense, if old software agreed enough. I’m probably skeptical because in the _Haskell_ world that never worked until a Coq-Platform-analogue was introduced. (Of course, that ecosystem is very different).
Michael Soegtrop (Oct 03 2021 at 08:19):The main goal is to make it easy to "look" at outdated projects - that is to run them in CoqIDE without messing around for a few days. IMHO this is a prerequisite for any porting effort.
Michael Soegtrop (Oct 03 2021 at 08:20):Possibly one should test a few older projects which stopped at 8.9 or 8.10 and see in which environment they compile.
Théo Zimmermann (Oct 03 2021 at 18:14):I based my suggestion on the fact that for porting Coq proofs from an old Coq to a recent Coq, we usually recommend going step by step (i.e., porting to some intermediate version first). That being said, I understand your point about having something which corresponds more likely to the state in which projects were tested back then.
Michael Soegtrop (Oct 04 2021 at 12:58):@Théo Zimmermann : so what is your conclusion on how the picks should be done?
Théo Zimmermann (Oct 04 2021 at 13:14):I think that in all likelihood this choice will not have a very big impact. If you feel that your solution is best, do go with it. But it may represent a bit more work than just finding suitable versions of the packages that are compatible with a broad range of Coq versions.
Michael Soegtrop (Oct 04 2021 at 13:38):But it may represent a bit more work than just finding suitable versions of the packages that are compatible with a broad range of Coq versions.
Yes. I will delay this to 2021.11 and do some statistics on older packages.
So except for a documentation update, the main branch (and 2021.09) is ready.
Théo Zimmermann (Oct 04 2021 at 14:05):Yes, I think this is wise to delay that work.
Last updated: Jun 03 2023 at 05:01 UTC