Stream: Coq devs & plugin devs

Topic: 8.12 release thread


view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Théo Zimmermann (May 15 2020 at 15:19):

So, we should probably reorder the two corresponding checkboxes.

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Enrico Tassi (May 15 2020 at 15:20):

(I won't be able to prepare it before monday afternoon)

view this post on Zulip 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.

view this post on Zulip Emilio Jesús Gallego Arias (May 15 2020 at 15:21):

Sounds good

view this post on Zulip Enrico Tassi (May 15 2020 at 15:21):

As you like

view this post on Zulip Enrico Tassi (May 15 2020 at 15:21):

less work for me ;-)

view this post on Zulip 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

view this post on Zulip Théo Zimmermann (May 15 2020 at 15:23):

Yes.

view this post on Zulip 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.

view this post on Zulip Enrico Tassi (May 15 2020 at 15:23):

It would be nice, but your PR 11158 is not exactly trivial

view this post on Zulip 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.

view this post on Zulip Théo Zimmermann (May 15 2020 at 15:24):

A lot of it is already generated by a script

view this post on Zulip Théo Zimmermann (May 15 2020 at 15:25):

(dev/tools/update-compat.py)

view this post on Zulip Enrico Tassi (May 15 2020 at 15:25):

You are right, I did not read the paragraph at the end

view this post on Zulip 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?

view this post on Zulip Théo Zimmermann (May 15 2020 at 15:25):

It looks like it isn't in sync with the latest changes...

view this post on Zulip Enrico Tassi (May 15 2020 at 15:26):

hum, no, I did the silly thing. It says copy "this" and I interpreted it strictly

view this post on Zulip Enrico Tassi (May 15 2020 at 15:26):

let me update it

view this post on Zulip Emilio Jesús Gallego Arias (May 15 2020 at 15:28):

Which one is not in sync? I guess the one in dev/doc ?

view this post on Zulip Théo Zimmermann (May 15 2020 at 15:29):

The one in dev/doc is the correct reference.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Théo Zimmermann (May 15 2020 at 15:34):

This does look more up-to-date to me :slight_smile:

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Théo Zimmermann (May 16 2020 at 18:05):

Let's create a needs: next release branch

view this post on Zulip Théo Zimmermann (May 16 2020 at 18:05):

Since the needs: labels are checked by the merging script.

view this post on Zulip 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).

view this post on Zulip Emilio Jesús Gallego Arias (May 16 2020 at 18:09):

Yeah this is something the bot could do

view this post on Zulip 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).

view this post on Zulip 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.)

view this post on Zulip Emilio Jesús Gallego Arias (May 18 2020 at 10:28):

Hugo, we are about to branch

view this post on Zulip Hugo Herbelin (May 18 2020 at 10:29):

OK

view this post on Zulip Emilio Jesús Gallego Arias (May 18 2020 at 10:29):

I don't see anything urgent, thanks; stuff seems under control.

view this post on Zulip 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

view this post on Zulip Emilio Jesús Gallego Arias (May 18 2020 at 10:30):

We can always backport if we think delaying is a mistake

view this post on Zulip 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?

view this post on Zulip Théo Zimmermann (May 18 2020 at 10:31):

Nope, all is good!

view this post on Zulip 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?

view this post on Zulip Enrico Tassi (May 18 2020 at 15:52):

Oh, I see emilio told me in a PR, ok

view this post on Zulip 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

view this post on Zulip Théo Zimmermann (May 18 2020 at 15:55):

(so that would be f123874, cf. our comments on this commit)

view this post on Zulip Théo Zimmermann (May 18 2020 at 16:00):

Well, never mind. We haven't been very consistent in this practice anyway.

view this post on Zulip Enrico Tassi (May 18 2020 at 16:01):

uff... I'll fit that, but I don't what would be the difference

view this post on Zulip Enrico Tassi (May 18 2020 at 16:02):

fixed

view this post on Zulip 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?

view this post on Zulip Théo Zimmermann (May 18 2020 at 16:04):

In the past, there were many alpha commits that targeted merge commits.

view this post on Zulip 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

