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.
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.
I've fixed two typos but this looks otherwise good to me!
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.
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.
Shouldn't it be "generated proofs do work on"
right, since there are several tactics. Thanks, corrected.
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
but maybe we can count on someone to highlight it on Twitter or similar, rather than saying that in the README
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.
@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.
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?
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
hammertactic, which uses external ATPs
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"
@Karl Palmskog : thanks - changed. I also mentioned the executables provided by coq-prime generator (which is not so obvious).
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
Yes, @Michael Soegtrop said he did this because the installers are not yet available.
I am currently signing and testing the macOS installers. Then I will have a quick look at the Windows installers.
The signed macOS installers are uploaded. Should I remove the "pre release"? The Windows installers likely take until Monday or so.
in my opinion, no need to wait 4 days for Windows installers...
@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?
@Enrico Tassi : do you take care of the snap package?
I will remove the "pre-release" flag now.
Who wants to announce the release?
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
Do you want me to test this snap? https://github.com/coq/platform/actions/runs/1753713752
I'll take care of signing the windows stuff
@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
@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.
I think it was created. I'll test the snap right away.
@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.
bad news, the snap is not working: https://github.com/coq/platform/pull/206
we should really find the time to:
Last time, I did the announcement despite not being involved in the release management for 8.13 nor 8.14.
I think our process documents that now our RMs do not have to care about the announcements anymore.
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
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.
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)
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)
@Enrico Tassi : I already uploaded the Windows installers.
I think the announcement should come from the Coq core team - mostly to make clear that it is the official distribution of Coq.
Theo: do you want to do it again?
Sure, I can do it.
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)
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?
It was broken, see the recent PR https://github.com/coq/platform/pull/206, then I think nobody uploaded it :-/
@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.
Sorry, but I'm busy ,I would appreciate if you could take care of it
OK, I will do it. @Karl Palmskog : can you test it in the next days? I will trigger it today evening.
OK, I never tried Coq via snap before, but I can do it
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
@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?
The secret says
Updated on Jan 11, 2021 so maybe it had 1 year validity
I'll see how to get a new one
$ 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: firstname.lastname@example.org 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
I re-run CI, lets see if it uploads the file or not
After 2 retry, it is uploaded to the store
I did not promote it to stable though, should I?
Right now it is candidate on both the new 2022 track, and the
Well, yes. That's the first release for Coq 8.14, it's time to make it stable.
It is just one click, but I'll wait @Michael Soegtrop 's OK to go ahead
ah ok, I'll do
I just did not follow, so if 2022.01 is officially out, I'll click
It is officially out and has been for quite some time already ;-)
@Enrico Tassi : thanks!
@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?
I do, let me look at it
Fixed, but it seems to take some time to go live
thanks for the heads up
looks live to me now, thanks
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?
Sorry I am still somehow snap agnostic (need to change that). @Enrico Tassi ?
I think the text in the release note on github is just outdated, the snap was uploaded in the end.
Fine - I adjust the text then.
Last updated: Jan 30 2023 at 11:03 UTC