Michael Soegtrop (Jun 13 2021 at 10:18): Michael Soegtrop (Jun 13 2021 at 10:18):I started to work in the 2021.08 release.
@Enrico Tassi : one thing I am unsure about is how we do the branch naming. Since coq.dev stopped working just when I was ready with my integration of different Coq versions into one Coq Platform release and I was busy after that, it never made it into the 2021.02 branch. So I am unsure if I should merge it there? But I guess the plan is anyway to rename it back to master after it is merged with the dev branch?
Enrico Tassi (Jun 13 2021 at 12:39):Great! I think we should pospone to switch to a single branch after 2021.08 is out
Enrico Tassi (Jun 13 2021 at 12:40):I'll try to help a little next week, maybe we can coordinate on monday
Michael Soegtrop (Jun 13 2021 at 12:40):So do you suggest that I simply push the multi version stuff as new 2021.08 branch?
Btw.: 2021.08 or 2021.07?
Michael Soegtrop (Jun 13 2021 at 12:44):Thinking about it a bit more: It might make sense to keep separate branches, because it might make sense that a Coq 8.13 installed with 2021.08 has newer packages than a Coq 8.13 installed with 2021.02. Not sure about this, though.
Enrico Tassi (Jun 13 2021 at 12:44):I'm a bit outdated, I did not follow much in the last month or so. I'm not so sure my judgement can help. IIRC #102 was ok, but i'm not sure I would touch 2021.02, since that one is supposed to be stable
Enrico Tassi (Jun 13 2021 at 12:45):ideally #102 should go to master, as we should fork off 2021.08 at some point, but I'm not sure either
Michael Soegtrop (Jun 13 2021 at 12:45):Well my changes don't change the outcome - they just also allow to install Coq 8.12 and Coq dev. For Coq 8.13 the result is the same, except for the opam switch name.
Michael Soegtrop (Jun 13 2021 at 12:46):Well right now we don't have a master branch.
Enrico Tassi (Jun 13 2021 at 12:46):Maybe @Théo Zimmermann has ideas as well.
Enrico Tassi (Jun 13 2021 at 12:47):if the outcome is unchanged, then merging is safe... my main problem is that I don't know where to push fixes. For example the snap one I've just merged, I pushed it to .02, but I hope it also goes in .08
Michael Soegtrop (Jun 13 2021 at 12:47):The question is if we should have one master branch from which we tag all releases or not. This would be possible if we say that the package pick for 8.13 is constant for all times. If we have separate branches, we could have different package picks for 8.13 in 2021.02 and 2021.08.
Enrico Tassi (Jun 13 2021 at 12:47):in Coq all fixes go to master, then we may push them to the other branches if we want
Michael Soegtrop (Jun 13 2021 at 12:48):In any case I will rebase to latest 2021.02 before I branch off 2021.08.
Enrico Tassi (Jun 13 2021 at 12:48):Michael Soegtrop said:
The question is if we should have one master branch from which we tag all releases or not. This would be possible if we say that the package pick for 8.13 is constant for all times.
This option seems the best to me
Enrico Tassi (Jun 13 2021 at 12:49):(once #102 is merged)
Michael Soegtrop (Jun 13 2021 at 12:49):So you say that the package pick for Coq 8.13 should never be touched.
Enrico Tassi (Jun 13 2021 at 12:50):I'm not su sure I understand this constraint.
Michael Soegtrop (Jun 13 2021 at 12:50):I think this is OK. and it might be more confusing than helpful to have separate picks for the same version of Coq in 2021.02 and 2021.08. Of cause this would also be more maintenance effort.
Michael Soegtrop (Jun 13 2021 at 12:51):Well we said that for one Coq Platform the package pick shall never be changed except for critical bug fixes.
Michael Soegtrop (Jun 13 2021 at 12:52):The question is if we could have a Coq Platform 2021.02-8.13 and 2021-08-8.13 with different picks, say VST 2.8 instead of VST 2.7.
Michael Soegtrop (Jun 13 2021 at 12:52):If we do this, we need different branches to handle it technically.
Enrico Tassi (Jun 13 2021 at 12:53):Hum, because you want to be able to release fixes for 2021.02-8.13?
Michael Soegtrop (Jun 13 2021 at 12:54):Not fixes - fixes could go into 2021.02.X (of cause for this one also needs a branch ...).
Enrico Tassi (Jun 13 2021 at 12:54):yes, that is what I meant
Michael Soegtrop (Jun 13 2021 at 12:54):The idea is more to have updated 8.13 compatible packages. Like VST 2.8 and CompCert 3.9 all work for 8.13 and 8.14.
Michael Soegtrop (Jun 13 2021 at 12:55):In 2021.02 we have VST 2.7 and CompCert 3.8.
Enrico Tassi (Jun 13 2021 at 12:55):imo 2021-08-8.13 should have 2.8+3.9, while 2021.02-8.13 stays with 2.7+3.8
Enrico Tassi (Jun 13 2021 at 12:56):if we need to branch for this, we will, but isn't just about having multiple pick (not per Coq version, but per pair platform-coq)?
Michael Soegtrop (Jun 13 2021 at 12:56):OK, I agree with that. Then we definitely need long term separate branches for each release and not just one master branch from which we do tags.
Michael Soegtrop (Jun 13 2021 at 12:57):I guess we went through this discussion already ...
Enrico Tassi (Jun 13 2021 at 12:57):Sorry, I told you I'm a bit off ;-)
Michael Soegtrop (Jun 13 2021 at 12:58):No, I meant I turn mentally in circles sometimes.
Michael Soegtrop (Jun 13 2021 at 12:59):So I push the multi Coq thing as master (it is already rebased to 2021.02), then I fix everything (dev has issues) and then I branch of 2021.08 from master?
Enrico Tassi (Jun 13 2021 at 12:59):that would be ok.
Enrico Tassi (Jun 13 2021 at 13:00):I still wonder if "branch of 2021.08 from master" is really needed after 102
Michael Soegtrop (Jun 13 2021 at 13:00):Hmm - I don't understand your last comment.
Enrico Tassi (Jun 13 2021 at 13:01):I did not look at the code, but I can imagine it being about adding a file coq_package_2021.08_8.14
Enrico Tassi (Jun 13 2021 at 13:02):102 adds support for coq_packages_8.x IIRC
Michael Soegtrop (Jun 13 2021 at 13:02):Ah, you mean we can branch off 2021.08 later - more before we do 2122.02?
Enrico Tassi (Jun 13 2021 at 13:02):I was stretching the idea to have one package selection file per platform times coq versionm eg coq_packages_2021.02_8.13
Enrico Tassi (Jun 13 2021 at 13:04):yes. I'll try to clarify:
Enrico Tassi (Jun 13 2021 at 13:07):I guess master will select a default package selection.
If it is dev, then we are forced to branch, change the default selection, and then tag at release time.
If the default selection is the latest released platform, then we don't really need to branch when we tag.
Unless we need to do a point release for an old platform (and then we would branch just to change the default selection I guess).
Ideally all the "stuff" is in master, and we only select which one the user gets by default.
Am I dreaming?
Michael Soegtrop (Jun 13 2021 at 13:10):The multi-version thing is here (https://github.com/MSoegtropIMC/platform/tree/multi-version)
Michael Soegtrop (Jun 13 2021 at 13:11):You have several package list files in (https://github.com/MSoegtropIMC/platform/tree/multi-version/versions) and can choose via command line or interactively one of these.
Michael Soegtrop (Jun 13 2021 at 13:11):The idea for CI is to run all of them (at least sometimes) as a matrix.
Enrico Tassi (Jun 13 2021 at 13:13):Yes, I was wondering if it is possible to have ./coq_platform_make.sh -packages=2021.02_8.13 and, at the same time, ./coq_platform_make.sh -packages=2021.08_8.13 (I know that branch/PR only lets you ./coq_platform_make.sh -packages=8.13)?
Michael Soegtrop (Jun 13 2021 at 13:13):So yes, we can tag releases from master and only branch of release branches in case there is a real need - as you say a patch release after a new version has been released. I would say we can wait until this happens.
Enrico Tassi (Jun 13 2021 at 13:14):So CI/matrix can test multiple coq/platform combinations, all in the master branch
Enrico Tassi (Jun 13 2021 at 13:14):ok
Michael Soegtrop (Jun 13 2021 at 13:14):It can do 8.12 + 8.13 + dev, but as is not 2021.02-8.13 and 2021.08-8.13, although this would be easy to add.
Enrico Tassi (Jun 13 2021 at 13:15):if we add it, then I think branch are way less nedded (which is good, IMO)
Michael Soegtrop (Jun 13 2021 at 13:15):Maybe it would be less confusing to users if we would actually offer "8.13 (2021.02 pick)" to the user in 2021.08.
Michael Soegtrop (Jun 13 2021 at 13:16):Then we could of cause also test it in CI and also do patches to this package list (the 2021.02 8.13) from master.
Enrico Tassi (Jun 13 2021 at 13:16):indeed
Enrico Tassi (Jun 13 2021 at 13:17):so 2021.08 will include a bunch of possible selections, even the old 2021.02
Michael Soegtrop (Jun 13 2021 at 13:17):So the user would get a list like
Michael Soegtrop (Jun 13 2021 at 13:18):At some point one could only show a selection interactively, but still have them all.
Enrico Tassi (Jun 13 2021 at 13:18):yes. If we do so, there will be no need to tag a fix 2021.02.2, for exammple, we can just release a 2021.08.2 with an updated selection for the old platform.
Enrico Tassi (Jun 13 2021 at 13:19):(I'm trying to see all scenarios)
Michael Soegtrop (Jun 13 2021 at 13:19):Yes. And as I said, it is likely less confusing than telling users to use Coq 8.13 from Coq Platform 2021.02 or 2021.08.
Enrico Tassi (Jun 13 2021 at 13:19):we agree
Enrico Tassi (Jun 13 2021 at 13:20):gotta go now, ciao
Michael Soegtrop (Jun 13 2021 at 13:20):Perfect. Also this has the advantage that one doesn't have to know if one should name it 2021.07 or 2021.08 before one actually does the release ;-)
Michael Soegtrop (Jun 13 2021 at 13:20):Ciao, thanks for the helpful discussion!
Théo Zimmermann (Jun 13 2021 at 20:40):I've read the discussion only now but I fully agree with your conclusion.
Andrew Appel (Jul 28 2021 at 19:54):I also just skimmed the end of the discussion, this makes sense to me. I look forward to the release of "Coq 8.13 (2021.08 package pick)" without having to wait for Coq 8.14.
Théo Zimmermann (Jul 29 2021 at 09:37):Yeah, given the delays in getting 8.14 out, this would definitely make sense.
Michael Soegtrop (Aug 18 2021 at 08:23):@Théo Zimmermann @Guillaume Melquiond : is there news on the 8.14 release? I was super busy the last few weeks but it is getting better.
Ali Caglayan (Aug 18 2021 at 08:59):We still have some blockers on the release that need to get resolved
Ali Caglayan (Aug 18 2021 at 08:59):https://github.com/coq/coq/milestone/32
Ali Caglayan (Aug 18 2021 at 08:59):They are some real head scratchers unfortunately.
Michael Soegtrop (Aug 19 2021 at 17:00):Is there an estimation? I don't want to push - I just need to make sure that I have a bit of time to do the platform work, and if it would take too long, I might do a 2021.08 pre release - either with 8.13 or with a 8.14 preview.
Théo Zimmermann (Aug 20 2021 at 15:00):Hi @Michael Soegtrop! I personally think that the 8.14 release has already been delayed way too much and maybe we should consider filling @Andrew Appel's request of a 2021.08 platform release / package pick, without waiting for Coq 8.14.
Michael Soegtrop (Aug 21 2021 at 08:21):@Théo Zimmermann : OK, I will look into it. What version of Coq would you recommend? 8.13 or should we do some sort of 8.14 preview tag?
Théo Zimmermann (Aug 21 2021 at 17:18):Yes, 8.13 could be the main version. Ideally we would also include an 8.14 preview tag, but that would require the involvement of @Guillaume Melquiond to make a tag.
Michael Soegtrop (Aug 21 2021 at 17:56):I guess the 8.13/8.14 question also depends on what desirable versions of packages require - if everything runs nicely with 8.13, I think we should make a clean 8.13 version and if 8.14 is ready, we can do another release. If we have 2021.08 and 2021.09 then, so be it.
Michael Soegtrop (Aug 21 2021 at 17:56):I will prepare everything during this week.
Last updated: Nov 29 2023 at 04:01 UTC