view this post on Zulip Théo Zimmermann (May 18 2020 at 16:05):

Yep, the spec is a bit imprecise.

view this post on Zulip Enrico Tassi (May 18 2020 at 16:05):

To me the first commit landing in master is the merge one

view this post on Zulip Théo Zimmermann (May 18 2020 at 16:05):

It used to be my interpretation as well.

view this post on Zulip Théo Zimmermann (May 18 2020 at 16:06):

But like I said, that's not a big deal.

view this post on Zulip 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

view this post on Zulip Enrico Tassi (May 18 2020 at 16:06):

Can you explain why?

view this post on Zulip Emilio Jesús Gallego Arias (May 18 2020 at 16:07):

use git log --topo-order

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Emilio Jesús Gallego Arias (May 18 2020 at 16:07):

so if you tag the merge commit

view this post on Zulip Emilio Jesús Gallego Arias (May 18 2020 at 16:07):

the commit that is actually merged

view this post on Zulip Emilio Jesús Gallego Arias (May 18 2020 at 16:07):

won't be considered to be part of 8.13

view this post on Zulip Emilio Jesús Gallego Arias (May 18 2020 at 16:08):

but won't be part of 8.12 either

view this post on Zulip 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

view this post on Zulip Emilio Jesús Gallego Arias (May 18 2020 at 16:09):

git describe for example would have found the 8.12 parent

view this post on Zulip Emilio Jesús Gallego Arias (May 18 2020 at 16:09):

incorrectly, this was discussed in 8.10/8.11 I believe

view this post on Zulip Enrico Tassi (May 18 2020 at 16:10):

ok, that is a good reason. I'll clarify the doc

view this post on Zulip Emilio Jesús Gallego Arias (May 18 2020 at 16:10):

Thanks

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Emilio Jesús Gallego Arias (May 18 2020 at 16:16):

We can test the first backport soon

view this post on Zulip Théo Zimmermann (May 18 2020 at 16:19):

Yes, but let's pin ci-basic-overlay.sh first.

view this post on Zulip 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

view this post on Zulip Emilio Jesús Gallego Arias (May 29 2020 at 10:17):

right?

view this post on Zulip 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

view this post on Zulip Emilio Jesús Gallego Arias (May 29 2020 at 10:18):

WDYT?

view this post on Zulip Emilio Jesús Gallego Arias (May 29 2020 at 10:24):

Two main blockers:

view this post on Zulip 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:

view this post on Zulip 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.

view this post on Zulip 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).

view this post on Zulip Emilio Jesús Gallego Arias (May 29 2020 at 12:43):

OSX packages should be actually testable right now, right?

view this post on Zulip 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

view this post on Zulip Emilio Jesús Gallego Arias (May 29 2020 at 12:44):

I'm pretty unhappy with the approach used in the Windows build

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Théo Zimmermann (May 29 2020 at 12:49):

(which should make this obsolete)

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip Emilio Jesús Gallego Arias (Jun 02 2020 at 16:46):

WDYT?

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Emilio Jesús Gallego Arias (Jun 02 2020 at 17:30):

The only positive point would be if migrating does make our life easier

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Théo Zimmermann (Jun 02 2020 at 17:31):

But I wouldn't keep both even for a limited period.

view this post on Zulip Emilio Jesús Gallego Arias (Jun 02 2020 at 17:31):

:+1:

view this post on Zulip 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:

view this post on Zulip Emilio Jesús Gallego Arias (Jun 02 2020 at 17:32):

I'll finish the PR tomorrow

view this post on Zulip Emilio Jesús Gallego Arias (Jun 02 2020 at 17:32):

then we see how the diff looks

view this post on Zulip Emilio Jesús Gallego Arias (Jun 02 2020 at 17:32):

and make a choice

view this post on Zulip 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

view this post on Zulip Emilio Jesús Gallego Arias (Jun 02 2020 at 17:32):

my win VM is almost ready

view this post on Zulip Théo Zimmermann (Jun 02 2020 at 17:40):

OK

view this post on Zulip Emilio Jesús Gallego Arias (Jun 03 2020 at 13:14):

