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?
No, you should absolutely not consider the old installers as giving any mandate to what the platform should do today.
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.
@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?
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.
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?
If both Coq and dependencies change, one might need three installs:
So I guess your proposals skip either 1 or 2?
@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.
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.
When you update a project, whether you update only Coq or also your deps is likely to be idiosyncratic…
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).
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.
Possibly one should test a few older projects which stopped at 8.9 or 8.10 and see in which environment they compile.
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.
@Théo Zimmermann : so what is your conclusion on how the picks should be done?
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.
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.
Yes, I think this is wise to delay that work.
Last updated: Jun 03 2023 at 05:01 UTC