Please create a tag for upcoming release of Coq 8.13

[gares]

The Coq team is planning to release Coq 8.13-beta1 on December 7, 2020
and Coq 8.13.0 on January 7, 2020.

Your project is currently scheduled for being bundled in the Windows installer.

We are currently testing commit aafdd43
on branch https://github.com/coq/bignums/tree/master
but we would like to ship a released version instead (a tag in git's slang).

Could you please tag that commit, or communicate us any other tag
that works with the Coq branch v8.13 at the latest 15 days before the
date of the final release?

Thanks!
CC: coq/coq#12334

[erikmd]

Hi @gares, I propose to create a branch v8.13 starting from master soon, after adding the corresponding CI configuration for Coq 8.13. However this will need the coqorg/coq:8.13 image (which I also have to prepare, hopefully this WE!)
Do you also need a tag of coq-bignums.8.13.0 for Coq 8.13-beta1, or just for Coq 8.13.0?
as IIRC, for previous bignums releases, we had just added a coq-bignums.8.12.dev package in https://github.com/coq/opam-coq-archive/tree/master/extra-dev/packages/coq-bignums for the Coq beta.

[erikmd]

BTW could you recall in which file you have specified that the coq beta is tested w.r.t. bignum aafdd43 ?

[gares]

I've just bumped the pin, see the last commit here:
coq/coq#13489
which compiled by the way.

You can make a branch, but I need something that does not move.

[erikmd]

OK thanks @gares!

I need something that does not move.

that's a very good point indeed.

and if you think a tag is useful, let's say I'll push a tag and release coq-bignums.8.13+beta1 in extra-dev this WE.

[gares]

It's up to you. If you say nothing I'll pick a non tagged commit for the beta, not the end of the world.
For the final, I'd really like a tagged version, so if you don't tag I will.
Please write here if you tag so that I get notified.

[erikmd]

Hi @gares

Please write here if you tag so that I get notified.

Done: https://github.com/coq/bignums/releases/tag/V8.13+beta1

cd bignums
$ git rev-parse V8.13+beta1
b524d21831ce9fb5ba3177bdc86e77c2c8647870

Will submit an extra-dev release in opam-coq-archive as well.

[erikmd]

Hi again @gares ,

just FYI I've updated the CI config for the v8.13 branch:

• Adding the coqorg/coq:8.13 image in the CI config
• Fixing the .opam file that was incorrectly requiring "coq" {= "dev"} beforehand (which was not "too serious" given the reference .opam file for end users is that of opam-coq-archive, but it was an issue anyway as it prevented having a working CI test for v8.13)

Anyway, I think it is unneeded for you to bump the SHA1 of bignums in Coq's CI config now as it is exactly the same OCaml and Coq code.

Anyway, I'll be able to tag coq-bignums.8.13.0 with the pin of this branch v8.13 048faca later on for the coq.8.13.0 release.

Hence a question in advance:

would you want that we do this coq-bignums.8.13.0 tag after the coq.8.13.0 release (which might make sense as bignums depends on coq), or a while beforehand? (as you have to hardcode bignums' SHA1-or-tag in advance in coq's CI config IIUC)

[gares]

I think you should tag before the 8.13.0 release. I'll refrain from merging PR that break the API, only critical fixes and doc updates.
For this release cycle, the release of Coq and the platforms are not 100% decorrelated.
Maybe next time we will make the meaning of the beta tag more formal (eg, name it release candidate) so that it is clear others can safely base on top of it.

[erikmd]

Hi @gares, OK thanks for your reply! actually if I tag the commit I proposed (048faca) as "coq-bignums.8.13.0", the only difference between coq-bignums.8.13+beta1 and coq-bignums.8.13.0 will be the .opam file dependencies constraints (which are fully correct now, and tested by the CI), so I guess this will be OK given your message…
In which case I propose to do this tag (coq-bignums.8.13.0) just in a few days, e.g. in the end of this week − (or please suggest another date if need be)

[erikmd]

Re-bonsoir @gares!
FYI unless you object, I'll do this "coq-bignums.8.13.0" tag this WE.

[gares]

OK

[erikmd]

done, so closing this issue.