Stream: Coq devs & plugin devs

Topic: Coq 8.11.2 release plans


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

Hello @Pierre-Marie Pédrot, I was wondering if you had any plans to ever release an 8.11.2 version since you hadn't backported anything since the 8.11.1 release. Now I see that you've just backported a batch of 11 PRs. Do you know when you'd like to release 8.11.2? From my point of view, the ideal would be to tag 8.11.2 before 8.12+beta1 because that would avoid having to think about presenting release notes for a non-linear release history, but that's up to you of course.

view this post on Zulip Pierre-Marie Pédrot (May 12 2020 at 08:10):

Indeed, this series of backports was motivated by the upcoming branch. I'll try to tag it on time.

view this post on Zulip Pierre-Marie Pédrot (May 14 2020 at 14:31):

Can I get somebody to merge https://github.com/coq/coq/pull/12327? Once done I should be able to tag quickly after.

view this post on Zulip Théo Zimmermann (May 14 2020 at 14:43):

Done

view this post on Zulip Pierre-Marie Pédrot (May 14 2020 at 14:48):

Thanks.

view this post on Zulip Pierre-Marie Pédrot (May 14 2020 at 20:35):

I've just tagged the 8.11.2.

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

FTR I just updated the "current" doc (https://coq.inria.fr/refman/ and https://coq.inria.fr/stdlib/) to point to 8.11.2, anticipating a bit on the release announcement.

view this post on Zulip Théo Zimmermann (May 26 2020 at 14:38):

@Pierre-Marie Pédrot When do you intend to publish / announce the 8.11.2 release?

view this post on Zulip Pierre-Marie Pédrot (May 26 2020 at 14:42):

I was waiting for news from the binary packages, I should probably ping the relevant people

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

Still no news from the people signing packages?

view this post on Zulip Maxime Dénès (Jun 05 2020 at 20:39):

The packages were signed on May, 28th.

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

Thanks for the info! @Pierre-Marie Pédrot It would be nice to announce the 8.11.2 release ASAP so that it comes before the 8.12+beta1 announcement.

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

@Pierre-Marie Pédrot Ping

view this post on Zulip Pierre-Marie Pédrot (Jun 09 2020 at 14:52):

Ah, right, sorry I forgot about this. Since I have not the right credentials, and haven't contacted @Vincent Laporte, the MacOS packages are not signed though.

view this post on Zulip Pierre-Marie Pédrot (Jun 09 2020 at 14:52):

(Processes with a truck factor of 1 are really a PITA by the way.)

view this post on Zulip Pierre-Marie Pédrot (Jun 09 2020 at 14:54):

I'll upload the Windows packages in the meantime, although that means publishing officially the release on GitHub

view this post on Zulip Pierre-Marie Pédrot (Jun 13 2020 at 13:41):

The website PR is pending, I am waiting for a review

view this post on Zulip Pierre-Marie Pédrot (Jun 13 2020 at 13:41):

As for the MacOS packages, still haven't had time to send an email to Vincent

view this post on Zulip Pierre-Marie Pédrot (Jun 13 2020 at 13:41):

Writing e-mails is a huge friction for me...

view this post on Zulip Pierre-Marie Pédrot (Jun 13 2020 at 13:42):

I'd have preferred wasting time trying to replicate the VM signing, but I am missing the credentials.

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

Pierre-Marie Pédrot said:

I'd have preferred wasting time trying to replicate the VM signing, but I am missing the credentials.

Really? I think you can get them from @Maxime Dénès too.

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

PR reviewed

view this post on Zulip Pierre-Marie Pédrot (Jun 13 2020 at 13:54):

No, last news were that @Maxime Dénès was unable to connect to the VM

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

OK, do you want me to write to Vincent to get the credentials for both you and me?

view this post on Zulip Pierre-Marie Pédrot (Jun 13 2020 at 13:57):

@Théo Zimmermann that would definitely help, thanks.

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

Is your GPG key available somewhere publicly or on a keyserver? Can you give me a fingerprint?

view this post on Zulip Notification Bot (Jun 13 2020 at 14:00):

This topic was moved here from #coq-community devs & users > Tips for @CoqLang tweets by Théo Zimmermann

view this post on Zulip Pierre-Marie Pédrot (Jun 13 2020 at 14:01):

BA47 A91F 9104 E721 84D7 0F6D 7922 C01F D9BA 3C7B

view this post on Zulip Pierre-Marie Pédrot (Jun 13 2020 at 14:14):

I've merged the 8.11.2 release announcement, otherwise it's going to delay you for the 8.12beta announcement

view this post on Zulip Pierre-Marie Pédrot (Jun 13 2020 at 14:14):

I'll update the MacOS package when available

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

@Pierre-Marie Pédrot Do you plan to send an announcement of the 8.11.2 release on Coq-Club / Discourse eventually? Did you manage to sign the macOS packages?

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

@Pierre-Marie Pédrot ping

view this post on Zulip Pierre-Marie Pédrot (Jun 16 2020 at 16:35):

I was fairly busy until today, I'll try to have a look at the signing tonight probably

view this post on Zulip Pierre-Marie Pédrot (Jun 16 2020 at 22:17):

Unfortunately it seems like the Azure CI has garbage collected the MacOS binary package, I'll push a temporary branch to recompile it

view this post on Zulip Pierre-Marie Pédrot (Jun 16 2020 at 22:19):

hopefully it will compile succesfully during the night :lucky:

view this post on Zulip Pierre-Marie Pédrot (Jun 17 2020 at 11:29):

I cannot connect the VNC client to the OSX machine it seems

view this post on Zulip Pierre-Marie Pédrot (Jun 17 2020 at 11:29):

on the ci-inria machine I get the following debug output

view this post on Zulip Pierre-Marie Pédrot (Jun 17 2020 at 11:29):

debug1: Connection to port 5900 forwarding to coq-osx1 port 5900 requested.
debug2: fd 9 setting TCP_NODELAY
debug2: fd 9 setting O_NONBLOCK
debug3: fd 9 is O_NONBLOCK
debug1: channel 3: new [direct-tcpip]
debug3: send packet: type 90
debug3: receive packet: type 92
channel 3: open failed: administratively prohibited: open failed
debug2: channel 3: zombie
debug2: channel 3: garbage collecting
debug1: channel 3: free: direct-tcpip: listening port 5900 for coq-osx1 port 5900, connect from ::1 port 57144 to ::1 port 5900, nchannels 4
debug3: channel 3: status: The following connections are open:
  #2 client-session (t4 r0 i0/0 o0/0 e[write]/0 fd 6/7/8 sock -1 cc -1)

view this post on Zulip Pierre-Marie Pédrot (Jun 17 2020 at 11:30):

note the scary "administratively prohibited"

view this post on Zulip Pierre-Marie Pédrot (Jun 17 2020 at 11:36):

ah, but the server is down, I have to launch it manually...

view this post on Zulip Pierre-Marie Pédrot (Jun 17 2020 at 11:55):

coq-osx1 doesn't seem to want to boot, despite several attempts: https://ci.inria.fr/project/coq/slaves#

view this post on Zulip Pierre-Marie Pédrot (Jun 17 2020 at 11:55):

what do?

view this post on Zulip Pierre-Marie Pédrot (Jun 17 2020 at 12:06):

ah, it ended up starting

view this post on Zulip Pierre-Marie Pédrot (Jun 17 2020 at 12:16):

gah, what am I supposed to do to check that the password I am entering is correct??

view this post on Zulip Pierre-Marie Pédrot (Jun 17 2020 at 12:16):

@Théo Zimmermann any idea?

view this post on Zulip Pierre-Marie Pédrot (Jun 17 2020 at 12:17):

Vicent's mail mentions a "user field" to test the input but there is nothing like that in sight

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

Maybe he meant "username" ?

view this post on Zulip Pierre-Marie Pédrot (Jun 17 2020 at 12:18):

I guess that there is some way to echo the keyboard

view this post on Zulip Pierre-Marie Pédrot (Jun 17 2020 at 12:18):

but I definitely can't find it

view this post on Zulip Pierre-Marie Pédrot (Jun 17 2020 at 12:18):

so I am blind-typing a password, which unsurprisingly doesn't work

view this post on Zulip Pierre-Marie Pédrot (Jun 17 2020 at 12:22):

WTF, writing is with the US keyboard layout worked

view this post on Zulip Pierre-Marie Pédrot (Jun 17 2020 at 12:28):

@Théo Zimmermann ahah, the password that Vicent sent us is not correct, it's only correct up to a back-and-forth through the VNC layouts

view this post on Zulip Pierre-Marie Pédrot (Jun 17 2020 at 12:29):

in a shell you have to transliterate the characters

view this post on Zulip Pierre-Marie Pédrot (Jun 17 2020 at 12:29):

wonderful

view this post on Zulip Pierre-Marie Pédrot (Jun 17 2020 at 12:30):

@Maxime Dénès that might explain your issues connecting to the VM...

view this post on Zulip Pierre-Marie Pédrot (Jun 17 2020 at 12:46):

I believe that the wiki page is outdated since it seems to be requiring the compilation to be performed on the macos machine

view this post on Zulip Pierre-Marie Pédrot (Jun 17 2020 at 12:59):

This is too mysterious for me, I'll add this to the call

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

OK thanks for trying. I won't be able to attend the call, so let me know what the conclusion is.

view this post on Zulip Anton Trunov (Jun 17 2020 at 19:08):

Just saw the notes from today's Coq Call: "need a MacOS specific team for testing packages and also, streamlining the dmg release process.". Since I'm a macOS user, I can try and help with that stuff if you'd like. (CC @Pierre-Marie Pédrot )

view this post on Zulip Maxime Dénès (Jun 18 2020 at 08:08):

That would be more than welcome!

view this post on Zulip Anton Trunov (Jun 18 2020 at 08:16):

@Maxime Dénès Folks, feel free to get in touch with me any time. I'll try to do my best.

view this post on Zulip Pierre-Marie Pédrot (Jun 18 2020 at 15:37):

@Théo Zimmermann it turns out that the wiki page on signing is fairly outdated

view this post on Zulip Pierre-Marie Pédrot (Jun 18 2020 at 15:37):

but with a heavy support from @Maxime Dénès we managed to sign the package

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

Oh! That's great news! Did you get a chance to update the wiki page as well?

view this post on Zulip Pierre-Marie Pédrot (Jun 18 2020 at 15:38):

a good chunk of the script can be reused

view this post on Zulip Pierre-Marie Pédrot (Jun 18 2020 at 15:38):

not yet, but I'll do this

view this post on Zulip Pierre-Marie Pédrot (Jun 18 2020 at 15:38):

we also need to version our signing infrastructure

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

thanks, that'd be useful

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

absolutely, yes!

view this post on Zulip Pierre-Marie Pédrot (Jun 18 2020 at 15:39):

it seems that we could do it directly on the CI actually

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

It'd been years that I've been dreaming of this.

view this post on Zulip Pierre-Marie Pédrot (Jun 18 2020 at 15:39):

apparently @Maxime Dénès wrote a PR to do that and the script on the VM is a variant of this

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

At some point I thought Maxime had managed to do it.

view this post on Zulip Pierre-Marie Pédrot (Jun 18 2020 at 15:40):

yes, it's unclear what happened, everything seems to be there but it's not used

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

So in any case, I guess you'll be uploading the installer and announcing the release very soon. I'll wait for your announcement before doing the one for 8.12+beta1.

view this post on Zulip Pierre-Marie Pédrot (Jun 18 2020 at 15:43):

I'll first need somebody to test the package because it seems it doesn't work on the MacOS on the VM

view this post on Zulip Pierre-Marie Pédrot (Jun 18 2020 at 15:43):

@Anton Trunov I am going to put the candidate package somewhere public and post a link here

view this post on Zulip Pierre-Marie Pédrot (Jun 18 2020 at 15:44):

so that you can test whether it's functional

view this post on Zulip Anton Trunov (Jun 18 2020 at 15:45):

@Pierre-Marie Pédrot Ok, great. Please ping me so I won't miss it

view this post on Zulip Matthieu Sozeau (Jun 18 2020 at 15:45):

I can give it a try too

view this post on Zulip Pierre-Marie Pédrot (Jun 18 2020 at 15:50):

@Théo Zimmermann as observed by Maxime, this PR contains all the necessary infrastructure for CI signing: https://github.com/coq/coq/pull/7501/files#diff-40388b094e5c40547292266117d120eaR44

view this post on Zulip Pierre-Marie Pédrot (Jun 18 2020 at 15:50):

somehow it disappeared from master

view this post on Zulip Pierre-Marie Pédrot (Jun 18 2020 at 15:52):

the script is now mostly empty, the line I linked contains arcane invocation for signing the package

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

Oh in fact this PR was only merged into v8.9 !?

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

Emilio commented:

Note that merging on master would maybe be more useful. Only thing is that the main instance won't enable the CI variable.

the day before it was merged

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

In fact, it was made v8.9-only because it was not managing to get approved to be merged into master...

view this post on Zulip Pierre-Marie Pédrot (Jun 18 2020 at 15:59):

@Anton Trunov @Matthieu Sozeau the package should be available at https://www.pédrot.fr/coq-8.11.2-installer-macos-signed.dmg

view this post on Zulip Anton Trunov (Jun 18 2020 at 16:20):

@Pierre-Marie Pédrot I tried a bunch of stuff that Théo suggested earlier. Everything worked. :tada: I'm on macOS 10.15.4 "Catalina"

view this post on Zulip Matthieu Sozeau (Jun 18 2020 at 17:49):

It installs and works fine, but I had to do the classic right-click + open as Apple didn't trust it

view this post on Zulip Pierre-Marie Pédrot (Jun 19 2020 at 09:54):

Thanks guys, I've uploaded the package and make the official release statement soon

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

Can we remove the extra branch on GitHub now? Would you like to cross-post the release announcement to Discourse?

view this post on Zulip Pierre-Marie Pédrot (Jun 19 2020 at 14:35):

Yep


Last updated: Jun 09 2023 at 08:01 UTC