Regarding the IDE issues, I'm unsure what to do with them.

view this post on Zulip Théo Zimmermann (Jun 03 2020 at 13:18):

One of them is certainly not a regression so could easily be postponed.

view this post on Zulip 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.

view this post on Zulip 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)

https://coq.gitlab.io/-/coq/-/jobs/578951538/artifacts/artifacts/buildlogs/unicoq-68ed13294ea8860a8c39950f7ca2ff0aa7211b9f-make_err.txt

Do you know how to interpret this? Could it be related to coq/coq#12421? (I only tested after backporting this PR.)

view this post on Zulip 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

view this post on Zulip Théo Zimmermann (Jun 03 2020 at 14:03):

Oh OK, so the easiest solution is to downgrad OCaml to 4.07, right?

view this post on Zulip Emilio Jesús Gallego Arias (Jun 03 2020 at 14:03):

See https://github.com/coq/coq/issues/12067

view this post on Zulip Emilio Jesús Gallego Arias (Jun 03 2020 at 14:03):

I think for now yes

view this post on Zulip 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?

view this post on Zulip Théo Zimmermann (Jun 04 2020 at 08:53):

@Michael Soegtrop thanks for asking! I definitely need your help. See coq/coq#12415.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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 ...

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Michael Soegtrop (Jun 04 2020 at 10:10):

So I take VST, CoqInterval and Gappa?

view this post on Zulip Théo Zimmermann (Jun 04 2020 at 10:11):

Yes, thanks!

view this post on Zulip Michael Soegtrop (Jun 04 2020 at 10:17):

OK. You also mentioned menhir above? What's the issue with it?

view this post on Zulip Michael Soegtrop (Jun 04 2020 at 10:17):

OCaml 4.08 for the menhir executable or Coq 8.12 for the Coq library?

view this post on Zulip Théo Zimmermann (Jun 04 2020 at 10:18):

  1. Menhirlib used to be in its own repo. It has moved to a subfolder of the Menhir repo.

view this post on Zulip Théo Zimmermann (Jun 04 2020 at 10:18):

  1. I've tried to adapt the build of Menhir (the latest release doesn't have a Makefile anymore) but failed to do so.

view this post on Zulip Michael Soegtrop (Jun 04 2020 at 10:18):

It is dune based now?

view this post on Zulip Théo Zimmermann (Jun 04 2020 at 10:19):

Yes.

view this post on Zulip Théo Zimmermann (Jun 04 2020 at 10:19):

See the corresponding commit (a99b4da) in coq/coq#12415.

view this post on Zulip Théo Zimmermann (Jun 04 2020 at 10:19):

See also the build failure in https://github.com/coq/coq/pull/12415#issuecomment-638711264.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Michael Soegtrop (Jun 04 2020 at 10:25):

OK, fine. The dune discussion group is only a click away :-)

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip Matthieu Sozeau (Jun 05 2020 at 13:41):

I'm working on it this afternoon, I'll submit a PR by the evening

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip Théo Zimmermann (Jun 05 2020 at 20:16):

Why only the fixes?

view this post on Zulip Matthieu Sozeau (Jun 05 2020 at 21:02):

To know how many we fixed in the period

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip Emilio Jesús Gallego Arias (Jun 08 2020 at 09:02):

For example https://github.com/coq/coq/pull/12471

view this post on Zulip 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.

view this post on Zulip Emilio Jesús Gallego Arias (Jun 08 2020 at 09:04):

Indeed, I'm readjusting at least one issue

view this post on Zulip 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]

view this post on Zulip 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).

view this post on Zulip 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).

view this post on Zulip 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?

view this post on Zulip Emilio Jesús Gallego Arias (Jun 08 2020 at 10:42):

we can tag I mean

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Emilio Jesús Gallego Arias (Jun 08 2020 at 10:43):

Tomorrow sounds fine

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Emilio Jesús Gallego Arias (Jun 11 2020 at 14:35):

I think that PR seems to tricky for 8.12 IMHO

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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).

view this post on Zulip Emilio Jesús Gallego Arias (Jun 11 2020 at 16:40):

