Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Release 8.13 #12334

Closed
39 tasks done
gares opened this issue May 15, 2020 · 3 comments
Closed
39 tasks done

Release 8.13 #12334

gares opened this issue May 15, 2020 · 3 comments
Assignees

Comments

@gares
Copy link
Member

gares commented May 15, 2020

Release process

As soon as the previous version branched off master

In principle, these steps should be undertaken by the RM of the next
release. Unfortunately, we have not yet been able to nominate RMs
early enough in the process for this person to be known at that point
in time.

  • Create a new issue to track the release process where you can copy-paste
    the present checklist (from dev/doc/release-process.md)

  • Change the version name to the next major version and the magic
    numbers (see #7008).

    Done in Update to 8.13. #12346

    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).

  • 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 the X.X+beta1 milestone if it did not already exist.

  • 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).

    • freeze: 16 November
    • beta: 7 December
    • final: 7 January

Anytime after the previous version is branched off master

  • Update the compatibility infrastructure to the next release,
    which consists of invoking
    dev/tools/update-compat.py with the
    --release flag; this sets up Coq to support three -compat flag
    arguments. To ensure that CI passes, you will have to decide what
    to do about all test-suite files which mention -compat U.U or
    Coq.Comapt.CoqUU (which is no longer valid, since we only keep
    compatibility against the two previous versions on releases), and
    you may have to prepare overlays for projects using the
    compatibility flags.

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 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). You can use the dev/tools/pin-ci.sh script to do this
    semi-automatically.

  • 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.

  • Add a new link to the 'versions' list of the refman (in
    html_context in doc/sphinx/conf.py).

