Skip to content

Howto Release

Jump to bottom Edit New page
Pierre Roux edited this page Oct 13, 2025 · 148 revisions

Howto Release

Current model:

  • only 1 released branch (master)
  • all releases are tags on master (no branch for, say, 1.8.x releases)
  • changing the model requires "mergers" to be informed (eventually to be discussed to the next meeting)
  • the current process should take about 2h if everything goes well.

Prerequisites

  • The person in charge of the release should have accounts on all services involved in the automatic verification of versions and pull requests:
    • github.com : math-comp/math-comp and math-comp/docker-mathcomp,
    • gitlab.inria.fr : (math-comp/math-comp (not-yet-created) and) math-comp/docker-mathcomp,
    • docker.com : mathcomp.
  • In addition, this person should be registered as a member of the math-comp core team on all these sites.

Steps

  • (optional but recommended) set up commit/tag GPG signing following instructions at https://help.github.com/en/articles/managing-commit-signature-verification

  • milestone faithful: look for issues and PR with no milestone that should belong to the current release, and give it the right milestone.

  • milestone full: check if all issues/PR in https://github.com/math-comp/math-comp/milestones are fixed/merged (eventually change the milestone of not-fixed/not-merged items)

  • send email to [email protected] telling your colleagues to please don't merge until further notice. Proposed text for this email:

    Subject: [IMPORTANT] Release of MathComp v${version} in progress

Dear all,

We are now starting the release process for mathcomp v${version}.
All pull requests targeted to this release have been merged. 
This message grabs the lock on the master branch.

**Please refrain from adding anything to the master branch until the lock is released.**

