Michael Soegtrop (Jul 12 2022 at 13:58): Michael Soegtrop (Jul 12 2022 at 13:58):I am currently preparing a preview for Coq Platform 2022.09 (a preview is not complete and might have packages which point to non release commits).
I wonder what is the best way to handle the latter. Currently I am creating in the Coq Platform local opam patch rep ".preview" packages, which point to specific commit. This is clear but has the disadvantage that dependent packages usually also need to be patched to allow the "preview" version.
I see two possible solutions to this:
What is your opinion? Do you have a better idea on how to handle this?
Karl Palmskog (Jul 12 2022 at 14:03):fine by me if you want to use extra-dev to host packages like this, as long as we have some idea what will happen with the packages afterwards (e.g., are they removed or live on), and there is a consistent naming convention for the packages.
Enrico Tassi (Jul 12 2022 at 14:04):option 2 seems better to me, it amounts at copying extra-dev in the platform overlay directory and pin there. This is in line with your work to keep extra-dev functioning well (for CI, and now also for preview releases)
Enrico Tassi (Jul 12 2022 at 14:05):the only "misleading" thing is that experienced opam users would find weird that .dev is pinned, but I think we can live with this
Michael Soegtrop (Jul 12 2022 at 14:19):@Karl Palmskog : the idea is to keep things in the Coq Platform local extra-dev repo. I don't see a good reason for publishing these, but of course this could also be done. It might be easier thought to have a "register the Coq Platform patch repos in my current switch" script for the pro users.
@Enrico Tassi : the idea was to have yet another folder, say "extra-preview-2022.09" or so, which is only registered for the preview release. I want the "dev" pick to be plain "dev". Usually if the pick works, dev works as well. The reason for having the preview packages is to have something stable.
Enrico Tassi (Jul 12 2022 at 14:31):right, but the version (as in opam) of the packages in extra-preview-2022.09/ would be dev right?
Enrico Tassi (Jul 12 2022 at 14:32):(even if they pin a commit, and not follow a branch)
Michael Soegtrop (Jul 12 2022 at 15:35):@Enrico Tassi : yes, I would call the dev in order to avoid that I need to patch dependent packages.
Michael Soegtrop (Jul 12 2022 at 15:35):So what is the conclusion?
Karl Palmskog (Jul 12 2022 at 18:01):fine by me to do "option 2" as Enrico recommends
Enrico Tassi (Jul 12 2022 at 19:10):option 2 is good
Théo Zimmermann (Jul 13 2022 at 10:41):I agree with option 2 as well.
Last updated: Jun 03 2023 at 03:01 UTC