Before the beta release date

  • Ensure the Credits chapter has been updated.
  • Prepare the release notes (see e.g.,
    #10833): in a PR against the master
    branch, move the contents from all files of doc/changelog/ that appear in
    the release branch into the manual doc/sphinx/changes.rst. Merge that PR
    into the master branch and backport it to the version branch.
  • 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).
  • When opening the corresponding PR for coq in the opam repository (coq/opam-coq-archive or ocaml/opam-repository),
    the package managers can Cc @erikmd to request that he prepare the necessary configuration for the Docker release in coqorg/coq
    (namely, he'll need to make sure a coq-bignums opam package is available in extra-dev, respectively released, so the Docker image gathering coq and coq-bignums can be built).
  • Draft a release on GitHub.
  • Sign the Windows and MacOS packages and upload them on GitHub.
    • The Windows packages must be signed by the Inria IT security service. They
      should be sent as a link to the binary together with its SHA256 hash in a
      signed e-mail, via our local contact (currently @maximedenes).
    • The MacOS packages should be signed by our own certificate, by sending them
      to @maximedenes. A detailed step-by-step guide can be found on the wiki.
  • Prepare a page of news on the website with the link to the GitHub release
    (see coq/www#63).
  • Upload the new version of the reference manual to the website.
    TODO: setup some continuous deployment for this.
  • Merge the website update, publish the release
    and send announcement e-mails.
  • Close the milestone

At the final release time

  • Prepare the release notes (see above)
  • 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.

Ping @Zimmi48 to:

  • Switch the default version of the reference manual on the website.
  • Publish a new version on Zenodo.

At the patch-level release time

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

@gares
Copy link
Member Author

gares commented Nov 4, 2020

Bench between V8.13+alpha and v8.13, more precisely
f123874..2ac7dfc

┌────────────────────────┬──────────────────────────┬──────────────────────────────────────────────┬──────────────────────────────────────────────┬────────────────────────────────┬───────────────────┐
│                        │      user time [s]       │                  CPU cycles                  │               CPU instructions               │     max resident mem [KB]      │    mem faults     │
│                        │                          │                                              │                                              │                                │                   │
│           package_name │     NEW     OLD  PDIFF   │               NEW               OLD  PDIFF   │               NEW               OLD  PDIFF   │        NEW        OLD  PDIFF   │  NEW  OLD PDIFF   │
├────────────────────────┼──────────────────────────┼──────────────────────────────────────────────┼──────────────────────────────────────────────┼────────────────────────────────┼───────────────────┤
│        coq-lambda-rust │ 1250.40 1564.92 -20.10 % │     3479982198381     4355430338129 -20.10 % │     4985674473842     6252607643619 -20.26 % │    1097596    1357908 -19.17 % │    0    0  +nan % │
├────────────────────────┼──────────────────────────┼──────────────────────────────────────────────┼──────────────────────────────────────────────┼────────────────────────────────┼───────────────────┤
│  coq-engine-bench-lite │  367.72  425.88 -13.66 % │     1032887564196     1195931458280 -13.63 % │     1746544663325     2080627055570 -16.06 % │    3978972    3523396 +12.93 % │    0    0  +nan % │
├────────────────────────┼──────────────────────────┼──────────────────────────────────────────────┼──────────────────────────────────────────────┼────────────────────────────────┼───────────────────┤
│ coq-mathcomp-ssreflect │   51.00   56.51  -9.75 % │      139872225473      154025750916  -9.19 % │      177937783902      199304689880 -10.72 % │     511964     588652 -13.03 % │    0    0  +nan % │
├────────────────────────┼──────────────────────────┼──────────────────────────────────────────────┼──────────────────────────────────────────────┼────────────────────────────────┼───────────────────┤
│              coq-flocq │  156.60  172.90  -9.43 % │      435320834868      479489848887  -9.21 % │      541745681057      612056186803 -11.49 % │     820536     902788  -9.11 % │    0    0  +nan % │
├────────────────────────┼──────────────────────────┼──────────────────────────────────────────────┼──────────────────────────────────────────────┼────────────────────────────────┼───────────────────┤
│ coq-mathcomp-odd-order │ 1055.29 1152.72  -8.45 % │     2939998054386     3211037105938  -8.44 % │     4692276047345     5149936245586  -8.89 % │     975624    1390844 -29.85 % │    0    0  +nan % │
├────────────────────────┼──────────────────────────┼──────────────────────────────────────────────┼──────────────────────────────────────────────┼────────────────────────────────┼───────────────────┤
│         coq-coquelicot │   67.88   73.47  -7.61 % │      186058316916      201537467344  -7.68 % │      236869115120      261681965574  -9.48 % │     566544     683468 -17.11 % │    0    0  +nan % │
├────────────────────────┼──────────────────────────┼──────────────────────────────────────────────┼──────────────────────────────────────────────┼────────────────────────────────┼───────────────────┤
│           coq-compcert │  639.81  689.19  -7.16 % │     1782780678598     1920656192629  -7.18 % │     2478360745818     2672932695172  -7.28 % │    1046812    1064688  -1.68 % │    0    0  +nan % │
├────────────────────────┼──────────────────────────┼──────────────────────────────────────────────┼──────────────────────────────────────────────┼────────────────────────────────┼───────────────────┤
│                    coq │  520.09  557.56  -6.72 % │     1458925278480     1560193194930  -6.49 % │     1960525127854     2108582860507  -7.02 % │     562064     602852  -6.77 % │    0    0  +nan % │
├────────────────────────┼──────────────────────────┼──────────────────────────────────────────────┼──────────────────────────────────────────────┼────────────────────────────────┼───────────────────┤
│  coq-mathcomp-fingroup │   47.63   50.54  -5.76 % │      131603622979      139621764475  -5.74 % │      181484063446      192628529759  -5.79 % │     481820     558004 -13.65 % │    0    0  +nan % │
├────────────────────────┼──────────────────────────┼──────────────────────────────────────────────┼──────────────────────────────────────────────┼────────────────────────────────┼───────────────────┤
│             coq-geocoq │ 1449.28 1529.41  -5.24 % │     4036145203582     4262167019928  -5.30 % │     6140237618413     6458271098475  -4.92 % │    1018764    1369012 -25.58 % │    0    0  +nan % │
├────────────────────────┼──────────────────────────┼──────────────────────────────────────────────┼──────────────────────────────────────────────┼────────────────────────────────┼───────────────────┤
│   coq-mathcomp-algebra │  138.00  145.52  -5.17 % │      383287718175      405137565088  -5.39 % │      495311070363      527072386673  -6.03 % │     546300     629460 -13.21 % │    0    0  +nan % │
├────────────────────────┼──────────────────────────┼──────────────────────────────────────────────┼──────────────────────────────────────────────┼────────────────────────────────┼───────────────────┤
│  coq-mathcomp-solvable │  170.52  178.29  -4.36 % │      474553087615      496405173111  -4.40 % │      671969092230      700552875528  -4.08 % │     659788     818268 -19.37 % │    0    0  +nan % │
├────────────────────────┼──────────────────────────┼──────────────────────────────────────────────┼──────────────────────────────────────────────┼────────────────────────────────┼───────────────────┤
│ coq-mathcomp-character │  154.91  161.72  -4.21 % │      431009004968      449411063390  -4.09 % │      599510400784      623334258813  -3.82 % │     708772     821800 -13.75 % │    0    0  +nan % │
├────────────────────────┼──────────────────────────┼──────────────────────────────────────────────┼──────────────────────────────────────────────┼────────────────────────────────┼───────────────────┤
│         coq-verdi-raft │ 1221.26 1272.34  -4.01 % │     3397612822103     3543336562589  -4.11 % │     4837767102442     4999561961702  -3.24 % │     899868    1905820 -52.78 % │    0    0  +nan % │
├────────────────────────┼──────────────────────────┼──────────────────────────────────────────────┼──────────────────────────────────────────────┼────────────────────────────────┼───────────────────┤
│            coq-unimath │ 3928.44 4089.57  -3.94 % │    10923459757173    11379218360659  -4.01 % │    20980179092759    21531821885219  -2.56 % │    1142420    1144200  -0.16 % │    0    0  +nan % │
├────────────────────────┼──────────────────────────┼──────────────────────────────────────────────┼──────────────────────────────────────────────┼────────────────────────────────┼───────────────────┤
│     coq-mathcomp-field │  223.51  231.82  -3.58 % │      621733341603      645002034166  -3.61 % │      951038065353      984293274301  -3.38 % │     673920     815768 -17.39 % │    0    0  +nan % │
├────────────────────────┼──────────────────────────┼──────────────────────────────────────────────┼──────────────────────────────────────────────┼────────────────────────────────┼───────────────────┤
│            coq-coqutil │   60.75   62.74  -3.17 % │      167661210762      174777517492  -4.07 % │      208679465150      220006315802  -5.15 % │     524164     531244  -1.33 % │    0    0  +nan % │
├────────────────────────┼──────────────────────────┼──────────────────────────────────────────────┼──────────────────────────────────────────────┼────────────────────────────────┼───────────────────┤
│              coq-verdi │  102.87  105.99  -2.94 % │      282577361242      292306008328  -3.33 % │      397692191474      408611393751  -2.67 % │     546136     564680  -3.28 % │    0    0  +nan % │
├────────────────────────┼──────────────────────────┼──────────────────────────────────────────────┼──────────────────────────────────────────────┼────────────────────────────────┼───────────────────┤
│       coq-fiat-parsers │  636.19  654.80  -2.84 % │     1779264641247     1830574658045  -2.80 % │     2725720503646     2754824599960  -1.06 % │    3639300    3671792  -0.88 % │    0    0  +nan % │
├────────────────────────┼──────────────────────────┼──────────────────────────────────────────────┼──────────────────────────────────────────────┼────────────────────────────────┼───────────────────┤
│           coq-bedrock2 │  227.12  230.78  -1.59 % │      627616226500      639467600263  -1.85 % │     1044150975683     1057438361368  -1.26 % │    1085096    1090772  -0.52 % │    0    0  +nan % │
├────────────────────────┼──────────────────────────┼──────────────────────────────────────────────┼──────────────────────────────────────────────┼────────────────────────────────┼───────────────────┤
│          coq-fourcolor │ 2571.54 2515.99  +2.21 % │     7170955552821     7015641817245  +2.21 % │    12433273788812    11550181345462  +7.65 % │     722468     905760 -20.24 % │    0    0  +nan % │
└────────────────────────┴──────────────────────────┴──────────────────────────────────────────────┴──────────────────────────────────────────────┴────────────────────────────────┴───────────────────┘

Results are good, CC @ppedrot
The slowdown on 4ct is kind of expected since #13431
Curiosity: @silene is the -20.24 % in memory usage on 4ct also related to your patch?

@gares
Copy link
Member Author

gares commented Nov 28, 2020

@mattam82 next week is the last one before the beta, please give a shot to the credits

@ejgallego
Copy link
Member

@gares I think you should close this.

@gares gares closed this as completed Apr 30, 2021
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

3 participants