Sounds good @Théo Zimmermann , indeed we are ready to tag

view this post on Zulip Emilio Jesús Gallego Arias (Jun 11 2020 at 16:40):

we need to add a note about OSX

view this post on Zulip Emilio Jesús Gallego Arias (Jun 11 2020 at 16:40):

minimum version

view this post on Zulip Emilio Jesús Gallego Arias (Jun 11 2020 at 16:40):

and little more

view this post on Zulip Emilio Jesús Gallego Arias (Jun 11 2020 at 16:40):

I guess we want to merge the last PR before closing?

view this post on Zulip Emilio Jesús Gallego Arias (Jun 11 2020 at 16:41):

Shall we announce the beta after the tag then?

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Emilio Jesús Gallego Arias (Jun 11 2020 at 16:48):

Ok, let's close then

view this post on Zulip 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.

view this post on Zulip 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)

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Enrico Tassi (Jun 12 2020 at 07:20):

(3G on 8.11 and 64bit 4.07)

view this post on Zulip 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?

view this post on Zulip Enrico Tassi (Jun 12 2020 at 07:24):

How much memory do the worker have? I hope more than 3G

view this post on Zulip Enrico Tassi (Jun 12 2020 at 07:25):

Also 32 bit should use less memory...

view this post on Zulip 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.

view this post on Zulip Théo Zimmermann (Jun 12 2020 at 14:47):

@Enrico Tassi Can you help me fix coq/coq#12501?

view this post on Zulip Enrico Tassi (Jun 12 2020 at 15:18):

I closed the GH tab, ping me here again if you need me

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Enrico Tassi (Jun 12 2020 at 15:31):

I'll push the commit on GH

view this post on Zulip Enrico Tassi (Jun 12 2020 at 15:32):

on top of coq-master

view this post on Zulip Théo Zimmermann (Jun 12 2020 at 15:33):

OK but I'd rather need it on top of coq-v8.12...

view this post on Zulip Enrico Tassi (Jun 12 2020 at 15:34):

there you are

view this post on Zulip Théo Zimmermann (Jun 12 2020 at 15:34):

Thanks

view this post on Zulip Enrico Tassi (Jun 12 2020 at 15:35):

I still keep them disabled in coq-master, if ever we run the windows job...

view this post on Zulip 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.

view this post on Zulip Théo Zimmermann (Jun 18 2020 at 14:24):

I'm currently creating the GitHub release but it takes forever to upload the installers.

view this post on Zulip Emilio Jesús Gallego Arias (Jun 18 2020 at 14:25):

I have a fast connection if that can hepl

view this post on Zulip Théo Zimmermann (Jun 18 2020 at 14:30):

It's already ongoing, so I just need to wait now.

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip Théo Zimmermann (Jun 20 2020 at 13:25):

It has been merged into nixpkgs master. It should reach nixpkgs-unstable pretty soon.

view this post on Zulip 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).

view this post on Zulip 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.

view this post on Zulip 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:

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Emilio Jesús Gallego Arias (Jul 09 2020 at 12:56):

Milestone 8.12.1 should be created soon .

view this post on Zulip Emilio Jesús Gallego Arias (Jul 15 2020 at 09:09):

Hi @Théo Zimmermann , so where we are at?

view this post on Zulip 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?

view this post on Zulip 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).

view this post on Zulip 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.

view this post on Zulip Théo Zimmermann (Jul 15 2020 at 09:50):

These are the two main blockers that I can see.

view this post on Zulip Emilio Jesús Gallego Arias (Jul 15 2020 at 10:07):

The OSX issue is unfortunate :S we need help from an OSX user

view this post on Zulip 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

view this post on Zulip Emilio Jesús Gallego Arias (Jul 15 2020 at 10:08):

both PRs are complementary so that's not a problem

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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 Search bug.

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).

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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/

view this post on Zulip Théo Zimmermann (Jul 15 2020 at 19:22):

OK thanks for the suggestion. It's worth trying that indeed.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Paolo Giarrusso (Jul 15 2020 at 19:26):

Hm, it's not even a dependency of that package

