About to tag 2022.01.0 · Coq Platform devs & users

Stream: Coq Platform devs & users

Topic: About to tag 2022.01.0

Michael Soegtrop (Jan 26 2022 at 12:04):

I am about to tag 2022.01.0 - a PR with some final changes (mathcomp version), clean up (mostly removing local opam packages available upstream) and the version bump is running.

Unless someone brings forward a good reason for not to, I will tag today evening.

Michael Soegtrop (Jan 26 2022 at 19:05):

I just created the release (marked as pre release until the installers are there). @Théo Zimmermann @Enrico Tassi : I would appreciate if you could review the release text.

I will test the macOS and Windows installers and create the snap tomorrow. The Windows installers can be sent to signing then.

Théo Zimmermann (Jan 26 2022 at 19:20):

I've fixed two typos but this looks otherwise good to me!

Karl Palmskog (Jan 27 2022 at 07:03):

I think the following could be a bit clearer:

Notes on Coq Hammer: The proof generator part of Coq Hammer is available on macOS and Linux only. The Coq Hammer Tactic which plays back proofs does work on Windows, though. So you can use / check Coq Hammer proofs on Windows - you just can't create them on Windows.

CoqHammer tactic proofs (note absence of space between "Coq" and "Hammer") can actually be created manually on Windows, i.e., a Windows user can write tactics that use sauto and its variants. But a Windows user can't call the hammer tactic and have it spit out such proofs automatically. So my suggestion:

Notes on CoqHammer: The proof generation component of CoqHammer is available on macOS and Linux only. The CoqHammer tactics which reconstruct generated proofs do work on Windows, though. So you can check and manually write CoqHammer tactic proofs on Windows - you just can't create them automatically.

Karl Palmskog (Jan 27 2022 at 07:15):

I think there is a typo here (my emphasis):

From a Coq Platform point of view, the Coq 8.15.0 variant is a beta release, so it is called 8.15~beta1. A Coq Platform release with a final package collection for Coq 8.14 is expected end of February 2022.

Ali Caglayan (Jan 27 2022 at 07:28):

Shouldn't it be "generated proofs do work on"

Karl Palmskog (Jan 27 2022 at 07:30):

right, since there are several tactics. Thanks, corrected.

Karl Palmskog (Jan 27 2022 at 07:32):

also, I honestly think the automated installation of coq-hammer and ATPs like z3tptp and eprover on both Linux and macOS deserves more attention, this is currently the best we have towards push-button automation

Karl Palmskog (Jan 27 2022 at 07:33):

but maybe we can count on someone to highlight it on Twitter or similar, rather than saying that in the README

Michael Soegtrop (Jan 27 2022 at 08:32):

also, I honestly think the automated installation of coq-hammer and ATPs like z3tptp and eprover on both Linux and macOS deserves more attention

It was definitely a bit of work and the main reason for the delay (just when I was about to be finished, there came a PR to substantially change the z3 opam package I relied on). I don't have a "Major improvements" section as in the last release - maybe I should put in this there.

Michael Soegtrop (Jan 27 2022 at 08:52):

@Karl Palmskog : I fixed the 8.14 vs 8.15 typo and reworked the notes on CoqHammer (extended them a bit beyond your suggestion). As you suggested I also added back a "Major enhancements" section mentioning CoqHammer.

Michael Soegtrop (Jan 27 2022 at 08:57):

I also put CoqPrime Generator into the Major enhancements list. Do you think the package authors should be mentioned for packages highlighted in the major enhancements?

Karl Palmskog (Jan 27 2022 at 08:58):

looks good, only nitpick suggestion now is that:

An important newly added package is the CoqHammer tactic, which uses external ATPs

may be more precise as:

An important newly added package, coq-hammer, provides the hammer tactic, which uses external ATPs

Karl Palmskog (Jan 27 2022 at 09:00):

I think all authorship is anyway captured in the package definitions. Would be better to highlight specific efforts that helped the platform, e.g., "author X kindly reorganized the project to improve the X package for the platform"

Michael Soegtrop (Jan 27 2022 at 09:09):

@Karl Palmskog : thanks - changed. I also mentioned the executables provided by coq-prime generator (which is not so obvious).

Karl Palmskog (Jan 27 2022 at 09:38):

is the marking of the 2022.01.0 release as a pre-release a conscious choice? This means it doesn't show up on the Coq Platform GitHub landing page