Best wishes,
-- 
${names of the release managers}

  • send the same contents to a new topic v${version} release in the stream #math-comp-devs

  • edit files CHANGELOG.md and CHANGELOG_UNRELEASED.md (the latter need to be generated with doc/changelog/generate-release-changelog.sh)

    • update CHANGELOG_UNRELEASED.md to regroup entries about the same file together (sort entries by some topological order of compilation).
    • move the contents of CHANGELOG_UNRELEASED.md at the head of CHANGELOG.md and update dates and releases
    • remove all files in doc/changelog/* that are now in CHANGELOG_UNRELEASED.md
    • remove CHANGELOG_UNRELEASED.md
    • update the links at the top of CHANGELOG.md to point-jump to the last releases
    • check that supported Coq versions are listed
    • check whether version numbers in INSTALL.md must be updated
    • compute and add the list of contributors with the following command (update the names of the tags, here we list contributors from 1.12.0 to now, fixme: apply mailmap also to coauthors):
    git log mathcomp-1.12.0.. --use-mailmap | egrep -i "(co-authored-by|author):.*" | cut -d : -f 2  | cut -d '<' -f 1 | sort -u | sed -e 's/ *$//' | tr -s '\n' ','

  • make sure the *.opam files at the root of the repository are accurate, in particular check the dependency in the versions of Coq.

  • close milestone (button Close in the list of milestones).

  • CI green

  • Publish the new documentation.

    • Start with setting the version name V="x_yy_z" (replace x_yy_z by the current release number in all the following)

    • Work in a fresh directory, named $FRESH_DIRECTORY in these notes, e.g.

      • FRESH_DIRECTORY=$(mktemp -d)
      • echo $FRESH_DIRECTORY

    • clone the math-comp web site (math-comp.github.io): git clone --depth 1 [email protected]:math-comp/math-comp.github.io.git $FRESH_DIRECTORY/math-comp.github.io

    • clone the math-comp repository git clone --depth 1 [email protected]:math-comp/math-comp.git $FRESH_DIRECTORY/math-comp

    • create a new branch cd $FRESH_DIRECTORY/math-comp.github.io && git checkout -b doc_$V

    • compile the doc. There are two ways, a quick one using nix and its cache and a slower one which does rebuild mathcomp on your computer.

    • update the symbolic link htmldoc to point to the last version of the documentation: cd $FRESH_DIRECTORY/math-comp.github.io && rm htmldoc && ln -s htmldoc_$V htmldoc

    • link the resulting doc in the file emacs $FRESH_DIRECTORY/math-comp.github.io/index.org by copy-pasting the line from a previous version and C-c C-l to edit the link

    • Run "emacs" index.org --batch -f org-html-export-to-html --kill (or within emacs type C-c C-e h h) to generate the index.html file

    • commit changes in math-comp.github.io/htmldoc with cd $FRESH_DIRECTORY/math-comp.github.io && git add index.org index.html htmldoc htmldoc_$V && git commit -m "htmldoc regenerated for release $V"

    • push the branch git push origin doc_$V

    • open a pull-request for branch doc_$V

Release

  • Go to github.com/math-comp/math-comp/releases/new in order to draft a new release
  • write in the Tag version text entry the version to be released prefixed with "mathcomp-", eg "mathcomp-1.8.0" and leave @ target "master"
  • title is "The Mathematical Components Library X.Y.Z"
  • In the description message list:
    • compatible Coq versions
    • main changes if any
    • convenience link to the CHANGELOG.md file, eg [CHANGELOG.md](https://github.com/math-comp/math-comp/blob/master/CHANGELOG.md)
  • if we release a beta, mark as a pre-release, otherwise as a release.
  • save the draft release
  • check it looks OK in https://github.com/math-comp/math-comp/releases
  • edit it one more and this time click "Publish the release"
  • Release the lock on math-comp/master by sending a mail to [email protected] 
    Subject: [IMPORTANT] Release of MathComp v${version} completed

Dear all,

The release has been tagged.
We are releasing the lock on math-comp master.

Best wishes,
-- 
${names of the release managers}
  • send the same contents to the topic v${version} release in the stream #math-comp-devs

Nix packages

To update nix packages do (only the first time):

  • On github, make a fork of https://github.com/NixOS/nixpkgs/
  • Clone git clone --depth=1 [email protected]:your_user_name/nixpkgs.git
  • Update remotes git remote add upstream https://github.com/NixOS/nixpkgs/

Then:

  • Create a branch for the pull request git fetch --depth=1 update upstream; git checkout -b update-mathcomp-$V upstream/master
  • Edit emacs pkgs/development/coq-modules/mathcomp/default.nix
    • In the release record a line like "1.14.0".sha256 = ""; (yes, the hash is empty)
    • In the defaultVersion record set { case = isGe "8.14"; out = "1.14.0"; }
  • Do a local build nix-build -A coqPackages_8_14.mathcomp
    • The build will fail with a message like 
      hash mismatch in fixed-output derivation '/nix/store/3rz47a815jf97k3fdixfjgm3ryz1llap-source':
wanted: sha256:0000000000000000000000000000000000000000000000000000
got:    sha256:07yamlp1c0g5nahkd2gpfhammcca74ga2s6qr7a3wm6y6j5pivk9
    • Update the sha256 in default.nix
    • Rerun the local build (shall not fail this time)
  • Push git push origin update-mathcomp-$V
  • Click on the link printed to open the pull request
    • add a comment FYI @vbgl @Zimmi48 @CohenCyril
    • if you have the rights add a comment saying @GrahamcOfBorg build coqPackages_8_14
  • test the PR on coq-nix-toolbox following instructions on https://github.com/coq-community/coq-nix-toolbox

Opam packages

  • Start with setting the version name VOP="x.yy.z"
  • in your math-comp git directory, run git pull --tags upstream to synchronize the information about the freshly made release
  • run bash etc/utils/packager ${VOP} from the root of the mathcomp repository that generates ./opam/released/
    • note that this tool takes the opam files from the release by default (e.g. in order to get the right versions of Coq at all times).
    • if the opam files were changed after the release, you can run bash etc/utils/packager with an extra argument (or use option --help). E.g. you can run bash etc/utils/packager ${VOP} master if the updated opam files are in your master branch.
  • make a "Fork" of https://github.com/rocq-prover/opam in your github account
  • cd $FRESH_DIRECTORY && git clone [email protected]:rocq-prover/opam.git && cd opam
  • git remote add ${USERNAME} [email protected]:${USERNAME}/opam.git
  • git checkout master && git pull origin master (if you use an old existing copy of the repository instead of the previous line)
  • git checkout -b mathcomp-${VOP}
  • cp -r ~/work/math-comp/opam/released/packages released/
  • git add released && git commit -m 'update mathcomp packages'
  • git push ${USERNAME} mathcomp-${VOP} (then follow the link printed by git in order to open the pull request)
  • in the pull request description, one can use ci-skip: coq-mathcomp-ssreflect.${VOP} coq-mathcomp-fingroup.${VOP} coq-mathcomp-algebra.1.19.0 coq-mathcomp-solvable.${VOP} coq-mathcomp-field.${VOP} to avoid having the CI compile each package multiple times (thanks Karl Palmskog for the trick, be careful to update all the version numbers, it won't work if the version numbers are not right first time)

Advertise the release

  • in your math-comp git directory, run git fetch --tags to synchronize the information about the freshly made release
  • write to the coq club and ssreflect mailing lists (currently [email protected] and [email protected] ) a message following this template
Subject: MathComp X.Y.Z released

We are proud to announce the immediate availability of the Mathematical Components library version X.Y.Z.
The webpage, and documentation, are available at https://math-comp.github.io/.

This release is compatible with Coq 8.Y1, 8.Y2 and X.Y
The main changes are  [... (if any) ...]
The contributors to this version are: ...
We also wish to thank all the reviewers of the various contributions.

See https://github.com/math-comp/math-comp/releases/tag/mathcomp-X.Y.Z to download or see the `CHANGELOG.md`.

Packages for opam, nix, and docker are in preparation.

Best regards,
-- 
The Mathematical Components team

as well as in the Zulip Coq and mathcomp channels and Coq's discourse (a mail to coq+announcements <[email protected]> would do).

Docker images

Work on this section should be done only after the pull-request for opam packages has been duly merged. The construction of docker images (see below) cannot happen before.

To prepare the configuration and automatically build the images:

    build:
      keywords:
        - '{matrix[coq]}'
  • Remove the - tag: 'latest-coq-{matrix[coq]}' lines from the previous release in this YAML file, provided the new release is a stable release, not a beta.
    • (As by convention with Docker tags, the latest keyword always denotes a stable release.)
  • Commit your changes by doing git commit -a -m 'New release'
  • Run git push -u origin mathcomp-1.8.0 (then follow the link printed by git in order to open the pull request).
  • Wait for the https://gitlab.inria.fr/math-comp/docker-mathcomp/-/pipelines to terminate.
    • Several linting/consistency-tests are performed by GitLab CI.
  • Review the computed list of tags from the images.yml spec by browsing the pipeline job debrief and opening the README artifact URL.
  • FTR, another standard way to retrieve the generated artifacts amounts to browse list of all pipelines, and click on the right-hand-side icon (see screenshot below) docker-keeper artifacts
    • NB: Rendering in your web browser might slightly differ
  • As soon as the new release package is available in opam-coq-archive, Merge the docker-mathcomp PR in master, which will generate a new pipeline with an additional (deploy) step to https://hub.docker.com/r/mathcomp/mathcomp
    • (Access to docker.com might be slow in general)
  • When the pipeline associated with the PR terminates:
    • click on the "notify / debrief" job (the last one of the pipeline)
      • to reach for the textual output of the run of the virtual machine
    • follow the steps to remove potential obsolete tags
      • (E.g., latest-coq-8.7 if compatibility with Coq 8.7 has been dropped by the new release.)
      • Concretely, this means: select the tags to be removed and choose the "remove" action using the webpage interface of docker.com.
    • upload the generated README.md to https://hub.docker.com/repository/docker/mathcomp/mathcomp/general
      • by clicking on Edit at the bottom of the docker.com webpage.
      • ⚠️ NB: this documentation step is important, otherwise end users may believe that the mathcomp release is not available on Docker Hub.
Add a custom footer

Clone this wiki locally