view this post on Zulip Paolo Giarrusso (Jul 15 2020 at 19:27):

_however_

view this post on Zulip Paolo Giarrusso (Jul 15 2020 at 19:27):

you're pinning the formulas but not Brew itself

view this post on Zulip 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)

view this post on Zulip Théo Zimmermann (Jul 15 2020 at 19:29):

Any idea how to remove those?

view this post on Zulip Paolo Giarrusso (Jul 15 2020 at 19:29):

there's brew untap, I can give you a command — but that's a side concern.

view this post on Zulip Paolo Giarrusso (Jul 15 2020 at 19:29):

Conjecture: maybe you should pin Brew itself as well to an older version.

view this post on Zulip Théo Zimmermann (Jul 15 2020 at 19:30):

Any idea how to proceed to do that?

view this post on Zulip Paolo Giarrusso (Jul 15 2020 at 19:30):

At the very least, Brew itself still uses ruby 2.6.

view this post on Zulip Paolo Giarrusso (Jul 15 2020 at 19:31):

/usr/local/Homebrew is a separate Git repo

view this post on Zulip 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)

view this post on Zulip Théo Zimmermann (Jul 15 2020 at 19:34):

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)

view this post on Zulip 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

view this post on Zulip Paolo Giarrusso (Jul 15 2020 at 19:34):

Still, I might try:

  1. remove taps by for i in homebrew/cask homebrew/services mongodb/brew github/gh aws/tap adoptopenjdk/openjdk; do brew untap $i; done
  2. checking out an old commit in that repo as well.

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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)

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Paolo Giarrusso (Jul 15 2020 at 19:50):

But IANANE (I Am Not A Nix Expert).

view this post on Zulip Paolo Giarrusso (Jul 15 2020 at 19:52):

So some/all of that might be unintentional FUD.

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Théo Zimmermann (Jul 16 2020 at 13:26):

I don't think coq/coq#12678 needs any discussion.

view this post on Zulip 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.

view this post on Zulip Emilio Jesús Gallego Arias (Jul 16 2020 at 13:30):

Umm, what is the concrete problem these hints have

view this post on Zulip Emilio Jesús Gallego Arias (Jul 16 2020 at 13:30):

we state they are fragile

view this post on Zulip Emilio Jesús Gallego Arias (Jul 16 2020 at 13:30):

but we don't say why

view this post on Zulip Emilio Jesús Gallego Arias (Jul 16 2020 at 13:31):

I'm not sure I'm happy with the warning enabled by default

view this post on Zulip Emilio Jesús Gallego Arias (Jul 16 2020 at 13:31):

now users are going to see it

view this post on Zulip Emilio Jesús Gallego Arias (Jul 16 2020 at 13:31):

and will wonder

view this post on Zulip Emilio Jesús Gallego Arias (Jul 16 2020 at 13:31):

"can I ignore this"?

view this post on Zulip Emilio Jesús Gallego Arias (Jul 16 2020 at 13:31):

if the answer is yes, the warning should only happen under +wall

view this post on Zulip Emilio Jesús Gallego Arias (Jul 16 2020 at 13:31):

if the answer is not, we should provide some more details

view this post on Zulip Emilio Jesús Gallego Arias (Jul 16 2020 at 13:31):

so call it a doc issue if you want

view this post on Zulip 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.

view this post on Zulip 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:

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Emilio Jesús Gallego Arias (Jul 21 2020 at 22:15):

but the patches backport fine [conflicts are "dummy"]

view this post on Zulip 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]

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Emilio Jesús Gallego Arias (Jul 22 2020 at 11:32):

I can re-try the backports if you give me the lock

view this post on Zulip 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.

view this post on Zulip 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 ?

view this post on Zulip 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).

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Théo Zimmermann (Jul 22 2020 at 14:47):

So the 7 bottom ones are the ones I pushed to the branch already.

view this post on Zulip Théo Zimmermann (Jul 22 2020 at 14:47):

And none of the above.

view this post on Zulip Emilio Jesús Gallego Arias (Jul 22 2020 at 14:55):

That's a good heuristic, thanks!

