HOWTORELEASE

How to release

Publish a release

1. Check that the milestone is complete

2. Check the contents of unstable.v

3. Announce on Zulip

• "We are preparing the X.Y.Z version of mathcomp-analysis, please do not merge into master until further notice."

4. Edit the changelogs

• git checkout -b changelog_X_Y_Z
• Commit message: "changelog for version X.Y.Z"

5. Update INSTALL.md if necessary (version numbers, dependencies, etc.)

6. Check the opam files if necessary (tags, authors, description, etc.)

• NB: until version 0.5.4, the unique opam file used to be generated using https://github.com/coq-community/templates (and modifications were done in meta.yml)

7. Generate the HTML documentation and PR to the MathComp website

• update the link to the last version of the doc in README.md

8. Close the milestone

9. Draft the release

   • github.com/math-comp/analysis/releases/new
   • Tag: X.Y.Z
   • Title: "MathComp Analysis X.Y.Z"
   • Summary:
     • "Compatible with MathComp X.YZ, ..."
     • main change (extracted from the changelog?)
     • changelog

10. Just after the release, download the github assets (.zip and .tar.gz files) and add them back manually as assets to the release. (This is to freeze the archives for use with opam, because assets generated by github are not guaranteed to have a stable hash.)

11. Announce to Zulip:

• "We have released the X.Y.Z version of mathcomp-analysis, it is now ok to merge into master. Changelog: https://github.com/math-comp/analysis/blob/master/CHANGELOG.md "

Publish the packages

1. Submit a new opam package to https://github.com/coq/opam-coq-archive

• you can generate the files with etc/packager X.Y.Z
• all package go to opam/released
• Karl Palmskog (when releasing MathComp-Analysis 1.3.1): to make opam archive CI go faster, you can put this in the PR message:

  ci-skip: coq-mathcomp-classical coq-mathcomp-reals coq-mathcomp-analysis coq-mathcomp-reals-stdlib
  

  basically, if two packages are added, they are both tested separately, even if they depend on each other, which makes everything take longer. The ci-skip thing can be used for dependencies of other packages, but it must use exactly the added package name

2. Add the new version on nixpkgs, this can be done following the procedure at https://github.com/coq-community/coq-nix-toolbox?tab=readme-ov-file#testing-coqpackages-updates-in-nixpkgs taking for instance example on https://github.com/NixOS/nixpkgs/pull/318007/files

3. Annouce on Zulip:

• "The X.Y.Z version of mathcomp-analysis is available as Opam (in U) and Nix packages." where U is among
  • https://rocq-prover.org/opam/released
  • https://rocq-prover.org/opam/extra-dev