Emilio Jesús Gallego Arias (May 11 2020 at 13:23): Emilio Jesús Gallego Arias (May 11 2020 at 13:23):Hi all, this is a thread to discuss everything related to the 8.12 release. For now, recall that the branching target is May 15th, so these are the last days to get Pull Requests that are not bugfixes merged in master
Emilio Jesús Gallego Arias (May 15 2020 at 14:45):Hi all, branching is expected to happen very soon. At this point only fixes and documentation improvements are allowed to target the 8.12 milestones; there are some pre-existing PRs that could still make it if they get processed in the next couple of days. If you have any question or request please don't hesitate to get in touch with us,
Théo and Emilio
Enrico Tassi (May 15 2020 at 15:16):I've created this https://github.com/coq/coq/issues/12334 and read the first paragraph. I won't have time to do any of it before Monday. BTW, it seems that creating the alpha tag is better done by the one that makes the 8.12 branche no?
Emilio Jesús Gallego Arias (May 15 2020 at 15:17):Indeed @Enrico Tassi , good point; we will push the tag. The problem with the tag is that it is supposed to be placed on the _first_ commit not in 8.12
Emilio Jesús Gallego Arias (May 15 2020 at 15:17):so indeed we cannot do when we branch, as we need to wait for a PR to be merged in master first
Théo Zimmermann (May 15 2020 at 15:18):Great, thanks @Enrico Tassi. My view is that the best course of action would be for the first PR to be merged into master after the branch be the one that updates the version number. And then, the tag would go on the commit this PR contains.
Théo Zimmermann (May 15 2020 at 15:19):So, we should probably reorder the two corresponding checkboxes.
Enrico Tassi (May 15 2020 at 15:19):Maybe it would make sense to "shift" the creation of this PR (the one doing the version renaming) https://github.com/coq/coq/pull/11158/files from RM n+1 to RM n, and have this tagged.
Enrico Tassi (May 15 2020 at 15:19):Anyway, I can tag on Monday myself, I'm just trying to understand how the process works
Théo Zimmermann (May 15 2020 at 15:19):In fact, the most important thing to my eyes is that this is the 8.12 RM which merges the PR bumping to 8.13.
Enrico Tassi (May 15 2020 at 15:20):(I won't be able to prepare it before monday afternoon)
Théo Zimmermann (May 15 2020 at 15:21):Since we are two 8.12 RMs, if you agree with this plan, I can take care of preparing the PR, and @Emilio Jesús Gallego Arias can take care of merging it.
Emilio Jesús Gallego Arias (May 15 2020 at 15:21):Sounds good
Enrico Tassi (May 15 2020 at 15:21):As you like
Enrico Tassi (May 15 2020 at 15:21):less work for me ;-)
Emilio Jesús Gallego Arias (May 15 2020 at 15:22):Actually the create-branch script could do all this; branch, push the branch, create the commit, submit the PR, merge it, and push the tag
Théo Zimmermann (May 15 2020 at 15:23):Yes.
Théo Zimmermann (May 15 2020 at 15:23):I wanted to work on such a script but did not do it yet, maybe I'll do it now.
Enrico Tassi (May 15 2020 at 15:23):It would be nice, but your PR 11158 is not exactly trivial
Enrico Tassi (May 15 2020 at 15:24):In particular it is not a simple sed, there is ADT with V8XX and some code matching on it.
Théo Zimmermann (May 15 2020 at 15:24):A lot of it is already generated by a script
Théo Zimmermann (May 15 2020 at 15:25):(dev/tools/update-compat.py)
Enrico Tassi (May 15 2020 at 15:25):You are right, I did not read the paragraph at the end
Théo Zimmermann (May 15 2020 at 15:25):BTW @Enrico Tassi did you copy the content of this new issue from dev/doc/release-process.md or from the 8.12 issue?
Théo Zimmermann (May 15 2020 at 15:25):It looks like it isn't in sync with the latest changes...
Enrico Tassi (May 15 2020 at 15:26):hum, no, I did the silly thing. It says copy "this" and I interpreted it strictly
Enrico Tassi (May 15 2020 at 15:26):let me update it
Emilio Jesús Gallego Arias (May 15 2020 at 15:28):Which one is not in sync? I guess the one in dev/doc ?
Théo Zimmermann (May 15 2020 at 15:29):The one in dev/doc is the correct reference.
Théo Zimmermann (May 15 2020 at 15:29):Because it is the one that we update when we want to make the process evolve.
Théo Zimmermann (May 15 2020 at 15:30):But now, I'm thinking that we could have the bot do many of these things for us, including opening the next "release issue" whenever we check boxes.
Enrico Tassi (May 15 2020 at 15:33):done, it was silly on my side, anyway I clarified it. now it should be brainless-compatible
Théo Zimmermann (May 15 2020 at 15:34):This does look more up-to-date to me :slight_smile:
Emilio Jesús Gallego Arias (May 15 2020 at 15:41):@Théo Zimmermann I think I may have done a pass on the issue that was not reflected on the .md file
Théo Zimmermann (May 15 2020 at 15:43):Interesting, then we might want to resync the .md file to take into account some of your changes.
Théo Zimmermann (May 15 2020 at 15:44):I've noted down automation ideas in coq/bot#51. We'll see if I finally get an intern this month and if this is something that he can push forward.
Emilio Jesús Gallego Arias (May 16 2020 at 18:05):@Théo Zimmermann something we don't have is a way to block PRs with the 8.13 milestone from being merged.
Emilio Jesús Gallego Arias (May 16 2020 at 18:05):We are keeping a (manual) eye on that, but yeah, it is far from optimal.
Théo Zimmermann (May 16 2020 at 18:05):Let's create a needs: next release branch
Théo Zimmermann (May 16 2020 at 18:05):Since the needs: labels are checked by the merging script.
Théo Zimmermann (May 16 2020 at 18:07):However, if a PR accidentally ends up being merged before the branching with the 8.13 milestone but it is actually fine for 8.12, then we can just fix the milestone (I did that for three PRs which had been milestoned as 8.12.0 but were merged so should have been 8.12+beta1).
Emilio Jesús Gallego Arias (May 16 2020 at 18:09):Yeah this is something the bot could do
Théo Zimmermann (May 16 2020 at 18:11):Indeed, such things could be checked as part of a major revamp of the automation for release and backporting management. Let's see what my intern can do about this, this summer (if the internship finally happens).
Hugo Herbelin (May 18 2020 at 10:27):Is there an update on when the 8.12 branch is done? (Or conversely, are there PRs on which prioritary reviews have still to be made? Which for me would be after 6pm GMT+2 though.)
Emilio Jesús Gallego Arias (May 18 2020 at 10:28):Hugo, we are about to branch
Hugo Herbelin (May 18 2020 at 10:29):OK
Emilio Jesús Gallego Arias (May 18 2020 at 10:29):I don't see anything urgent, thanks; stuff seems under control.
Emilio Jesús Gallego Arias (May 18 2020 at 10:30):A couple of PRs seem that won't be ready, but IMO not a big deal
Emilio Jesús Gallego Arias (May 18 2020 at 10:30):We can always backport if we think delaying is a mistake
Emilio Jesús Gallego Arias (May 18 2020 at 10:30):@Théo Zimmermann , you see something urgent in the sense of what Hugo asks?
Théo Zimmermann (May 18 2020 at 10:31):Nope, all is good!
Enrico Tassi (May 18 2020 at 15:50):Finally some time. I see the branch was made, as well as the commit coq/coq#ea6cb6b542e8c356192bb77f234586e0f6d55c8c. Should I tag it with V8.13+alpha?
Enrico Tassi (May 18 2020 at 15:52):Oh, I see emilio told me in a PR, ok
Emilio Jesús Gallego Arias (May 18 2020 at 15:55):Note that the first 8.13 commit is not the merge PR but the merge parent
Théo Zimmermann (May 18 2020 at 15:55):(so that would be f123874, cf. our comments on this commit)
Théo Zimmermann (May 18 2020 at 16:00):Well, never mind. We haven't been very consistent in this practice anyway.
Enrico Tassi (May 18 2020 at 16:01):uff... I'll fit that, but I don't what would be the difference
Enrico Tassi (May 18 2020 at 16:02):fixed
Emilio Jesús Gallego Arias (May 18 2020 at 16:03):Théo Zimmermann said:
Well, never mind. We haven't been very consistent in this practice anyway.
What do you mean?
Théo Zimmermann (May 18 2020 at 16:04):In the past, there were many alpha commits that targeted merge commits.
Enrico Tassi (May 18 2020 at 16:04):The VX.X+alpha tag marks the first commit to be in master and not in the
branch of the previous version.
Apart from that, I don't see how I should have understood that from the text above
Théo Zimmermann (May 18 2020 at 16:05):Yep, the spec is a bit imprecise.
Enrico Tassi (May 18 2020 at 16:05):To me the first commit landing in master is the merge one
Théo Zimmermann (May 18 2020 at 16:05):It used to be my interpretation as well.
Théo Zimmermann (May 18 2020 at 16:06):But like I said, that's not a big deal.
Emilio Jesús Gallego Arias (May 18 2020 at 16:06):Théo Zimmermann said:
In the past, there were many alpha commits that targeted merge commits.
8.11 / 8.12 were correctly set; IMHO this not something we can ignore, tagging on the merge commit is incorrect
Enrico Tassi (May 18 2020 at 16:06):Can you explain why?
Emilio Jesús Gallego Arias (May 18 2020 at 16:07):use git log --topo-order
Emilio Jesús Gallego Arias (May 18 2020 at 16:07):the first commit to land in a branch can never be a merge commit
Emilio Jesús Gallego Arias (May 18 2020 at 16:07):in the sense that by topological ordering the parent commit would not be on the branch
Emilio Jesús Gallego Arias (May 18 2020 at 16:07):so if you tag the merge commit
Emilio Jesús Gallego Arias (May 18 2020 at 16:07):the commit that is actually merged
Emilio Jesús Gallego Arias (May 18 2020 at 16:07):won't be considered to be part of 8.13
Emilio Jesús Gallego Arias (May 18 2020 at 16:08):but won't be part of 8.12 either
Emilio Jesús Gallego Arias (May 18 2020 at 16:08):so would we had tagged the merged commit, f1238742f931269167e7c2704b53bb285d05f39d would be orphaned in terms of tags
Emilio Jesús Gallego Arias (May 18 2020 at 16:09):git describe for example would have found the 8.12 parent
Emilio Jesús Gallego Arias (May 18 2020 at 16:09):incorrectly, this was discussed in 8.10/8.11 I believe
Enrico Tassi (May 18 2020 at 16:10):ok, that is a good reason. I'll clarify the doc
Emilio Jesús Gallego Arias (May 18 2020 at 16:10):Thanks
Emilio Jesús Gallego Arias (May 18 2020 at 16:15):But yeah, first commit not in a branch is determined in git-land by topological order, descending from the earliest merge point ; to avoid confusion there are scripts around that do that
Emilio Jesús Gallego Arias (May 18 2020 at 16:16):Coq 8.12 projects for backports seems to be working correctly! @Théo Zimmermann
Emilio Jesús Gallego Arias (May 18 2020 at 16:16):We can test the first backport soon
Théo Zimmermann (May 18 2020 at 16:19):Yes, but let's pin ci-basic-overlay.sh first.
Emilio Jesús Gallego Arias (May 29 2020 at 10:17):Salut @Théo Zimmermann , where we are at the beta? It seems to me we could try do the packages even today
Emilio Jesús Gallego Arias (May 29 2020 at 10:17):right?
Emilio Jesús Gallego Arias (May 29 2020 at 10:17):Barring a few things, it seems that we don't expect a lot of changes
Emilio Jesús Gallego Arias (May 29 2020 at 10:18):WDYT?
Emilio Jesús Gallego Arias (May 29 2020 at 10:24):Two main blockers:
Théo Zimmermann (May 29 2020 at 10:41):What do you mean doing the packages? Tagging? I don't think this is doable today and to my eyes there are several blockers:
Emilio Jesús Gallego Arias (May 29 2020 at 11:17):Thanks for the detailed summary @Théo Zimmermann ; I've adjusted a few issues. I was referring to building the test packages; IMO we may want to try before the beta tag to see if there are any build problems [as you mentioned] and to have some testing. Once we have tested we can proceed to tag.
Théo Zimmermann (May 29 2020 at 12:42):Then, yes, it should be possible to do this pretty soon (main issue is fixing the coq-menhirlib issue).
Emilio Jesús Gallego Arias (May 29 2020 at 12:43):OSX packages should be actually testable right now, right?
Emilio Jesús Gallego Arias (May 29 2020 at 12:43):For Win we can disable compcert for now; and try to see what happens
Emilio Jesús Gallego Arias (May 29 2020 at 12:44):I'm pretty unhappy with the approach used in the Windows build
Théo Zimmermann (May 29 2020 at 12:48):OSX packages should be actually testable right now, right?
Yes, and they are continuously generated so we could already request someone with a Mac to test them.
Théo Zimmermann (May 29 2020 at 12:48):For Win we can disable compcert for now; and try to see what happens
Yeah, that would work.
Théo Zimmermann (May 29 2020 at 12:49):I'm pretty unhappy with the approach used in the Windows build
Me too, but the reason why I've not been in a hurry to fix this is because of the upcoming platform.
Théo Zimmermann (May 29 2020 at 12:49):(which should make this obsolete)
Emilio Jesús Gallego Arias (Jun 02 2020 at 11:51):@Théo Zimmermann , it seems that once we process https://github.com/coq/coq/pull/12429 , and the doc PRs [these are ready tho] we could try to tag, WDYT?
Emilio Jesús Gallego Arias (Jun 02 2020 at 11:52):As I wrote on the Github Actions thread, it is feasible to bulid 8.12 Win packages using Github Actions, if we would like to do so.
Emilio Jesús Gallego Arias (Jun 02 2020 at 11:52):Of course we would not be able to remove the Inria-cloud packages yet, but if you think it is a good idea we could provide both sets of windows packages in the beta
Théo Zimmermann (Jun 02 2020 at 16:13):After looking at the PR, I am not confident that you will manage to have the infrastructure in place soon enough to generate the 8.12 beta Windows package with GitHub Actions. But if you do get there in time, then I would be happy to replace the GitLab CI setup with Inria runners. Why do you say we would have to ship packages generated with both?
Emilio Jesús Gallego Arias (Jun 02 2020 at 16:46):I can have a working version for this week; the problems are due to the complex interface to the current build scripts but I will fire my win VM up and should solve all the problems. Cygwin install went in the way it had to do so that IMO was the most critical issue.
My point about still having both packages is that we are quite late, I mean we should still have to generate both packages for a while, and only when the Azure package has been more tested we could think of actually replacing it.
Emilio Jesús Gallego Arias (Jun 02 2020 at 16:46):WDYT?
Théo Zimmermann (Jun 02 2020 at 17:26):If this is how you see things, then I think this is an argument to say this infrastructure change would be 8.13 material.
Emilio Jesús Gallego Arias (Jun 02 2020 at 17:30):I'm really exploring options @Théo Zimmermann , I don't have a particular view; I'm perfectly fine with the win build rework being 8.13, but of course I'd like to hear what you think
Emilio Jesús Gallego Arias (Jun 02 2020 at 17:30):The only positive point would be if migrating does make our life easier
Emilio Jesús Gallego Arias (Jun 02 2020 at 17:30):but indeed if we deem it too risky that's a no go for 8.12
Théo Zimmermann (Jun 02 2020 at 17:31):I think it might, but just a little. And I think the risk is reasonable if we do the change in the beta.
Emilio Jesús Gallego Arias (Jun 02 2020 at 17:31):I'd say let's finish the GH actions packaging anyways, and we re-evaluate
Théo Zimmermann (Jun 02 2020 at 17:31):But I wouldn't keep both even for a limited period.
Emilio Jesús Gallego Arias (Jun 02 2020 at 17:31)::+1:
Emilio Jesús Gallego Arias (Jun 02 2020 at 17:32):My personal view is that we should take as little risk as possible, so I propose this:
Emilio Jesús Gallego Arias (Jun 02 2020 at 17:32):I'll finish the PR tomorrow
Emilio Jesús Gallego Arias (Jun 02 2020 at 17:32):then we see how the diff looks
Emilio Jesús Gallego Arias (Jun 02 2020 at 17:32):and make a choice
Emilio Jesús Gallego Arias (Jun 02 2020 at 17:32):even so we should keep the backup for a while, just in case, but I'm happy to take care of that
Emilio Jesús Gallego Arias (Jun 02 2020 at 17:32):my win VM is almost ready
Théo Zimmermann (Jun 02 2020 at 17:40):OK
Emilio Jesús Gallego Arias (Jun 03 2020 at 13:14):Regarding the IDE issues, I'm unsure what to do with them.
Théo Zimmermann (Jun 03 2020 at 13:18):One of them is certainly not a regression so could easily be postponed.
Théo Zimmermann (Jun 03 2020 at 13:19):The one reported by Enrico might be a regression. We should check if we can reproduce it. If it only happens through Wine, it is not a big deal.
Théo Zimmermann (Jun 03 2020 at 13:26):While trying to build the Windows package with add-ons, I got a failure in Unicoq:
Dynlink error: The module `Int_misc' is already loaded (either by the main program or a previously-dynlinked library)
Do you know how to interpret this? Could it be related to coq/coq#12421? (I only tested after backporting this PR.)
Emilio Jesús Gallego Arias (Jun 03 2020 at 14:01):This is due to many Coq plugins broken in OCaml >= 4.08 , there is an open issue already
Théo Zimmermann (Jun 03 2020 at 14:03):Oh OK, so the easiest solution is to downgrad OCaml to 4.07, right?
Emilio Jesús Gallego Arias (Jun 03 2020 at 14:03):See https://github.com/coq/coq/issues/12067
Emilio Jesús Gallego Arias (Jun 03 2020 at 14:03):I think for now yes
Michael Soegtrop (Jun 04 2020 at 08:04):@Théo Zimmermann : I wanted to ask what remains to be done for the version picking. Please note that I am still working on improved makefiles for VST which use a platform supplied CompCert. There is an open PR from me at VST which needs a bit more work. It might not be ready for the 8.12 beta but I hope to finish it within a week. Anything else?
Théo Zimmermann (Jun 04 2020 at 08:53):@Michael Soegtrop thanks for asking! I definitely need your help. See coq/coq#12415.
Michael Soegtrop (Jun 04 2020 at 09:00):You mean you need a Windows build server maintenance run? Luckily I am at home - I will look into it.
Théo Zimmermann (Jun 04 2020 at 09:01):This (thanks!) and help on fixing menhir, making sure CompCert and VST work, as well as Gappa and Interval.
Michael Soegtrop (Jun 04 2020 at 10:04):@Théo Zimmermann : what the time line for the release? I didn't start to look much into it, because until yesterday I really had 0 time and I thought it would more disturb than help if I get involved except with answering specific questions since timeline was early this week. But now it looks better on my side and also the time line looks more relaxed (which always happend in the past when doing the picking). If you say it is now more next week Monday ...
Théo Zimmermann (Jun 04 2020 at 10:05):I think we will release as soon as we are able to, which could be indeed around early next week.
Théo Zimmermann (Jun 04 2020 at 10:06):We are still waiting for a release summary (Matthieu is working on this) and a few infrastructure fixes in the refman.
Théo Zimmermann (Jun 04 2020 at 10:07):But if it turns out to take too long to find how to properly build some add-ons we may remove them from the beta installer to avoid further delaying the release.
Michael Soegtrop (Jun 04 2020 at 10:10):But if it turns out to take too long to find how to properly build some add-ons we may remove them from the beta installer to avoid further delaying the release.
Fair enough. I think for the beta it would be ok to take VST from my fork. The platform friendly build is fully working, even with 32 and 64 bit dual install. What is not working is support for some legacy build situations some people need, but I think it woul dbe fine to not have this in beta. I will discuss it with Andrew.
Michael Soegtrop (Jun 04 2020 at 10:10):So I take VST, CoqInterval and Gappa?
Théo Zimmermann (Jun 04 2020 at 10:11):Yes, thanks!
Michael Soegtrop (Jun 04 2020 at 10:17):OK. You also mentioned menhir above? What's the issue with it?
Michael Soegtrop (Jun 04 2020 at 10:17):OCaml 4.08 for the menhir executable or Coq 8.12 for the Coq library?
Théo Zimmermann (Jun 04 2020 at 10:18): Théo Zimmermann (Jun 04 2020 at 10:18): Michael Soegtrop (Jun 04 2020 at 10:18):It is dune based now?
Théo Zimmermann (Jun 04 2020 at 10:19):Yes.
Théo Zimmermann (Jun 04 2020 at 10:19):See the corresponding commit (a99b4da) in coq/coq#12415.
Théo Zimmermann (Jun 04 2020 at 10:19):See also the build failure in https://github.com/coq/coq/pull/12415#issuecomment-638711264.
Michael Soegtrop (Jun 04 2020 at 10:20):OK, that should be doable. So I can also look into menhir, but I will start with the other 3. When I am finished with these, I will let you know and we can discuss who does menhir.
Théo Zimmermann (Jun 04 2020 at 10:20):I thought menhir was a dependency of CompCert and thus VST, and this is why I started by looking into it.
Michael Soegtrop (Jun 04 2020 at 10:24):I thought menhir was a dependency of CompCert and thus VST, and this is why I started by looking into it.
Indeed, so I guess it is better if I start with menhir. Or I start with Gappa and Interval and you look into menhir meanhwile - as you prefer.
Théo Zimmermann (Jun 04 2020 at 10:24):I've spent too much time on this already and I'd like to attend to other issues so I'd be happy to give you the full hand on this PR.
Michael Soegtrop (Jun 04 2020 at 10:25):OK, fine. The dune discussion group is only a click away :-)
Michael Soegtrop (Jun 04 2020 at 10:26):So I will do Menhir, VST, Gappa and CoqInterval, likely in that order unless I get stuck somewhere.
Théo Zimmermann (Jun 05 2020 at 13:40):@Matthieu Sozeau We are getting closer and closer to being able to tag the beta. When do you think you will have the release summary ready?
Matthieu Sozeau (Jun 05 2020 at 13:41):I'm working on it this afternoon, I'll submit a PR by the evening
Matthieu Sozeau (Jun 05 2020 at 16:27):How do we count the merged PRs and closed issues since 8.11? I don't think we have a process for that, do we?
Matthieu Sozeau (Jun 05 2020 at 17:07):Doing a github search with "is:pr is:closed milestone:8.12+beta1 label:"kind: fix" " seems good enough
Théo Zimmermann (Jun 05 2020 at 20:16):Why only the fixes?
Matthieu Sozeau (Jun 05 2020 at 21:02):To know how many we fixed in the period
Théo Zimmermann (Jun 06 2020 at 16:47):Ah! But you could have filtered the closed issues in the milestone! coqbot adds issues automatically to the milestone of the PR that closed it.
Emilio Jesús Gallego Arias (Jun 08 2020 at 09:02):@Théo Zimmermann you want to target all fixes to 8.12.0 already, or these is time for the beta?
Emilio Jesús Gallego Arias (Jun 08 2020 at 09:02):For example https://github.com/coq/coq/pull/12471
Théo Zimmermann (Jun 08 2020 at 09:03):We don't know yet for sure when we will tag the beta as it depends on the completion of a few remaining PRs, so until we do, I'd say fixes should still target 8.12+beta1. We can easily postpone them when the time comes.
Emilio Jesús Gallego Arias (Jun 08 2020 at 09:04):Indeed, I'm readjusting at least one issue
Emilio Jesús Gallego Arias (Jun 08 2020 at 10:36):So things look pretty good right @Théo Zimmermann ? I guess https://github.com/coq/coq/pull/12103 is the last thing blocking the beta ?
[We can take care of the Release notes emsemble I think]
Théo Zimmermann (Jun 08 2020 at 10:39):coq/coq#12103 is not a blocker: if it is ready before the beta, good, if it is not, no problem: the URL we should advertise for the manual will be https://coq.github.io/doc/v8.12/refman, which is a moving target, therefore it is not a problem if a doc PR is not included in the beta (except the release summary of course).
Théo Zimmermann (Jun 08 2020 at 10:40):We should just give @Michael Soegtrop the day to finish his work on the add-ons. By the end of the day, if Gappa is not ready, I propose that we remove it from the beta (the rest of the add-ons should be OK).
Emilio Jesús Gallego Arias (Jun 08 2020 at 10:42):Sounds good, we can backport the last couple of fixes that went it today then, let's finish the release notes and maybe we can branch on Wed?
Emilio Jesús Gallego Arias (Jun 08 2020 at 10:42):we can tag I mean
Emilio Jesús Gallego Arias (Jun 08 2020 at 10:43):would you like to release on time for the Coq workshop? IMO is doable.
Théo Zimmermann (Jun 08 2020 at 10:43):Yeah, I was even hoping we could tag tomorrow, but maybe that's not actually realistic.
Emilio Jesús Gallego Arias (Jun 08 2020 at 10:43):Tomorrow sounds fine
Théo Zimmermann (Jun 08 2020 at 10:43):Emilio Jesús Gallego Arias said:
would you like to release on time for the Coq workshop? IMO is doable.
If the beta goes well (no unexpected serious problem), then yes.
Théo Zimmermann (Jun 11 2020 at 08:53):So, we are very very close to being able to tag. There are still two PRs targeting master and which are ready to merge @Emilio Jesús Gallego Arias (coq/coq#12481 and coq/coq#12492). In particular, I need the latter one to finish the add-on pinning.
Théo Zimmermann (Jun 11 2020 at 08:59):Besides this, the main remaining thing to discuss is what to do with the deprecation warnings for terms as hints (coq/coq#11970): leave it; remove it; or replace it by the proposal at coq/coq#12493.
Emilio Jesús Gallego Arias (Jun 11 2020 at 14:35):I think that PR seems to tricky for 8.12 IMHO
Emilio Jesús Gallego Arias (Jun 11 2020 at 15:05):One that we should maybe consider is https://github.com/coq/coq/pull/12479
Emilio Jesús Gallego Arias (Jun 11 2020 at 15:05):That seems to me like the kind of change that is important to have early
Théo Zimmermann (Jun 11 2020 at 16:14):Nah, we give reviewers a chance to have it merged in time. They didn't react. This is now 8.13 material.
Théo Zimmermann (Jun 11 2020 at 16:32):@Emilio Jesús Gallego Arias It looks like we are very very close to tag. I propose to postpone the last two issues and to close the milestone (it will signal not to add new PRs to the milestone but doesn't actually prevent us to add some, like the PR changing the version number).
Emilio Jesús Gallego Arias (Jun 11 2020 at 16:40):Sounds good @Théo Zimmermann , indeed we are ready to tag
Emilio Jesús Gallego Arias (Jun 11 2020 at 16:40):we need to add a note about OSX
Emilio Jesús Gallego Arias (Jun 11 2020 at 16:40):minimum version
Emilio Jesús Gallego Arias (Jun 11 2020 at 16:40):and little more
Emilio Jesús Gallego Arias (Jun 11 2020 at 16:40):I guess we want to merge the last PR before closing?
Emilio Jesús Gallego Arias (Jun 11 2020 at 16:41):Shall we announce the beta after the tag then?
Théo Zimmermann (Jun 11 2020 at 16:41):Emilio Jesús Gallego Arias said:
we need to add a note about OSX
The two previous releases (8.11.1 and 8.11.2) had the same limitation though. If you want to note it somewhere, it could be only in the GitHub release.
Théo Zimmermann (Jun 11 2020 at 16:42):Emilio Jesús Gallego Arias said:
I guess we want to merge the last PR before closing?
On the contrary, I was suggesting to close now, before it is empty, as a way of signaling that there should no longer be new PRs added to it.
Théo Zimmermann (Jun 11 2020 at 16:44):Emilio Jesús Gallego Arias said:
Shall we announce the beta after the tag then?
Usually, we announce to Coqdev as soon as the tag is put that packages are ready to be prepared, and then take the next day to update the website, create the release on GitHub, upload the installers, and do the proper announcement.
Emilio Jesús Gallego Arias (Jun 11 2020 at 16:48):Ok, let's close then
Théo Zimmermann (Jun 12 2020 at 07:15):We had an error in the Windows 32 bits build on v8.12. This was the first time that we tested it with all add-ons in fact (oops). That being said, it is "just" an out of memory error while building Coq-Elpi, so it is likely non systematic and I've thus restarted the job. But I won't put the tag before CI is fully green.
Enrico Tassi (Jun 12 2020 at 07:16):Coq-Elpi has one test about a huge inductive that is indeed memory hungry. You can probably disable it if it is a problem on 32 bits (I don't test it there)
Théo Zimmermann (Jun 12 2020 at 07:18):OK, can you open a PR that disables it? Depending on whether it fails twice in a row or not, we can decide to merge it before or after tagging the beta.
Enrico Tassi (Jun 12 2020 at 07:19):theories/derive/tests/test_bcongr.v uses ~3G here, as the name says it is a test so removing it from _CoqProject is not a problem
Enrico Tassi (Jun 12 2020 at 07:20):(3G on 8.11 and 64bit 4.07)
Enrico Tassi (Jun 12 2020 at 07:21):Théo Zimmermann said:
OK, can you open a PR that disables it? Depending on whether it fails twice in a row or not, we can decide to merge it before or after tagging the beta.
I can open a PR, but on which project and about what? A PR on coq-elpi removing the test? A PR adding a patch to the windows build?
Enrico Tassi (Jun 12 2020 at 07:24):How much memory do the worker have? I hope more than 3G
Enrico Tassi (Jun 12 2020 at 07:25):Also 32 bit should use less memory...
Théo Zimmermann (Jun 12 2020 at 08:42):A PR adjusting the Windows build. I should be able to do it myself with what you just explained.
Théo Zimmermann (Jun 12 2020 at 14:47):@Enrico Tassi Can you help me fix coq/coq#12501?
Enrico Tassi (Jun 12 2020 at 15:18):I closed the GH tab, ping me here again if you need me
Théo Zimmermann (Jun 12 2020 at 15:25):@Enrico Tassi For which ref did you prepare your patch? I cannot manage to apply it.
Enrico Tassi (Jun 12 2020 at 15:31):gares@ollypat:~/LPCIC/coq-elpi$ git describe
v1.4.1-1-gdcdf72a
I had an open windows, I did not think about it since these tests did not change in the last year or so
Enrico Tassi (Jun 12 2020 at 15:31):I'll push the commit on GH
Enrico Tassi (Jun 12 2020 at 15:32):on top of coq-master
Théo Zimmermann (Jun 12 2020 at 15:33):OK but I'd rather need it on top of coq-v8.12...
Enrico Tassi (Jun 12 2020 at 15:34):there you are
Théo Zimmermann (Jun 12 2020 at 15:34):Thanks
Enrico Tassi (Jun 12 2020 at 15:35):I still keep them disabled in coq-master, if ever we run the windows job...
Théo Zimmermann (Jun 12 2020 at 17:37):Hopefully, this time everything should work out fine. But let's still wait for CI to fully pass on v8.12 before tagging.
Théo Zimmermann (Jun 18 2020 at 14:24):I'm currently creating the GitHub release but it takes forever to upload the installers.
Emilio Jesús Gallego Arias (Jun 18 2020 at 14:25):I have a fast connection if that can hepl
Théo Zimmermann (Jun 18 2020 at 14:30):It's already ongoing, so I just need to wait now.
Karl Palmskog (Jun 18 2020 at 15:17):I'd just like to point out that 8.12+beta1 has been on core-dev OPAM for a while, perhaps you guys can ping Érik when the official release happens about the Docker images? Haven't seen him for a while here.
Karl Palmskog (Jun 19 2020 at 20:32):is there any Nix 8.12 version now (aside from the v8.12 coq-on-cachix) we can use in CI? If not, is this planned to happen soon?
Théo Zimmermann (Jun 20 2020 at 13:25):It has been merged into nixpkgs master. It should reach nixpkgs-unstable pretty soon.
Michael Soegtrop (Jun 29 2020 at 07:52):@Théo Zimmermann : I managed to come up with a platform friendly make file for VST and also a x86 CompCert opam package. There is already one merged (https://github.com/coq/opam-coq-archive/pull/1318) but doing further tests with VST I found that the installation method I chose there is not practical, so I did (https://github.com/coq/opam-coq-archive/pull/1319) to change it. In the end I decided to install variants in non standard folders where they can be linked from with -Q or -R. This is a bit inconvenient but all other solutions are quite complicated, hacky and errror prone. The way it is done in 8.12.beta essentially only supports 32 bit. I think we can leave it like this and do a 32+64 bit and possibly also a multi platform variant for the platform (I plan to do this during the Coq workshop next week).
Michael Soegtrop (Jun 29 2020 at 07:53):P.S.: the VST PR is (https://github.com/PrincetonUniversity/VST/pull/406)
P.P.S.: I did't have time to look into the CoqIDE issues and likely won't have time for this before Thursday.
Théo Zimmermann (Jun 29 2020 at 15:16):We will likely wait some time after the Coq workshop to release 8.12.0 anyway because having the two RMs also be the workshop organizers is a bit too much! :laughing:
Michael Soegtrop (Jun 30 2020 at 15:06):OK, this relaxes things a bit. Anyway I think I mixed up the Coq Workshop next week and the Coq User Workshop which I think was supposed to happen last week (https://github.com/coq/coq/wiki/Coq-Users-and-Developers-Workshop-2020). Did it actually take place last week? I will participate in the Coq Workshop Su/Mo and reserved the rest of the week to prepare the platform release, which then can happen shortly after the 8.12.0 release.
Théo Zimmermann (Jun 30 2020 at 17:45):It didn't happen in the end. I think it is supposed to be postponed and held virtually in automn.
Théo Zimmermann (Jul 09 2020 at 12:19):If everything goes well, we'll try to tag 8.12.0 next Friday (17th). No more PRs with overlays please.
Emilio Jesús Gallego Arias (Jul 09 2020 at 12:56):Milestone 8.12.1 should be created soon .
Emilio Jesús Gallego Arias (Jul 15 2020 at 09:09):Hi @Théo Zimmermann , so where we are at?
Emilio Jesús Gallego Arias (Jul 15 2020 at 09:10):We may discuss a couple of points in the call today, right? And then really freeze the branch?
Théo Zimmermann (Jul 15 2020 at 09:47):We really need to figure out how to fix https://github.com/coq/coq/issues/12657 (macOS job failing).
Théo Zimmermann (Jul 15 2020 at 09:50):And we need to take a decision on https://github.com/coq/coq/pull/12537 vs https://github.com/coq/coq/pull/12663 regarding the Search bug.
Théo Zimmermann (Jul 15 2020 at 09:50):These are the two main blockers that I can see.
Emilio Jesús Gallego Arias (Jul 15 2020 at 10:07):The OSX issue is unfortunate :S we need help from an OSX user
Emilio Jesús Gallego Arias (Jul 15 2020 at 10:07):Regarding Search I'd rather keep the semantics in < 8.12 , and leave @Gaëtan Gilbert patch to the kernel in master for some testing; for me it is too risky
Emilio Jesús Gallego Arias (Jul 15 2020 at 10:08):both PRs are complementary so that's not a problem
Emilio Jesús Gallego Arias (Jul 15 2020 at 10:08):yeah given the status of the milestone I think we will have to tag next week maybe
Théo Zimmermann (Jul 15 2020 at 10:19):Emilio Jesús Gallego Arias said:
The OSX issue is unfortunate :S we need help from an OSX user
I'm afraid an OSX user is not gonna suffice.
Hugo Herbelin (Jul 15 2020 at 16:50):Théo Zimmermann said:
And we need to take a decision on https://github.com/coq/coq/pull/12537 vs https://github.com/coq/coq/pull/12663 regarding the
Searchbug.
About #12537, to be on the safest side, but also so that the new features of Search are fully functional, I propose to make a (one-liner) fix one step closer to the original code (see my last comment there which explains the - avoidable - assumption made by the patch, AFAICS).
Emilio Jesús Gallego Arias (Jul 15 2020 at 17:46):@Hugo Herbelin I'd prefer https://github.com/coq/coq/pull/12693 I guess; what do you think?
Hugo Herbelin (Jul 15 2020 at 18:00):Emilio Jesús Gallego Arias said:
Hugo Herbelin I'd prefer https://github.com/coq/coq/pull/12693 I guess; what do you think?
https://github.com/coq/coq/pull/12693 looks nice indeed.
Paolo Giarrusso (Jul 15 2020 at 19:13):For the mac issue, I have a different suggestion, and I hope it's wrong: to get ruby 2.6, install ruby instead of ruby@2.6, and keep the same snapshost from 2019-09-03.
Paolo Giarrusso (Jul 15 2020 at 19:14):2.6.x was the latest Ruby release in September 2019, so I'd bet that's what you'd get — see the dates of these URLs:
https://www.ruby-lang.org/en/news/2018/12/25/ruby-2-6-0-released/
https://www.ruby-lang.org/en/news/2019/12/25/ruby-2-7-0-released/
Théo Zimmermann (Jul 15 2020 at 19:22):OK thanks for the suggestion. It's worth trying that indeed.
Théo Zimmermann (Jul 15 2020 at 19:23):But actually, our configuration never mentions ruby, it looks like it is just installed as a dependency of adwaita-icon-theme, so I'm not sure exactly what to change.
Théo Zimmermann (Jul 15 2020 at 19:26):I'm wondering if it's not just that the trick to pin homebrew is unsound and the database of known packages isn't in sync with the pin.
Paolo Giarrusso (Jul 15 2020 at 19:26):Hm, it's not even a dependency of that package
Paolo Giarrusso (Jul 15 2020 at 19:27):_however_
Paolo Giarrusso (Jul 15 2020 at 19:27):you're pinning the formulas but not Brew itself
Paolo Giarrusso (Jul 15 2020 at 19:27):also the image has a bunch of extra "taps" with more formulas that you don't need (and which might interfere)
Théo Zimmermann (Jul 15 2020 at 19:29):Any idea how to remove those?
Paolo Giarrusso (Jul 15 2020 at 19:29):there's brew untap, I can give you a command — but that's a side concern.
Paolo Giarrusso (Jul 15 2020 at 19:29):Conjecture: maybe you should pin Brew itself as well to an older version.
Théo Zimmermann (Jul 15 2020 at 19:30):Any idea how to proceed to do that?
Paolo Giarrusso (Jul 15 2020 at 19:30):At the very least, Brew itself still uses ruby 2.6.
Paolo Giarrusso (Jul 15 2020 at 19:31):/usr/local/Homebrew is a separate Git repo
Paolo Giarrusso (Jul 15 2020 at 19:31):$ cd /usr/local/Homebrew; git remote -v
origin https://github.com/Homebrew/brew (fetch)
origin https://github.com/Homebrew/brew (push)
Just pinning this repo as well to a version from this date would suffice to pin brew? No need to recompile anything? (I guess not: Ruby is interpreted)
Paolo Giarrusso (Jul 15 2020 at 19:34):Ruby is interpreted indeed, but I'm not a Ruby expert, and this is still an unsupported config
Paolo Giarrusso (Jul 15 2020 at 19:34):Still, I might try:
for i in homebrew/cask homebrew/services mongodb/brew github/gh aws/tap adoptopenjdk/openjdk; do brew untap $i; done Paolo Giarrusso (Jul 15 2020 at 19:35):I'm not sure how to stop brew from updating itself, but that might be a new enough feature
Paolo Giarrusso (Jul 15 2020 at 19:37):In retrospect, if that doesn't work, skipping brew and inlining the installation instructions from your old versions, maybe just for gtk, might be simpler.
Paolo Giarrusso (Jul 15 2020 at 19:39):IOW, bump Brew, use brew install gnu-time opam pkg-config adwaita-icon-theme without gtksourceview3, and install those libraries by hand (for this release)
Paolo Giarrusso (Jul 15 2020 at 19:40):Any of these choices is still duct tape, but bumping gtk version in a rush is more dangerous.
Théo Zimmermann (Jul 15 2020 at 19:42):Thanks for all the advice! I'll try what you suggested. Longer term, since it looks like reproducible builds still aren't supported by brew, I wonder if it might not be a good idea to get the required dependencies through Nix. Although, not being very knowledgeable in macOS packaging, there might be other issues lurking if we were to try that.
Paolo Giarrusso (Jul 15 2020 at 19:49):Hope that helps. AFAICS, Brew's "reproducible builds" weren't even meant to address this use case.
Paolo Giarrusso (Jul 15 2020 at 19:50):I've never learned to use Nix, so I'm not sure I can comment on that — except that Nix installs binaries in non-standard paths, some of those binaries embed those paths, and installing Nix on MacOs 10.15 (used to?) require some surgery.
Paolo Giarrusso (Jul 15 2020 at 19:50):But IANANE (I Am Not A Nix Expert).
Paolo Giarrusso (Jul 15 2020 at 19:52):So some/all of that might be unintentional FUD.
Paolo Giarrusso (Jul 15 2020 at 19:52):OTOH, if you "just" need to pin gtk. and maybe opam and adwaita-icon-theme (as I'd guessed), inlining installation of those libraries _might_ not be a bad idea.
Emilio Jesús Gallego Arias (Jul 16 2020 at 13:23):Ok, so I think we are close to be set modulo the OSX problem. https://github.com/coq/coq/pull/12678 is still a bit concerning tho and we didn't manage to get a quorum to discuss about it.
There are some recent PRs fixing notation bugs but I'm not sure if these should be delayed to 8.12.1
Théo Zimmermann (Jul 16 2020 at 13:26):I don't think coq/coq#12678 needs any discussion.
Théo Zimmermann (Jul 16 2020 at 13:27):The story is simple: devs agreed to deprecate, users were not happy, we undeprecate but keep a warning.
Emilio Jesús Gallego Arias (Jul 16 2020 at 13:30):Umm, what is the concrete problem these hints have
Emilio Jesús Gallego Arias (Jul 16 2020 at 13:30):we state they are fragile
Emilio Jesús Gallego Arias (Jul 16 2020 at 13:30):but we don't say why
Emilio Jesús Gallego Arias (Jul 16 2020 at 13:31):I'm not sure I'm happy with the warning enabled by default
Emilio Jesús Gallego Arias (Jul 16 2020 at 13:31):now users are going to see it
Emilio Jesús Gallego Arias (Jul 16 2020 at 13:31):and will wonder
Emilio Jesús Gallego Arias (Jul 16 2020 at 13:31):"can I ignore this"?
Emilio Jesús Gallego Arias (Jul 16 2020 at 13:31):if the answer is yes, the warning should only happen under +wall
Emilio Jesús Gallego Arias (Jul 16 2020 at 13:31):if the answer is not, we should provide some more details
Emilio Jesús Gallego Arias (Jul 16 2020 at 13:31):so call it a doc issue if you want
Théo Zimmermann (Jul 16 2020 at 13:47):OK, maybe this is still an issue, but this is a compromise between what @Pierre-Marie Pédrot wants and what users want. The current situation is that we have a deprecation warning and users are not happy about it, so I'd rather merge this PR rather than doing nothing.
Emilio Jesús Gallego Arias (Jul 16 2020 at 13:50):Sure we need to merge the PR, but we should improve the docs on two counts:
Emilio Jesús Gallego Arias (Jul 21 2020 at 22:15):@Théo Zimmermann I think we should be set for tomorrow; the OSX problem is IMHO best workarounded by ignoring the brew failure; it would be great to discuss a bit on the hints warning, but I think we can aim to tag after the call
Emilio Jesús Gallego Arias (Jul 21 2020 at 22:15):I tried to backport all remaining patchees, but ran into a problem with the setup; so I undid everything; a tad more documentation on this wouldn't hurt
Emilio Jesús Gallego Arias (Jul 21 2020 at 22:15):but the patches backport fine [conflicts are "dummy"]
Emilio Jesús Gallego Arias (Jul 21 2020 at 22:16):I can try the backport again if you give me the green light [my problem was related to the dummy commit, but I think I know how to workaround that now]
Théo Zimmermann (Jul 22 2020 at 09:14):I've noticed that you have moved manually some cards in the Coq 8.12 project, then backtracked. In principle, you never have to manage these cards manually. @coqbot takes care of moving them when you push the backports to v8.12.
Théo Zimmermann (Jul 22 2020 at 09:17):The way I generally proceed today is git checkout backport-v8.12 (the branch on which I prepare the backports and which is associated to coq/coq#12391), git reset --hard upstream/v8.12, dev/tools/backport-pr.sh --no-signature-check XXXX any number of times and git push --force-with-lease (to the backport-v8.12 branch on my fork) to trigger CI in the draft PR.
Théo Zimmermann (Jul 22 2020 at 09:17):This dummy commit thing needs taking care of only when you push to v8.12 if you want to make sure that the draft PR doesn't get closed.
Théo Zimmermann (Jul 22 2020 at 09:19):But I still don't see any backport of the Equations overlay, that would be necessary to be able to backport coq/coq#12523.
Emilio Jesús Gallego Arias (Jul 22 2020 at 11:17):The dummy commit thing is a bit confusing, specially as it removing .gitlab-ci which is the main goal of the PR to be open. I guess this should be documented a bit better ? [Or I missed for example the coqbot part]
I will backport the equations PR once I get the CI running
Emilio Jesús Gallego Arias (Jul 22 2020 at 11:32):I can re-try the backports if you give me the lock
Théo Zimmermann (Jul 22 2020 at 13:42):The dummy commit is just to keep the PR open when it is empty. I just gave you the instructions above on how I proceed. The fact that I start with a git reset --hard upstream/v8.12 is precisely to get rid of this dummy commit.
Emilio Jesús Gallego Arias (Jul 22 2020 at 14:34):Indeed, I was wondering where to add the instructions, maybe in RELEASE_PROCESS.md ?
Théo Zimmermann (Jul 22 2020 at 14:35):I pushed the easy backports to the backport-v8.12 branch. Feel free to push more on top (there's no dummy commit anymore).
Théo Zimmermann (Jul 22 2020 at 14:35):Emilio Jesús Gallego Arias said:
Indeed, I was wondering where to add the instructions, maybe in RELEASE_PROCESS.md ?
Here or in https://github.com/coq/coq/blob/master/CONTRIBUTING.md#release-management.
Emilio Jesús Gallego Arias (Jul 22 2020 at 14:36):Actually the reason I moved the cards manually was to signal I was adding the backports to the PR
Emilio Jesús Gallego Arias (Jul 22 2020 at 14:36):If I understand correctly now I'd have to scan manually the branch and the column to see what you added?
Emilio Jesús Gallego Arias (Jul 22 2020 at 14:37):Anyways I'm taking the lock, will push the remaining ones and prepare the overlays
Théo Zimmermann (Jul 22 2020 at 14:47):Yes, but what I did to signal the ones whose backport I already prepared was to move them to the bottom of the column.
Théo Zimmermann (Jul 22 2020 at 14:47):So the 7 bottom ones are the ones I pushed to the branch already.
Théo Zimmermann (Jul 22 2020 at 14:47):And none of the above.
Emilio Jesús Gallego Arias (Jul 22 2020 at 14:55):That's a good heuristic, thanks!
Emilio Jesús Gallego Arias (Jul 22 2020 at 14:56):I'm still puzzled about the OSX package :S
Emilio Jesús Gallego Arias (Jul 22 2020 at 14:56):maybe we can chat 5 minutes after the call?
Théo Zimmermann (Jul 22 2020 at 15:00):Very briefly possibly. I must be AFK for about an hour between 17.30 and 18.30.
Emilio Jesús Gallego Arias (Jul 22 2020 at 15:00):Yeah let's keep it very brief
Théo Zimmermann (Jul 22 2020 at 15:08):It looks like there is a new issue in the Windows build: https://gitlab.com/coq/coq/-/jobs/650943712
Is this a Cygwin mirror being down?
Emilio Jesús Gallego Arias (Jul 22 2020 at 15:11):Yup looks like a transient failure
Emilio Jesús Gallego Arias (Jul 22 2020 at 15:13):We are running late with the call :S
Emilio Jesús Gallego Arias (Jul 22 2020 at 15:13):So what should we do
Emilio Jesús Gallego Arias (Jul 22 2020 at 15:13):the issue is quite tricky I'm afraid
Emilio Jesús Gallego Arias (Jul 22 2020 at 15:13):Makefile.ide is doing very weird stuff to generate the GTK installer
Théo Zimmermann (Jul 22 2020 at 15:13):Maybe we can leave the call now and have a chat now on BBB?
Emilio Jesús Gallego Arias (Jul 22 2020 at 15:14):Ok I'm in your bbb room
Théo Zimmermann (Jul 22 2020 at 20:07):@Emilio Jesús Gallego Arias I shouldn't have backported coq/coq#12701 without updating VST (the consequence is a failing VST), and I'm waiting on Michael to do the VST update so I'm going to fix what I pushed earlier to backport-v8.12 (and consequently, the PR order in the Coq 8.12 project).
Emilio Jesús Gallego Arias (Jul 22 2020 at 20:20):Umm, shouldn't we just bump the vst_ref to something more recent?
Emilio Jesús Gallego Arias (Jul 22 2020 at 20:22):oh well, the windows package
Emilio Jesús Gallego Arias (Jul 22 2020 at 20:58):Ok, we should be almost set now
Emilio Jesús Gallego Arias (Jul 22 2020 at 20:58):IMHO we only want to merge the one PR for hints
Emilio Jesús Gallego Arias (Jul 22 2020 at 20:58):and the PR for the changelog
Emilio Jesús Gallego Arias (Jul 22 2020 at 20:59):Also we need to update the equations poitner
Emilio Jesús Gallego Arias (Jul 22 2020 at 20:59):as for vst, if it is not ready let's just disable the build in 8.12.0
Emilio Jesús Gallego Arias (Jul 22 2020 at 21:02):Will push to the branch once the CI completes
Emilio Jesús Gallego Arias (Jul 23 2020 at 12:21):Hey @Théo Zimmermann , so I think we are almost good, we should merge https://github.com/coq/coq/pull/12678 , then I'll backport the remaining changes, update https://github.com/coq/coq/pull/12734 , and we can merge the release commit and tag
Emilio Jesús Gallego Arias (Jul 23 2020 at 12:21):right?
Emilio Jesús Gallego Arias (Jul 23 2020 at 12:22):VST seems like I will have to stay in the pinned version
Théo Zimmermann (Jul 23 2020 at 12:23):Regarding VST, have you followed the e-mail exchange with Michael?
Emilio Jesús Gallego Arias (Jul 23 2020 at 12:24):I am a bit lost there
Théo Zimmermann (Jul 23 2020 at 12:24):Other than this, yes, I think that you covered everything remaining.
Emilio Jesús Gallego Arias (Jul 23 2020 at 12:25):CI seems to pass
Théo Zimmermann (Jul 23 2020 at 12:26):There is no issue with the current VST version, but it was a pinned commit specifically for the beta. VST is releasing a new version now and the idea was to include it in the Windows installer for 8.12.0.
Théo Zimmermann (Jul 23 2020 at 12:26):Michael is taking care of this but this has been delayed by some other things.
Théo Zimmermann (Jul 23 2020 at 12:26):So he's saying he should have something ready tonight.
Théo Zimmermann (Jul 23 2020 at 12:27):In any case, we'll use a version from his fork.
Emilio Jesús Gallego Arias (Jul 23 2020 at 12:29):I see thanks, so not a real showstopper I think. IMHO it is getting a bit late so 8.12 may have to include the beta version if we don't hear soon
Emilio Jesús Gallego Arias (Jul 23 2020 at 12:34):Ok rest of backports pushed to the CI branch
Emilio Jesús Gallego Arias (Jul 23 2020 at 13:00):I'm gonna adjust a few issues
Karl Palmskog (Jul 23 2020 at 13:04):sorry if I'm not keeping up with discussions/issues, etc., but what's the current release prognosis? 8.12.0 soon or another beta?
Emilio Jesús Gallego Arias (Jul 23 2020 at 13:05):8.12.0 today
Emilio Jesús Gallego Arias (Jul 23 2020 at 13:05):8.12.1 in Sep
Emilio Jesús Gallego Arias (Jul 23 2020 at 13:27):@Théo Zimmermann so i was wondering if an additional column in the release project would help
Emilio Jesús Gallego Arias (Jul 23 2020 at 13:28):to signal that a backport is pending CI
Théo Zimmermann (Jul 23 2020 at 13:29):Possibly. I used to have one, before I wrote the automation to manage the project.
Emilio Jesús Gallego Arias (Jul 23 2020 at 13:30)::+1:
Emilio Jesús Gallego Arias (Jul 23 2020 at 13:30):Ok so I think in around 1-hour the branch will be ready
Emilio Jesús Gallego Arias (Jul 23 2020 at 13:30):pending adjustments on the overlays for packages if needed
Emilio Jesús Gallego Arias (Jul 23 2020 at 13:31):Seems in good shape; tho it is quite a noisy release in terms of warnings [hints, omega, etc...]
Emilio Jesús Gallego Arias (Jul 23 2020 at 14:29):Ok, CI is almost ready, will push to 8.12 soon
Emilio Jesús Gallego Arias (Jul 23 2020 at 15:25):@Théo Zimmermann I've noticed that there seems to be a hanging changelog
Emilio Jesús Gallego Arias (Jul 23 2020 at 15:25):due to it using .md?
Théo Zimmermann (Jul 23 2020 at 15:25):That's typical :frown:
Emilio Jesús Gallego Arias (Jul 23 2020 at 15:25):Indeed that needs fixing
Emilio Jesús Gallego Arias (Jul 23 2020 at 15:26):let me prepare the PR
Théo Zimmermann (Jul 23 2020 at 15:27):OK, note that it is missing from the 8.12+beta1 section, not the 8.12.0 section.
Emilio Jesús Gallego Arias (Jul 23 2020 at 15:29):ok pr done
Michael Soegtrop (Jul 23 2020 at 18:32):I am a bit confused about the new file types. Which of the files generated by coqc do I have to install?
Théo Zimmermann (Jul 23 2020 at 19:51):@Michael Soegtrop If you are talking about vos / vok I think you don't have to install any of them.
Emilio Jesús Gallego Arias (Jul 23 2020 at 20:10):Thanks @Théo Zimmermann , PR backported
Emilio Jesús Gallego Arias (Jul 23 2020 at 20:10):will rebase release commit as soon as CI is OK
Emilio Jesús Gallego Arias (Jul 23 2020 at 20:53):ok everything is ready , for some reason github didn't update https://github.com/coq/coq/pull/12735 after my push to 8.12 but that PR contains only one extra commit
Théo Zimmermann (Jul 24 2020 at 07:32):Yes, I noticed this behavior already. GitHub only update PR commits when you push directly to their branch, and not when you push to the base branch.
Michael Soegtrop (Jul 24 2020 at 08:42):Théo Zimmermann said:
Michael Soegtrop If you are talking about
vos/vokI think you don't have to install any of them.
Yes, I was aksing about .vos/.vok. I wonder why coq itself installs a few of these.
Also: should I install .glob files? The documentation says that these are intended for coqdoc. Is it so that when I don't install them and someone creates documentation for a dependent project, this wouldn't reference the pre installed library sources properly? Are there also uses in editors?
And I can't say I understand what the .aux files are good for.
Emilio Jesús Gallego Arias (Jul 24 2020 at 12:55):Here's the windows installer of what essentially is the release if anyone wants to test.
Emilio Jesús Gallego Arias (Jul 24 2020 at 12:55):https://gitlab.com/coq/coq/-/jobs/654490347/artifacts/browse/artifacts/
Emilio Jesús Gallego Arias (Jul 24 2020 at 12:55):@Théo Zimmermann I let you tag
Théo Zimmermann (Jul 24 2020 at 12:55):OK
Ralf Jung (Jul 25 2020 at 08:07):If nobody already did that, I'll create opam packages
Ralf Jung (Jul 25 2020 at 08:36):https://github.com/ocaml/opam-repository/pull/16876
Théo Zimmermann (Jul 27 2020 at 08:24):@Maxime Dénès Can you send a request to the person signing Windows packages at Inria to sign the Windows installers for 8.12.0 (available at https://gitlab.com/coq/coq/-/jobs/655496286/artifacts/file/artifacts/coq-8.12.0-installer-windows-x86_64.exe and https://gitlab.com/coq/coq/-/jobs/655496287/artifacts/file/artifacts/coq-8.12.0-installer-windows-i686.exe) or let me know who this person is and what's the process to contact them?
Maxime Dénès (Jul 27 2020 at 08:25):Sure, I'll send you an e-mail.
Théo Zimmermann (Jul 27 2020 at 09:25):@Maxime Dénès and @Pierre-Marie Pédrot: I'm currently attempting to follow the instructions at https://github.com/coq/coq/wiki/SigningReleases. After having created the SSH tunel, I run vncviewer localhost in another terminal and get a single field to enter the password, no field for the username. From the e-mail of Vincent, I thought I would also get a field for the username, where I would need to type ci and where I could check the keyboard layout (I'm already on a US keyboard anyway). In the end, my authentication attempts get rejected.
Pierre-Marie Pédrot (Jul 27 2020 at 09:28):So, it's a mess.
Pierre-Marie Pédrot (Jul 27 2020 at 09:29):The password that Vincent sent us is not correct IIUC.
Pierre-Marie Pédrot (Jul 27 2020 at 09:29):It's correct up to a keyboard translation error.
Théo Zimmermann (Jul 27 2020 at 09:30):Ah OK, thanks for the clarification.
Théo Zimmermann (Jul 27 2020 at 09:30):I'll try to reverse engineer the correct password then.
Pierre-Marie Pédrot (Jul 27 2020 at 09:31):I can retry connecting myself to give you more input
Théo Zimmermann (Jul 27 2020 at 09:31):Let me try first, and I'll let you know.
Pierre-Marie Pédrot (Jul 27 2020 at 09:31):OK.
Pierre-Marie Pédrot (Jul 27 2020 at 09:32):also the signing script is horribly outdated
Pierre-Marie Pédrot (Jul 27 2020 at 09:32):with laborious help from @Maxime Dénès we managed to sign the package
Théo Zimmermann (Jul 27 2020 at 09:32):But you didn't update the wiki page?
Pierre-Marie Pédrot (Jul 27 2020 at 09:33):partially
Pierre-Marie Pédrot (Jul 27 2020 at 09:33):but if anything this would need a fresh script
Pierre-Marie Pédrot (Jul 27 2020 at 09:33):and I hadn't time then so...
Théo Zimmermann (Jul 27 2020 at 09:36):OK, I failed in my attempt to reverse engineer the password. Can you try to login again?
Théo Zimmermann (Jul 27 2020 at 10:31):The signing tuto says to run coq_dowload to get the sources? Do we really need the sources in addition to the binary to sign the binary?
Théo Zimmermann (Jul 27 2020 at 11:30)::victory: all installers have been signed
Théo Zimmermann (Jul 27 2020 at 12:42):I've edited the signing documentation and the prepare.sh script. It should be much more straightforward to sign the macOS package next time.
Jason Gross (Jul 30 2020 at 06:52):I believe .aux files store information about proof scripts so that the second time you evaluate a file in async mode, it can skip even the proofs that don't have Proof using, and can also know which proofs it's not worth spawning a worker thread for
Michael Soegtrop (Jul 31 2020 at 10:33):Jason Gross said:
I believe .aux files store information about proof scripts so that the second time you evaluate a file in async mode, it can skip even the proofs that don't have Proof using, and can also know which proofs it's not worth spawning a worker thread for
thanks for the explanation. So this means it doesn't make sense to install them for libraries since they are just an optimization for recompiling files one anyway uses in compiled form. And even if one steps through a library file it will still work - it is just an optimization.
Emilio Jesús Gallego Arias (Sep 09 2020 at 14:47):After discussion in the Coq Call today we may want to move forward the planned date for 8.12.1 a bit
Emilio Jesús Gallego Arias (Sep 09 2020 at 14:47):@Théo Zimmermann what do you think about targeting a candidate for end of next week?
Emilio Jesús Gallego Arias (Sep 09 2020 at 14:48):I will take care of the issues assigned to me, @Hugo Herbelin would also like to push a few fixes for notations needed by SF
Théo Zimmermann (Sep 09 2020 at 15:13):Sure, we can try.
Théo Zimmermann (Sep 09 2020 at 15:14):I've already backported most of the backlog. For https://github.com/coq/coq/pull/12881, I'm waiting on a confirmation.
Hugo Herbelin (Sep 16 2020 at 06:09):Emilio Jesús Gallego Arias said:
I will take care of the issues assigned to me, Hugo Herbelin would also like to push a few fixes for notations needed by SF
I made #13026 for SF and I believe that this is all they need.
As far as the 8.2.1 PRs I made are concerned, #13026, #12999, #12960, #12946 are looking for an assignee (they are quite simple).
Emilio Jesús Gallego Arias (Sep 16 2020 at 11:59):Noted, thanks Hugo, may give it a go today.
Emilio Jesús Gallego Arias (Sep 17 2020 at 16:28):@Théo Zimmermann how are we doing with this?
Emilio Jesús Gallego Arias (Sep 17 2020 at 16:28):I'm positive I want to ship a couple of patches for 8.12
Emilio Jesús Gallego Arias (Sep 17 2020 at 16:29):one in particular is required to make Dune work with native, as it fixes a bug we discovered with testing
Théo Zimmermann (Sep 17 2020 at 16:31):Backporting queue is almost empty but this is not the case of the 8.12.1 milestone. Personally, I wouldn't mind putting the tag as soon as coq/coq#12919 is merged and backported.
Théo Zimmermann (Sep 17 2020 at 16:32):The other bug fixes could wait. There will be an 8.12.2 release.
Théo Zimmermann (Sep 17 2020 at 16:32):That being said, if people want a couple more days to merge a few PRs, that's not a problem either.
Théo Zimmermann (Sep 17 2020 at 16:33):We should also recheck the installers before we tag.
Emilio Jesús Gallego Arias (Sep 17 2020 at 16:34):When would you ideally like to have the cut off?
Emilio Jesús Gallego Arias (Sep 17 2020 at 16:35):#12895 is pretty serious tho, i can take care of it soon
Emilio Jesús Gallego Arias (Sep 17 2020 at 16:35):Also a couple of Hugo's PR should strongly go in, but I think I can handle these now
Théo Zimmermann (Sep 17 2020 at 16:51):I don't have any preference regarding the cutoff date, but let's avoid delaying it too much since it seemed quite urgent to produce a new release for some users.
Emilio Jesús Gallego Arias (Sep 22 2020 at 17:48):I am gonna focus on the remaining TODO on my part for this, @Théo Zimmermann I'll move some issues to 8.12.2 so please have a look later on to see if something looks off to you.
Théo Zimmermann (Sep 22 2020 at 17:49):Sure, though I don't see much that would be blocking.
Théo Zimmermann (Sep 22 2020 at 17:49):As I said before, I'm still waiting on a review / merge of coq/coq#12919.
Théo Zimmermann (Sep 22 2020 at 17:49):I've already taken care of backporting all the PRs in the queue so far.
Théo Zimmermann (Sep 22 2020 at 17:50):However, we have a serious issue with Windows packaging (cf. coq/coq#13065). This one will be blocking the release until it is fixed / worked around.
Emilio Jesús Gallego Arias (Sep 22 2020 at 18:19):Yeah that's pretty serious, maybe we could just pin the corresponding cygwin packages?
Emilio Jesús Gallego Arias (Sep 22 2020 at 18:19):That should not be too hard
Emilio Jesús Gallego Arias (Sep 22 2020 at 18:19):We could also release and do the windows package later
Théo Zimmermann (Sep 23 2020 at 08:00):Pinning seems more complex than expected. See the discussion in the issue.
Théo Zimmermann (Sep 23 2020 at 08:01):We could also release and do the windows package later
If it takes too long to fix, maybe.
Théo Zimmermann (Oct 01 2020 at 07:26):@Emilio Jesús Gallego Arias Do you have any remaining blocking issue for 8.12.1? For my part, after the Windows packaging fix and backporting the quotation fix, I don't. We should just prepare the release notes PR and have some people recheck the packages before tagging.
Emilio Jesús Gallego Arias (Oct 01 2020 at 14:02):Yes I have a couple of things I'll like to get in; I'll process them today.
Emilio Jesús Gallego Arias (Oct 01 2020 at 14:02):Pity the path issue is more tricky than it looks, I'll try to improve it too
Théo Zimmermann (Oct 05 2020 at 09:36):@Emilio Jesús Gallego Arias Any update?
Emilio Jesús Gallego Arias (Oct 05 2020 at 20:04):@Théo Zimmermann I'm busy with my talk tomorrow, but after the seminar I shall be able to get everything done, sorry for the delay
Emilio Jesús Gallego Arias (Oct 05 2020 at 20:04):Only critical fix is change in the patch we added for Dune + native
Emilio Jesús Gallego Arias (Oct 05 2020 at 20:04):So Dune + native can work in 8.12.1
Emilio Jesús Gallego Arias (Oct 05 2020 at 20:04):yeah there we issues due to the way libraries are located
Théo Zimmermann (Oct 05 2020 at 21:24):What is this patch? I didn't see it in the 8.12.1 milestone.
Emilio Jesús Gallego Arias (Oct 06 2020 at 18:39):It is a one liner on the specific native output dir flag; I'm too tired to test it today sorry; will submit and hopefully finish the rest tomorrow, sorry again.
Théo Zimmermann (Oct 07 2020 at 09:48):No worries.
Théo Zimmermann (Oct 13 2020 at 09:45):@Emilio Jesús Gallego Arias Shall we move forward on releasing 8.12.1 and just stop trying to add new bug fixes in it?
Maxime Dénès (Oct 13 2020 at 12:01):The distance to the closest bug fix is divided by two every week :)
Emilio Jesús Gallego Arias (Oct 14 2020 at 17:15):Ok @Théo Zimmermann , sorry for the delay, I've submitted https://github.com/coq/coq/pull/13193 which would be great to have in 8.12.1 if possible, for the rest we can delay tho I'm gonna try to address the open bugs now that I finished that one which was the prioritary for me.
Théo Zimmermann (Oct 14 2020 at 17:21):Great news!
Emilio Jesús Gallego Arias (Oct 15 2020 at 11:06):Ok, all other two bugs now have PRs that fix them and in theory could be backported
Emilio Jesús Gallego Arias (Oct 19 2020 at 10:23):Hey @Théo Zimmermann , so we may try to release this week then? The pending PRs themselves are pretty trivial I think.
Théo Zimmermann (Oct 19 2020 at 10:24):Sure, it has waited long enough!
Emilio Jesús Gallego Arias (Oct 19 2020 at 10:26):So let's go for it, we need assignees for the PRs tho
Théo Zimmermann (Nov 10 2020 at 09:29):@Emilio Jesús Gallego Arias I'd like an opinion from you whether to backport or not coq/coq#13284.
Théo Zimmermann (Nov 10 2020 at 09:30):Then, I suppose we also need to wait for coq/coq#13331 to be in since it fixes a proof of False.
Théo Zimmermann (Nov 10 2020 at 09:31):Other than this, I was ready to open the PR bumping the version number in v8.12.
Emilio Jesús Gallego Arias (Nov 10 2020 at 13:27):Thanks @Théo Zimmermann , regarding the bug, the API breakage is very unlikely to have any impact, so I'd go with the maintainers, for the critical bug we need to discuss a bit more as I think there is still some fishy going but indeed seems like a good idea to wait :S , fix should be merged very soon I think.
Last updated: Dec 01 2023 at 04:01 UTC