view this post on Zulip Emilio Jesús Gallego Arias (Jul 22 2020 at 14:56):

I'm still puzzled about the OSX package :S

view this post on Zulip Emilio Jesús Gallego Arias (Jul 22 2020 at 14:56):

maybe we can chat 5 minutes after the call?

view this post on Zulip 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.

view this post on Zulip Emilio Jesús Gallego Arias (Jul 22 2020 at 15:00):

Yeah let's keep it very brief

view this post on Zulip 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?

view this post on Zulip Emilio Jesús Gallego Arias (Jul 22 2020 at 15:11):

Yup looks like a transient failure

view this post on Zulip Emilio Jesús Gallego Arias (Jul 22 2020 at 15:13):

We are running late with the call :S

view this post on Zulip Emilio Jesús Gallego Arias (Jul 22 2020 at 15:13):

So what should we do

view this post on Zulip Emilio Jesús Gallego Arias (Jul 22 2020 at 15:13):

the issue is quite tricky I'm afraid

view this post on Zulip Emilio Jesús Gallego Arias (Jul 22 2020 at 15:13):

Makefile.ide is doing very weird stuff to generate the GTK installer

view this post on Zulip Théo Zimmermann (Jul 22 2020 at 15:13):

Maybe we can leave the call now and have a chat now on BBB?

view this post on Zulip Emilio Jesús Gallego Arias (Jul 22 2020 at 15:14):

Ok I'm in your bbb room

view this post on Zulip 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).

view this post on Zulip Emilio Jesús Gallego Arias (Jul 22 2020 at 20:20):

Umm, shouldn't we just bump the vst_ref to something more recent?

view this post on Zulip Emilio Jesús Gallego Arias (Jul 22 2020 at 20:22):

oh well, the windows package

view this post on Zulip Emilio Jesús Gallego Arias (Jul 22 2020 at 20:58):

Ok, we should be almost set now

view this post on Zulip Emilio Jesús Gallego Arias (Jul 22 2020 at 20:58):

IMHO we only want to merge the one PR for hints

view this post on Zulip Emilio Jesús Gallego Arias (Jul 22 2020 at 20:58):

and the PR for the changelog

view this post on Zulip Emilio Jesús Gallego Arias (Jul 22 2020 at 20:59):

Also we need to update the equations poitner

view this post on Zulip 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

view this post on Zulip Emilio Jesús Gallego Arias (Jul 22 2020 at 21:02):

Will push to the branch once the CI completes

view this post on Zulip 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

view this post on Zulip Emilio Jesús Gallego Arias (Jul 23 2020 at 12:21):

right?

view this post on Zulip Emilio Jesús Gallego Arias (Jul 23 2020 at 12:22):

VST seems like I will have to stay in the pinned version

view this post on Zulip Théo Zimmermann (Jul 23 2020 at 12:23):

Regarding VST, have you followed the e-mail exchange with Michael?

view this post on Zulip Emilio Jesús Gallego Arias (Jul 23 2020 at 12:24):

I am a bit lost there

view this post on Zulip Théo Zimmermann (Jul 23 2020 at 12:24):

Other than this, yes, I think that you covered everything remaining.

view this post on Zulip Emilio Jesús Gallego Arias (Jul 23 2020 at 12:25):

CI seems to pass

view this post on Zulip 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.

view this post on Zulip Théo Zimmermann (Jul 23 2020 at 12:26):

Michael is taking care of this but this has been delayed by some other things.

view this post on Zulip Théo Zimmermann (Jul 23 2020 at 12:26):

So he's saying he should have something ready tonight.

view this post on Zulip Théo Zimmermann (Jul 23 2020 at 12:27):

In any case, we'll use a version from his fork.

view this post on Zulip 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

view this post on Zulip Emilio Jesús Gallego Arias (Jul 23 2020 at 12:34):

Ok rest of backports pushed to the CI branch

view this post on Zulip Emilio Jesús Gallego Arias (Jul 23 2020 at 13:00):

I'm gonna adjust a few issues

view this post on Zulip 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?

view this post on Zulip Emilio Jesús Gallego Arias (Jul 23 2020 at 13:05):

