Michael Soegtrop (Feb 27 2021 at 13:22): Michael Soegtrop (Feb 27 2021 at 13:22):@Enrico Tassi : I tried to enable the smoke tets kit on the 8.12 branch. The VST/COmpCert test seem to fail because VST and CompCert is not installed by default. I tested the silent command line install you use in the github action and when I try this locally, it indeed does not install CompCert and VST. What I don't understand is why the smoke test works in the 2021.02 branch - it also shouldn't install VST, but the smoke test passes. Do you understand this?
Enrico Tassi (Feb 27 2021 at 13:30):I think you may need to backport https://github.com/coq/platform/commit/28facfe8a280318d8d98da2e3e0e0d7cabc4b385
Michael Soegtrop (Feb 27 2021 at 13:31):Ah, thanks!
Michael Soegtrop (Feb 27 2021 at 16:58):Thinking about this, since now we name it after a date and not a Coq version and since all the scripts are the same except for the package list and switch name, I am thinking about adding the package files for the different versions to the 2021.02 branch and adding a script question on which version of Coq shall be installed (possibly not a question but just a command line option).
What do you think?
Btw.: the main reason for supporting older versions is fighting bit rot - it is much easier to port a proof when one can single step it in a Coq version where it works.
Théo Zimmermann (Feb 27 2021 at 18:05):Yes, I think that could be a good idea. But for a fixed version (like 2021.02.1), it would be natural that if you activate one of the older Coq versions, you get exactly the same version of the other packages. If when you select the previous Coq version, then you get the previous package set, then it is better to consider that this gets a different major version name.
Théo Zimmermann (Feb 27 2021 at 18:06):This would not always be possible, so it would be reasonable that this is done on a "best effort" basis and when this version of a package is not compatible with the previous version of Coq, then you get a previous version of the package.
Enrico Tassi (Feb 27 2021 at 18:29):Hum, I can imagine an option to override Coq, but then you would need to tell opam to ignore the version constraints of the other packages, eg all the plugins depend on one version of Coq (maybe except for gappa). I mean you could first ask if package p.v is installable given the coq version and if not drop its version constraint and just install p
Enrico Tassi (Feb 27 2021 at 18:34):A related question is: instead of a branch per version, we may just have a platform_coq_packages.sh file, eg platform_coq_packages.2021.02.x.sh, this could ease sharing stuff between platform version, and it would be possible to provide "hybrid" package sets with a overridden Coq (in this case the versions compatible are to be listed there once and forall). Eg platform_coq_packages.2021.02_on_Coq8.12.sh
Enrico Tassi (Feb 27 2021 at 18:36):after all, once the main infrastructure is finished, a release should just be a list of packages/versions plus some overlays to fix stuff.
Enrico Tassi (Feb 27 2021 at 18:36):git branches don't really help for this
Michael Soegtrop (Feb 28 2021 at 07:58):Hum, I can imagine an option to override Coq, but then you would need to tell opam to ignore the version constraints of the other packages, eg all the plugins depend on one version of Coq (maybe except for gappa)
Not sure I understand you. The idea is more to provide easy access to complete older platforms. As Théo said, the package list should be the same as what was common say when Coq 8.11 was out. This can help in porting, because one can esily install several versions of the platform in different switches and then step through teh same proof in an old Coq (platform) and a new one.
One thing I keep forgetting: bsides the package file a large part of the Coq platform is the opam patch repo, although I hope to reduce this to 0 over time. It might be possible to have the patches for different versions in one opam repo, since different platform version usually binf different package versions. I will give this a try locally (merge the opam patch repo of 8.12.2, 2021.02 and dev-ci) and see what happens.
Last updated: Jun 03 2023 at 03:01 UTC