Stream: Coq Platform devs & users

Topic: About to tag 2022.01.0


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

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

view this post on Zulip Théo Zimmermann (Jan 26 2022 at 19:20):

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

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

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

view this post on Zulip Ali Caglayan (Jan 27 2022 at 07:28):

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

view this post on Zulip Karl Palmskog (Jan 27 2022 at 07:30):

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

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

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

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

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

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

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

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

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

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

view this post on Zulip Théo Zimmermann (Jan 27 2022 at 09:43):

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

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

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

view this post on Zulip Karl Palmskog (Jan 27 2022 at 10:54):

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

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

view this post on Zulip Michael Soegtrop (Jan 27 2022 at 13:14):

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

view this post on Zulip Michael Soegtrop (Jan 27 2022 at 13:15):

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

view this post on Zulip Michael Soegtrop (Jan 27 2022 at 13:19):

Who wants to announce the release?

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

view this post on Zulip Enrico Tassi (Jan 27 2022 at 13:23):

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

view this post on Zulip Enrico Tassi (Jan 27 2022 at 13:23):

I'll take care of signing the windows stuff

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

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

view this post on Zulip Enrico Tassi (Jan 27 2022 at 13:42):

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

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

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

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

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

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

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

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

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

view this post on Zulip Michael Soegtrop (Jan 27 2022 at 16:39):

@Enrico Tassi : I already uploaded the Windows installers.

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

view this post on Zulip Michael Soegtrop (Jan 27 2022 at 16:43):

Theo: do you want to do it again?

view this post on Zulip Théo Zimmermann (Jan 27 2022 at 17:59):

Sure, I can do it.

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

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

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

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

view this post on Zulip Enrico Tassi (Feb 11 2022 at 14:03):

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

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

view this post on Zulip Karl Palmskog (Feb 11 2022 at 16:39):

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

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

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

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

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

view this post on Zulip Enrico Tassi (Feb 15 2022 at 10:36):

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

view this post on Zulip Enrico Tassi (Feb 15 2022 at 21:02):

After 2 retry, it is uploaded to the store

view this post on Zulip Enrico Tassi (Feb 15 2022 at 21:03):

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

view this post on Zulip Enrico Tassi (Feb 15 2022 at 21:04):

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

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

view this post on Zulip Enrico Tassi (Feb 15 2022 at 21:04):

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

view this post on Zulip Enrico Tassi (Feb 15 2022 at 21:04):

ah ok, I'll do

view this post on Zulip Enrico Tassi (Feb 15 2022 at 21:05):

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

view this post on Zulip Enrico Tassi (Feb 15 2022 at 21:06):

done

view this post on Zulip Théo Zimmermann (Feb 15 2022 at 21:17):

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

view this post on Zulip Michael Soegtrop (Feb 16 2022 at 10:13):

@Enrico Tassi : thanks!

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

view this post on Zulip Enrico Tassi (Feb 18 2022 at 13:39):

I do, let me look at it

view this post on Zulip Enrico Tassi (Feb 18 2022 at 13:41):

Fixed, but it seems to take some time to go live
thanks for the heads up

view this post on Zulip Karl Palmskog (Feb 18 2022 at 13:44):

looks live to me now, thanks

view this post on Zulip Karl Palmskog (Mar 09 2022 at 17:56):

the release notes for 2022.01 still say this:

The Snap installer is still in production / signing and will be uploaded as soon as it is available (a few days).

Should this maybe be updated/removed now that the Snap is out?

view this post on Zulip Michael Soegtrop (Mar 09 2022 at 19:09):

Sorry I am still somehow snap agnostic (need to change that). @Enrico Tassi ?

view this post on Zulip Enrico Tassi (Mar 09 2022 at 19:10):

I think the text in the release note on github is just outdated, the snap was uploaded in the end.

view this post on Zulip Enrico Tassi (Mar 09 2022 at 19:11):

here: https://github.com/coq/platform/releases/tag/2022.01.0

view this post on Zulip Michael Soegtrop (Mar 10 2022 at 07:01):

Fine - I adjust the text then.


Last updated: Jan 30 2023 at 11:03 UTC