Stream: Coq Platform devs & users

Topic: 8.12.2 release


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

@Michael Soegtrop V8.12.2 is available now (and is almost identical to 8.12.1 up to two fixes) so I suggest that you focus on releasing a platform Windows installer for this version instead of 8.12.1 (and then we can sign it and distribute it on https://github.com/coq/coq/releases/tag/V8.12.2).

view this post on Zulip Michael Soegtrop (Dec 11 2020 at 17:23):

@Théo Zimmermann : sure, I will update the 8.12 branch. I am doing some last tests (e.g. Max and homebrew) and writing some additional instructions and then its time for a release.

view this post on Zulip Michael Soegtrop (Dec 14 2020 at 09:48):

@Théo Zimmermann : I am now ready with 8.12.1 - everything tested, readme files polished ... I wonder if I should tag this state but not publicly release it and then update to 8.12.2. Some packages test for explicit Coq version numbers and need to be adjusted to 8.12.2 (e.g. VST).

How is the proecdure for the signed installers? I do a tag, we build this e.g. on one of the build servers and then I attach it afterwards to the release?

view this post on Zulip Théo Zimmermann (Dec 14 2020 at 13:59):

Yes, making a tag for 8.12.1.0 and waiting for 8.12.2.0 to publicly release sounds good to me.

view this post on Zulip Théo Zimmermann (Dec 14 2020 at 14:00):

To sign a Windows installer, we need to send it to someone at Inria. See https://github.com/coq/coq/blob/master/dev/doc/release-process.md#these-steps-are-the-same-for-all-releases-beta-final-patch-level.

view this post on Zulip Théo Zimmermann (Dec 14 2020 at 14:02):

Then, we can add the Windows installer for 8.12.2 to the GitHub release (https://github.com/coq/coq/releases/tag/V8.12.2) just like Enrico did for 8.13+beta1.

view this post on Zulip Michael Soegtrop (Dec 14 2020 at 19:23):

@Théo Zimmermann : I just created the 8.12.1.0 release, but as discussed I won't announce it publically yet. I think i should anyway create a signed installer since this version is really extensively tested and I think it should be archived for reference even if we switch to 8.12.2 very soon.

view this post on Zulip Michael Soegtrop (Dec 15 2020 at 09:09):

@Théo Zimmermann : I just created the 8.12.2.0 tag/release. How shall we proceed with the Windows installer? Shall I build it (also the one for 8.12.1) locally on the release runner and you pick it from there?

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

Yes, we can do like this.

view this post on Zulip Michael Soegtrop (Dec 15 2020 at 09:11):

OK, I will start it now and ping you when it is finished.

view this post on Zulip Michael Soegtrop (Dec 15 2020 at 09:12):

I start with 8.12.2 and then do the 8.12.1.

view this post on Zulip Michael Soegtrop (Dec 15 2020 at 09:13):

How about a 32 bit installer? Do you think it is required or shall we do this first on 8.13?

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

If it's easy, it would be good to provide it. If it doesn't work yet, it can wait.

view this post on Zulip Michael Soegtrop (Dec 15 2020 at 13:21):

@Théo Zimmermann : The installer is finished, but it seems to have an issue. I think the compiled GTK resource file is missing, so opening a dialog crashes it - I see what I can do about it.

view this post on Zulip Théo Zimmermann (Dec 16 2020 at 09:08):

OK. Let me know if this is something you think will be fixed easily or not so that I know whether to announce 8.12.2 now or wait for the signed Windows installer before doing so. Thanks again for all your work!

view this post on Zulip Michael Soegtrop (Dec 16 2020 at 09:10):

Should be easy to fix - I just fear that the CI maintenance scripts deleted my test build from yesterday, so I have to start from scratch, which takes a few hours to build.

view this post on Zulip Michael Soegtrop (Dec 17 2020 at 11:29):

@Théo Zimmermann : I am still on this (was a bit held up by the CI issue in Enrico's PR). CoqIDE works now also in more thorough tests, but some stuff like style files are still missing.

There are btw. quite some differences between the old and new installer, so I think for 8.12.2 you should also build and publish the legacy installer (I have seen there is no as yet - not sure if your plan was to publish the platform one). Both have some stuff one - as far as I can tell - doesn't need (the legacy one a lot of cmo/cma/cmx files - the new one some Ocaml stuff).

view this post on Zulip Théo Zimmermann (Dec 17 2020 at 11:35):

My plan was indeed not to provide the legacy installer because Windows CI has been broken since gcc was updated in Cygwin. I now have a PR fixing CI in master by bumping OCaml to 4.10.2 (https://github.com/coq/coq/pull/13650) but I don't think it will work with all add-ons in v8.12 because IIRC even OCaml 4.08 didn't. Fixing the failure could also be done by patching Coq as in the opam-repository, but I was not planning to do it.

view this post on Zulip Michael Soegtrop (Dec 17 2020 at 11:43):

I see. Well then I will test it a bit more and then we should go for it. It would be a good test. In case I miss a serious detail, we can still have a 8.12.3.

view this post on Zulip Théo Zimmermann (Dec 17 2020 at 11:46):

I've also opened https://github.com/coq/coq/pull/13653 for v8.12 now using a patch that @Paolo Giarrusso pointed me to. If it works, then I will feel bad at having been too lazy to even try that before. But if I do end up generating a Windows installer with this commit, I will still call it 8.12.2 because the content will be the same.

view this post on Zulip Théo Zimmermann (Dec 17 2020 at 12:35):

So it turns out that simply applying this patch wasn't enough to fix the build. I won't try further.

view this post on Zulip Michael Soegtrop (Dec 17 2020 at 14:24):

OK. I will do some final adjustments to the platform installer later today, test it and then you can use this.

view this post on Zulip Théo Zimmermann (Dec 17 2020 at 19:23):

Thanks!

view this post on Zulip Michael Soegtrop (Dec 18 2020 at 11:58):

@Théo Zimmermann : I am still looking at all the gtksourceview language and style files. I think I need 5 of them in addition to the Coq specific files. Do you think I should simply add all (the old installer did that), compressed about 250k, or should I pick the files I need. The latter might lead to hard to find maintenance issues if something changes here, although that is not so super likely.

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

I would add all of them indeed!

view this post on Zulip Michael Soegtrop (Dec 18 2020 at 12:08):

That's also what I thought. Thanks!

view this post on Zulip Michael Soegtrop (Dec 18 2020 at 13:35):

@Théo Zimmermann : I put an 8.12.2 64 bit installer on coq-windows in folder C:\installer. It survived some basic tests and smoke tests.

view this post on Zulip Michael Soegtrop (Dec 18 2020 at 13:36):

A 32 bit installer is a bit more work but hopefully not that much - @Enrico Tassi already fixed quite a few bugs in that.

view this post on Zulip Théo Zimmermann (Dec 18 2020 at 21:58):

@Michael Soegtrop how long the installer is going to survive without being removed by the clean-up scripts? I won't have access to a computer before tomorrow.

view this post on Zulip Michael Soegtrop (Dec 18 2020 at 23:02):

I put it outside of the CI folder, so it will be there until it is manually deleted.

view this post on Zulip Théo Zimmermann (Dec 21 2020 at 08:36):

Thanks, I've retrieved the installer and I've sent it for signature.

view this post on Zulip Théo Zimmermann (Dec 21 2020 at 08:37):

Hopefully the person in charge of signing packages is not yet on vacation.

view this post on Zulip Théo Zimmermann (Dec 21 2020 at 08:37):

Otherwise, it may wait for two weeks.

view this post on Zulip Michael Soegtrop (Dec 21 2020 at 09:01):

@Théo Zimmermann : thanks! I will also do a 32 bit installer today.

view this post on Zulip Karl Palmskog (Dec 21 2020 at 09:21):

@Michael Soegtrop any chance for the general VST-2.7 package in the Coq opam archive before new year? I was hoping to update my VST stuff to 64 bit (including my template project)

view this post on Zulip Michael Soegtrop (Dec 21 2020 at 10:34):

@Karl Palmskog : on the way. I needed two patches to the tag of Andrew and also one patch to CompCert 3.8 to get everything working. The CompCert patch I will submit to opam, but for VST I would prefer to have the tag changed. If it helps I can create a public opam package for VST 2.7 which points to the release-2.7 branch of VST (I created it yesterday) and update it later to point to the updated tag. But I would expect that we can have a new tag soon.

view this post on Zulip Karl Palmskog (Dec 21 2020 at 11:15):

releases based on tags are preferable. I guess I can always do some custom VST-2.7 locally until the tag-based release appears. I just noticed I had some spare time until new year and that 2.7 was nearly out.

view this post on Zulip Karl Palmskog (Dec 21 2020 at 11:16):

VST is probably at the top of my ranking of "most difficult Coq project to build/install/depend on" (without opam)


Last updated: Jan 29 2023 at 19:02 UTC