Théo Zimmermann (Jan 27 2022 at 09:43):

Yes, @Michael Soegtrop said he did this because the installers are not yet available.

Michael Soegtrop (Jan 27 2022 at 10:20):

I am currently signing and testing the macOS installers. Then I will have a quick look at the Windows installers.

Michael Soegtrop (Jan 27 2022 at 10:47):

The signed macOS installers are uploaded. Should I remove the "pre release"? The Windows installers likely take until Monday or so.

Karl Palmskog (Jan 27 2022 at 10:54):

in my opinion, no need to wait 4 days for Windows installers...

Michael Soegtrop (Jan 27 2022 at 13:14):

@Gaëtan Gilbert @Théo Zimmermann @Enrico Tassi : I had a quick look at the Windows installers and they look fine (besides two benign issues in the installer - it shows ppxlib for selection because it is pinned and the uninstaller leaves one file for whatever reason). Can you please take the installers from (https://github.com/coq/platform/actions/runs/1752402976) and have them signed?

Michael Soegtrop (Jan 27 2022 at 13:14):

@Enrico Tassi : do you take care of the snap package?

Michael Soegtrop (Jan 27 2022 at 13:15):

I will remove the "pre-release" flag now.

Michael Soegtrop (Jan 27 2022 at 13:19):

Who wants to announce the release?

Karl Palmskog (Jan 27 2022 at 13:21):

I suggest just copying the old release on Discourse and replacing the relevant parts: https://coq.discourse.group/t/coq-platform-2021-09-0/1487

Enrico Tassi (Jan 27 2022 at 13:23):

Do you want me to test this snap? https://github.com/coq/platform/actions/runs/1753713752

Enrico Tassi (Jan 27 2022 at 13:23):

I'll take care of signing the windows stuff

Enrico Tassi (Jan 27 2022 at 13:29):

@Michael Soegtrop I'll put you in CC of the signing request, as usual, so that you will receive the link to download the signed binaries

Michael Soegtrop (Jan 27 2022 at 13:42):

@Enrico Tassi : yes, I would appreciate if you could test the snap file - I still didn't look into it. Is the new stream already created?
And yes, please put me on CC for the signing request.

Enrico Tassi (Jan 27 2022 at 13:42):

I think it was created. I'll test the snap right away.

Michael Soegtrop (Jan 27 2022 at 13:46):

@Karl Palmskog : the releases are usually announced by one of the involved release managers on coq-club and discourse. This would be @Guillaume Melquiond for 8.14 or @Gaëtan Gilbert for 8.15.

@Guillaume Melquiond : sorry that it took so long with the Coq Platform release for Coq 8.14.1 - I was really super busy.

Enrico Tassi (Jan 27 2022 at 13:49):

bad news, the snap is not working: https://github.com/coq/platform/pull/206
we should really find the time to:

clean up the "cleanup script"
run the smoke test on the snap

Théo Zimmermann (Jan 27 2022 at 14:43):

Last time, I did the announcement despite not being involved in the release management for 8.13 nor 8.14.

Théo Zimmermann (Jan 27 2022 at 14:43):

I think our process documents that now our RMs do not have to care about the announcements anymore.

Enrico Tassi (Jan 27 2022 at 15:10):

FTR the packages are signed (but I won't upload them since I don't have the time today). @Michael Soegtrop you can do it, or I will tomorrow

Karl Palmskog (Jan 27 2022 at 15:12):

yes, I think RMs are just doing Coq or GitHub stuff these days, they are not the ones announcing the proverbial party when platforms are released.

Karl Palmskog (Jan 27 2022 at 15:13):

my view is that either someone from the core team or the Platform team (or their intersection) should post the release announcement on Discourse (essentially just copying some parts of the Platform release notes along with some boilerplate)

Karl Palmskog (Jan 27 2022 at 15:15):

anyway, we were hoping to discuss stuff like this in the next Coq call (who is doing what in all the Coq+ecosystem release processes)

Michael Soegtrop (Jan 27 2022 at 16:39):

@Enrico Tassi : I already uploaded the Windows installers.

Michael Soegtrop (Jan 27 2022 at 16:40):

I think the announcement should come from the Coq core team - mostly to make clear that it is the official distribution of Coq.

Michael Soegtrop (Jan 27 2022 at 16:43):

Theo: do you want to do it again?

Théo Zimmermann (Jan 27 2022 at 17:59):

Sure, I can do it.

Théo Zimmermann (Jan 28 2022 at 17:31):

Just did a tweet announce as well: https://twitter.com/CoqLang/status/1487115940185714693

Just released: Coq Platform 2022.01.0 which includes Coq 8.14.1 as a main version and Coq 8.15.0 as a preview! Now you can run the "hammer" tactic of CoqHammer without hassle :tada: Check out the announcement on Discourse: https://coq.discourse.group/t/coq-platform-2022-01-0/1545

- The Coq proof assistant (@CoqLang)

Karl Palmskog (Feb 11 2022 at 12:08):

The snap for 8.14.1/2022.01 is not up yet: https://snapcraft.io/coq-prover

Did I miss the discussion on why this got stuck? Can anyone else here help with the process?

Enrico Tassi (Feb 11 2022 at 12:53):

It was broken, see the recent PR https://github.com/coq/platform/pull/206, then I think nobody uploaded it :-/

Michael Soegtrop (Feb 11 2022 at 13:56):

@Enrico Tassi : do you do it or shall I do it? My assumption was that after the PR you do it and give the result a final check. I still have difficulties testing the snap stuff.

Enrico Tassi (Feb 11 2022 at 14:03):

Sorry, but I'm busy ,I would appreciate if you could take care of it

Michael Soegtrop (Feb 11 2022 at 16:38):

OK, I will do it. @Karl Palmskog : can you test it in the next days? I will trigger it today evening.

Karl Palmskog (Feb 11 2022 at 16:39):

OK, I never tried Coq via snap before, but I can do it

Enrico Tassi (Feb 11 2022 at 16:48):

Note that I did test it locally. It works but coqc spits a warning about inaccessible paths (from the snap). See: https://coq.zulipchat.com/#narrow/stream/237656-Coq-devs.20.26.20plugin.20devs/topic/coqc.20scanning.20PATH

Michael Soegtrop (Feb 15 2022 at 09:37):

@Enrico Tassi : somehow the snap store upload does not work any more. See e.g. (https://github.com/coq/platform/runs/5161974186?check_suite_focus=true). Can you have a look?

Enrico Tassi (Feb 15 2022 at 09:43):

The secret says Updated on Jan 11, 2021 so maybe it had 1 year validity
I'll see how to get a new one

Enrico Tassi (Feb 15 2022 at 10:36):

$ snapcraft export-login /tmp/login
Enter your Ubuntu One e-mail address and password.
If you do not have an Ubuntu One account, you can create one at https://snapcraft.io/account
Email: coq-team@inria.fr
Password:
...
expires:     2023-02-15T09:47:55.881713
...
This exported login is not encrypted. Do not commit it to version control!

The I did put this file as the secret here: https://github.com/coq/platform/settings/secrets/actions

Enrico Tassi (Feb 15 2022 at 10:36):

I re-run CI, lets see if it uploads the file or not

Enrico Tassi (Feb 15 2022 at 21:02):

After 2 retry, it is uploaded to the store

Enrico Tassi (Feb 15 2022 at 21:03):

I did not promote it to stable though, should I?

Enrico Tassi (Feb 15 2022 at 21:04):

Right now it is candidate on both the new 2022 track, and the latest one

Théo Zimmermann (Feb 15 2022 at 21:04):

Well, yes. That's the first release for Coq 8.14, it's time to make it stable.

Enrico Tassi (Feb 15 2022 at 21:04):

It is just one click, but I'll wait @Michael Soegtrop 's OK to go ahead

Enrico Tassi (Feb 15 2022 at 21:04):

ah ok, I'll do

Enrico Tassi (Feb 15 2022 at 21:05):

I just did not follow, so if 2022.01 is officially out, I'll click

Enrico Tassi (Feb 15 2022 at 21:06):

done

Théo Zimmermann (Feb 15 2022 at 21:17):

It is officially out and has been for quite some time already ;-)

Michael Soegtrop (Feb 16 2022 at 10:13):

@Enrico Tassi : thanks!

Karl Palmskog (Feb 18 2022 at 13:38):

@Enrico Tassi even though the snap for 2022.01 is now out on https://snapcraft.io/coq-prover, the description is still for the old release (it mentions Coq 8.13.2 and links to the README for 2021.09). Do you have privileges to change this?