Release 8.12

[ejgallego]

Release process

As soon as 8.11 has branched off master and 8.12 RM have been nominated do:

• Create the X.X+beta1 milestone if it did not already exist.
• Put the corresponding alpha tag using git tag -s.
  The VX.X+alpha tag marks the first commit to be in master and not in the
  branch of the previous version.
• Create a new issue to track the release process [copy-paste the present checklist]
• Version updating PR ([release] Update files for 8.12 release per release process. #11158):
  • Change the version name to the next major version and the magic numbers (see #7008).
  • Update the compatibility infrastructure see below for details
• Update the release plan wiki page
• Decide the release calendar with the team (freeze date, beta date, final
  release date) and put this information in the milestone (using the
  description and due date fields), and in the release wiki page

About one month before the beta

• Create the X.X.0 milestone and set its due date.

• Send an announcement of the upcoming freeze on Coqdev / Discourse and ask people to
  remove from the beta milestone what they already know won't be ready on time
  (possibly postponing to the X.X.0 milestone for minor bug fixes,
  infrastructure and documentation updates).

• Determine which issues should / must be fixed before the beta, add them
  to the beta milestone, possibly with a
  "priority: blocker"
  label. Make sure that all these issues are assigned (and that the assignee
  provides an ETA).

• Ping the development coordinator (@mattam82) to get him started on
  the update to the Credits chapter of the reference manual.
  See also #7058.

  The command that was used in the previous versions to get the list
  of contributors for this version is git shortlog -s -n VX.X+alpha..master | cut -f2 | sort -k 2. Note that the ordering is
  approximative as it will misplace people with middle names. It is
  also probably not correctly handling Co-authored-by info that we
  have been using more lately, so should probably be updated to
  account for this.

On the date of the feature freeze

• Create the new version branch vX.X (using this name will ensure that
  the branch will be automatically protected).

• Pin the versions of libraries and plugins in
  dev/ci/ci-basic-overlays.sh to use commit hashes or tag (or, if it
  exists, a branch dedicated to compatibility with the corresponding
  Coq branch).

• Remove all remaining unmerged feature PRs from the beta milestone.

• Start a new project to track PR backporting. The project should
  have a "Request X.X+beta1 inclusion" column for the PRs that were
  merged in master that are to be considered for backporting, and a
  "Shipped in X.X+beta1" columns to put what was backported. A message
  to @coqbot in the milestone description tells it to
  automatically add merged PRs to the "Request ... inclusion" column
  and backported PRs to the "Shipped in ..." column. See previous
  milestones for examples. When moving to the next milestone
  (e.g. X.X.0), you can clear and remove the "Request X.X+beta1
  inclusion" column and create new "Request X.X.0 inclusion" and
  "Shipped in X.X.0" columns.

  The release manager is the person responsible for merging PRs that
  target the version branch and backporting appropriate PRs that are
  merged into master.

• Delay non-blocking issues to the appropriate milestone and ensure
  blocking issues are solved. If required to solve some blocking issues,
  it is possible to revert some feature PRs in the version branch only.

Before the beta release date

• Ensure the Credits chapter has been updated.
• Ensure that an appropriate version of the plugins we will distribute with
  Coq has been tagged.
• Have some people test the recently auto-generated Windows and MacOS
  packages.
• In a PR:
  • Change the version name from alpha to beta1 (see
    #7009).
  • We generally do not update the magic numbers at this point.
  • Set is_a_released_version to true in configure.ml.
• Put the VX.X+beta1 tag using git tag -s.
• Check using git push --tags --dry-run that you are not
  pushing anything else than the new tag. If needed, remove spurious
  tags with git tag -d. When this is OK, proceed with git push --tags.
• Set is_a_released_version to false in configure.ml
  (if you forget about it, you'll be reminded whenever you try to
  backport a PR with a changelog entry).

These steps are the same for all releases (beta, final, patch-level)

• Send an e-mail on Coqdev announcing that the tag has been put so that
  package managers can start preparing package updates (including a
  coq-bignums compatible version).
• Ping @erikmd to update the Docker images in coqorg/coq
  (requires coq-bignums in extra-dev for a beta / in released
  for a final release).
• Draft a release on GitHub.
• Get @maximedenes to sign the Windows and MacOS packages and
  upload them on GitHub.
• Prepare a page of news on the website with the link to the GitHub release
  (see coq/www#63).
• Merge the website update, publish the release
  and send announcement e-mails.
• Ping @Zimmi48 to publish a new version on Zenodo.
  TODO: automate this.
• Close the milestone

At the final release time

• In a PR:
  • Change the version name from X.X.0 and the magic numbers (see
    #7271).
  • Set is_a_released_version to true in configure.ml.
• Put the VX.X.0 tag.
• Check using git push --tags --dry-run that you are not
  pushing anything else than the new tag. If needed, remove spurious
  tags with git tag -d. When this is OK, proceed with git push --tags.
• Set is_a_released_version to false in configure.ml
  (if you forget about it, you'll be reminded whenever you try to
  backport a PR with a changelog entry).

Repeat the generic process documented above for all releases.

• Switch the default version of the reference manual on the website.

At the patch-level release time

We generally do not update the magic numbers at this point (see
2881a18).

Compatibility Infrastructure Update

Additionally, in the same commit, update the compatibility
infrastructure, which consists of invoking
dev/tools/update-compat.py with the
--master flag.

Note that the update-compat.py script must be run twice: once
immediately after branching with the --master flag (which sets
up Coq to support four -compat flag arguments), in the same
commit as the one that updates coq_version in
configure.ml, and once again later on before
the next branch point with the --release flag (see next section).

[ejgallego]

@Zimmi48 I tweaked the start of the issue a bit to make it more compact; OMMV, changes are small tho; I will wait to tweak this more until we meet.

[ejgallego]

Some topics for 8.12:

• progress on dune as a default build system
• removal of omega
• documentation?

[Zimmi48]

FTR, I am currently preparing the draft PR with the release notes.

[ejgallego]

I will take care of the PR with the beta version bump. Two main points seem:

• Ensure the Credits chapter has been updated.
• Ensure that an appropriate version of the plugins we will distribute with Coq has been tagged.

I understand @mattam82 is already working on the first item, how's the status on the second point tho? Seems like quite a complex process?

[Zimmi48]

I'll look into it possibly with help from @MSoegtropIMC.

[MSoegtropIMC]

I am about to finish my reals PR and then will pick up the platform work. Do you have a timeline?

[Zimmi48]

Yes, and it is short (we're supposed to release 8.12+beta1 early next week). I'll work on this today.

[MSoegtropIMC]

I see - unfortunately I have little time until the weekend, but I have time to review it and help in case you need it. You might want to take the file from the 8.11 release branch - it might be closer to what you finally need and contains in comments the reasoning for the picks I did then which is likely very similar for 8.12.

[Zimmi48]

Thanks, I'm using it as a reference, but virtually all tested projects have received compatibility fixes in 8.12, so they will all have to be updated.

[Zimmi48]

@erikmd Would you mind preparing a Docker image for Coq 8.12+beta1 (available on opam).

[erikmd]

Hi @Zimmi48, thanks for the ping! currently coqorg/coq:8.12 = coqorg/coq:8.12-alpha and I recently made some progress for coq-community/docker-coq#4 but this large refactoring is still on-going − so yes I'm going to bump that image from now on with the current build system: it should be ready in less than 2 hours, I'll let you know in this issue.

[erikmd]

Regarding bignums, the compatible version is already in extra-dev, but for 8.12.0 I'll need to release coq-bignums.8.12.0 (say, from the last commit of the v8.12 branch of bignums) as well. This could be done from now on, but I guess it's better to wait for the opam package of coq.8.12.0 do to that, isn't it?

[Zimmi48]

Yes, it sounds better to wait in case there's a last minute API change.

[erikmd]

I'll let you know in this issue.

Done:

$ docker pull coqorg/coq:8.12 && docker run --rm -it coqorg/coq:8.12 bash -c \
    "opam switch && opam list"
…
#   switch          compiler                       description
->  4.05.0          ocaml-base-compiler.4.05.0     4.05.0
    4.07.1+flambda  ocaml-variants.4.07.1+flambda  4.07.1+flambda
# Packages matching: installed
# Name                   # Installed # Synopsis
base-bigarray            base
base-num                 base        Num library distributed with the OCaml compiler
base-threads             base
base-unix                base
conf-findutils           1           Virtual package relying on findutils
conf-m4                  1           Virtual package relying on m4
coq                      8.12+beta1  pinned to version 8.12+beta1
coq-bignums              8.12.dev    Bignums, the Coq library of arbitrary large numbers
dune                     2.5.1       pinned to version 2.5.1
num                      0           pinned to version 0
ocaml                    4.05.0      The OCaml compiler (virtual package)
ocaml-base-compiler      4.05.0      Official 4.05.0 release
ocaml-config             1           OCaml Switch Configuration
ocaml-secondary-compiler 4.08.1-1    OCaml 4.08.1 Secondary Switch Compiler
ocamlfind                1.8.1       pinned to version 1.8.1
ocamlfind-secondary      1.8.1       ocamlfind support for ocaml-secondary-compiler
opam-depext              1.1.3       Query and install external dependencies of OPAM packages

[Zimmi48]

Release announcements (for 8.12.1) will be done soon. This will be the last 8.12 release.

[ejgallego]

Great work, thanks a lot @Zimmi48