8.12.0 today

view this post on Zulip Emilio Jesús Gallego Arias (Jul 23 2020 at 13:05):

8.12.1 in Sep

view this post on Zulip 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

view this post on Zulip Emilio Jesús Gallego Arias (Jul 23 2020 at 13:28):

to signal that a backport is pending CI

view this post on Zulip Théo Zimmermann (Jul 23 2020 at 13:29):

Possibly. I used to have one, before I wrote the automation to manage the project.

view this post on Zulip Emilio Jesús Gallego Arias (Jul 23 2020 at 13:30):

:+1:

view this post on Zulip Emilio Jesús Gallego Arias (Jul 23 2020 at 13:30):

Ok so I think in around 1-hour the branch will be ready

view this post on Zulip Emilio Jesús Gallego Arias (Jul 23 2020 at 13:30):

pending adjustments on the overlays for packages if needed

view this post on Zulip 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...]

view this post on Zulip Emilio Jesús Gallego Arias (Jul 23 2020 at 14:29):

Ok, CI is almost ready, will push to 8.12 soon

view this post on Zulip 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

view this post on Zulip Emilio Jesús Gallego Arias (Jul 23 2020 at 15:25):

due to it using .md?

view this post on Zulip Théo Zimmermann (Jul 23 2020 at 15:25):

That's typical :frown:

view this post on Zulip Emilio Jesús Gallego Arias (Jul 23 2020 at 15:25):

Indeed that needs fixing

view this post on Zulip Emilio Jesús Gallego Arias (Jul 23 2020 at 15:26):

let me prepare the PR

view this post on Zulip 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.

view this post on Zulip Emilio Jesús Gallego Arias (Jul 23 2020 at 15:29):

ok pr done

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip Emilio Jesús Gallego Arias (Jul 23 2020 at 20:10):

Thanks @Théo Zimmermann , PR backported

view this post on Zulip Emilio Jesús Gallego Arias (Jul 23 2020 at 20:10):

will rebase release commit as soon as CI is OK

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Michael Soegtrop (Jul 24 2020 at 08:42):

Théo Zimmermann said:

Michael Soegtrop If you are talking about vos / vok I 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.

view this post on Zulip 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.

view this post on Zulip Emilio Jesús Gallego Arias (Jul 24 2020 at 12:55):

https://gitlab.com/coq/coq/-/jobs/654490347/artifacts/browse/artifacts/

view this post on Zulip Emilio Jesús Gallego Arias (Jul 24 2020 at 12:55):

@Théo Zimmermann I let you tag

view this post on Zulip Théo Zimmermann (Jul 24 2020 at 12:55):

OK

view this post on Zulip Ralf Jung (Jul 25 2020 at 08:07):

If nobody already did that, I'll create opam packages

view this post on Zulip Ralf Jung (Jul 25 2020 at 08:36):

https://github.com/ocaml/opam-repository/pull/16876

view this post on Zulip 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?

view this post on Zulip Maxime Dénès (Jul 27 2020 at 08:25):

Sure, I'll send you an e-mail.

view this post on Zulip 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.

view this post on Zulip Pierre-Marie Pédrot (Jul 27 2020 at 09:28):

So, it's a mess.

view this post on Zulip Pierre-Marie Pédrot (Jul 27 2020 at 09:29):

The password that Vincent sent us is not correct IIUC.

view this post on Zulip Pierre-Marie Pédrot (Jul 27 2020 at 09:29):

It's correct up to a keyboard translation error.

view this post on Zulip Théo Zimmermann (Jul 27 2020 at 09:30):

Ah OK, thanks for the clarification.

view this post on Zulip Théo Zimmermann (Jul 27 2020 at 09:30):

I'll try to reverse engineer the correct password then.

view this post on Zulip Pierre-Marie Pédrot (Jul 27 2020 at 09:31):

I can retry connecting myself to give you more input

view this post on Zulip Théo Zimmermann (Jul 27 2020 at 09:31):

Let me try first, and I'll let you know.

view this post on Zulip Pierre-Marie Pédrot (Jul 27 2020 at 09:31):

OK.

view this post on Zulip Pierre-Marie Pédrot (Jul 27 2020 at 09:32):

also the signing script is horribly outdated

view this post on Zulip Pierre-Marie Pédrot (Jul 27 2020 at 09:32):

with laborious help from @Maxime Dénès we managed to sign the package

view this post on Zulip Théo Zimmermann (Jul 27 2020 at 09:32):

But you didn't update the wiki page?

view this post on Zulip Pierre-Marie Pédrot (Jul 27 2020 at 09:33):

partially

view this post on Zulip Pierre-Marie Pédrot (Jul 27 2020 at 09:33):

but if anything this would need a fresh script

view this post on Zulip Pierre-Marie Pédrot (Jul 27 2020 at 09:33):

and I hadn't time then so...

view this post on Zulip 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?

view this post on Zulip 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?

view this post on Zulip Théo Zimmermann (Jul 27 2020 at 11:30):

:victory: all installers have been signed

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip Théo Zimmermann (Sep 09 2020 at 15:13):

Sure, we can try.

view this post on Zulip 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.

view this post on Zulip 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).

view this post on Zulip Emilio Jesús Gallego Arias (Sep 16 2020 at 11:59):

Noted, thanks Hugo, may give it a go today.

view this post on Zulip Emilio Jesús Gallego Arias (Sep 17 2020 at 16:28):

@Théo Zimmermann how are we doing with this?

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Théo Zimmermann (Sep 17 2020 at 16:32):

The other bug fixes could wait. There will be an 8.12.2 release.

view this post on Zulip 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.

view this post on Zulip Théo Zimmermann (Sep 17 2020 at 16:33):

We should also recheck the installers before we tag.

view this post on Zulip Emilio Jesús Gallego Arias (Sep 17 2020 at 16:34):

When would you ideally like to have the cut off?

view this post on Zulip Emilio Jesús Gallego Arias (Sep 17 2020 at 16:35):

#12895 is pretty serious tho, i can take care of it soon

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Théo Zimmermann (Sep 22 2020 at 17:49):

Sure, though I don't see much that would be blocking.

view this post on Zulip 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.

view this post on Zulip Théo Zimmermann (Sep 22 2020 at 17:49):

I've already taken care of backporting all the PRs in the queue so far.

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip Emilio Jesús Gallego Arias (Sep 22 2020 at 18:19):

That should not be too hard

view this post on Zulip Emilio Jesús Gallego Arias (Sep 22 2020 at 18:19):

We could also release and do the windows package later

view this post on Zulip Théo Zimmermann (Sep 23 2020 at 08:00):

Pinning seems more complex than expected. See the discussion in the issue.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Théo Zimmermann (Oct 05 2020 at 09:36):

@Emilio Jesús Gallego Arias Any update?

view this post on Zulip 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

view this post on Zulip Emilio Jesús Gallego Arias (Oct 05 2020 at 20:04):

Only critical fix is change in the patch we added for Dune + native

view this post on Zulip Emilio Jesús Gallego Arias (Oct 05 2020 at 20:04):

So Dune + native can work in 8.12.1

view this post on Zulip Emilio Jesús Gallego Arias (Oct 05 2020 at 20:04):

yeah there we issues due to the way libraries are located

view this post on Zulip Théo Zimmermann (Oct 05 2020 at 21:24):

What is this patch? I didn't see it in the 8.12.1 milestone.

view this post on Zulip 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.

view this post on Zulip Théo Zimmermann (Oct 07 2020 at 09:48):

No worries.

view this post on Zulip 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?

view this post on Zulip Maxime Dénès (Oct 13 2020 at 12:01):

The distance to the closest bug fix is divided by two every week :)

view this post on Zulip 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.

view this post on Zulip Théo Zimmermann (Oct 14 2020 at 17:21):

Great news!

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Théo Zimmermann (Oct 19 2020 at 10:24):

Sure, it has waited long enough!

view this post on Zulip Emilio Jesús Gallego Arias (Oct 19 2020 at 10:26):

So let's go for it, we need assignees for the PRs tho

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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: Oct 16 2021 at 01:03 UTC