From fe0e7379bee8b7035f4831a2643db2c1f3234e77 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Sat, 19 Dec 2020 17:18:10 +0100 Subject: [PATCH 01/16] new release cycle --- text/052-platform-release-cycle.md | 158 +++++++++++++++++++++++++++++ 1 file changed, 158 insertions(+) create mode 100644 text/052-platform-release-cycle.md diff --git a/text/052-platform-release-cycle.md b/text/052-platform-release-cycle.md new file mode 100644 index 00000000..06a953f0 --- /dev/null +++ b/text/052-platform-release-cycle.md @@ -0,0 +1,158 @@ +- Title: Coq and Coq platform release cycle + +- Driver: Enrico + +---- + +# Summary + +We aim at a release process for Coq and the Coq platform which makes it +easier for users to provide feedback and for developers to deliver fixes. + +In a nutshell the Coq "beta period" is replaced by a Coq platform "beta period". +Coq devs tag an almost final version on top of which the Coq platform core is +built. Coq point release are then used to *quickly* deliver fixes +to the platform. + +# Motivation + +The beta testing period does not provide enough feedback to sensibly improve +Coq between the `VX+beta1` and `VX.0` tags. The reasons are, most important +last: +- users have better things to do, frankly +- one month is short, especially with Christmas, summer holydays or conferences + around (our beta period is December or May) +- in order to test Coq you are likely to need a bunch of Coq packages, and they + are typically only available after the beta period is over + +Moreover the "beta period" is also seen by devs as a time frame where they can +still change many things. As a results users are even less happy to spend time +working on a moving target. + +Finally, due to the cost of backporting breaking changes from the master +branch to the release branch, this only happenes very early in the release +cycle (for example only 2 such changes were backported in the beta period +for 8.12, 0 for 8.13). + +## New actor: platform + +The Coq platform is a selection of Coq packages which work well +for a given Coq version. One of its objective is to disentangle the release +of Coq with the release of other packages. It provides scripts that build +that selection of Coq packages on Windows, Mac and Linux from sources +on the user's machine, and as well binary installers (prebuilt) for users +to quickly get a working environment. + +This product is what users will test in this new model; Coq is a core +component of it. + +# Detailed design + +The new process' timeline: +``` + D D D D D +coq --+---(1)---+------(2)----+-----(3)----+---+--+---- + vX branch/ | | | + X+rc tag/ | | + X.0 tag/ | + X.1 tag/ + + I I +platform -----------+----(4)------+--------(5)---------+ + vX branch/ | | + X+beta tag/ | + X.0 tag/ +Artifacts: +- D = docker image for Coq (and opam package) +- I = binary installers for Coq platform (and opam packages and docker image) +``` + +## Coq + +On time based schedule the RM branches vX. + +1. The RM shepherds the few PR which are ready and pins projects tracked by CI + (using commit hashes, not necessarily tags). Then he tags Coq. This should + take 10 days. No packages are built, just a git tag. A docker image is built, + so that project maintainers can use it in CI. No breaking change is allowed + from now on (unless a severe problem is found). +2. Doc is updated (eg. Changes file) and eventual fixes required by the platform + are done. Ideally no other change is done. This should take 10 days. +3. In response to a severe bug report Coq devs make an hotfix in master which is + backported to vX by the RM which then tags a point release, possibly as soon + as the fix is available and merged. + +## Platform + +When Coq X+rc is tagged, the PRM branches vX + +4. Starting with the pins made by RM on Coq's CI all packages part of the + platform (or its core) are pinned (in accordance with upstreams, which are + notified about the ongoing process). Most, if not all, packages are in Coq's + CI so there should be no surprises, otherwise issues are reported to Coq + devs. When done a X+beta tag is done and packages made available to users. + A docker image with the entire platform prebuilt should be built. This + should take 20 days. +5. As users pick up the platform and find severe bugs in Coq, the platform picks + up point releases of Coq containing hotfixes and eventually extends packages + beyond the core set. + +## Synchronization points + +- The end of (1) starts the release cycle of the platform. +- The end of (2) and (4) don't need to be done at the same time, but if they + are then the new release cycle coincides with the old one (up to the + renaming of X.0 into X+beta). +- Coq's X.0 tag can be made as soon as the doc is clear. This will stress the + fact that upstreams can pin with no worries. + +## Announces + +- Coq tags are only announced to devs +- Coq platform pins are communicated to upstream devs, which may tag/release. +- Coq platform tags and packages are announced to the community + +## Coq CI + +- must test standard configurations +- must test all platform projects with ML parts +- must test a selection of platform scripts (to test the script themselves, + not the build of platform packages) +- should test platform projects with V files which are depended upon in the + platform +- can test anything else of course, including non standard configurations + +## Platform CI + +- on branch vX it should test all packages and build installers as artifacts +- on branch master it should take Coq master and its pins for the subset of + packages it covers and test all the packages, eventually report the + failures upstream + +### Terminology +- "severe bug" is a bug which *blocks* many users with no decent workaround, + or a soundness bug. +- "hotfix" is a minimal patch that repairs a problem, not necessarily the nice + solution which may require refactoring or cleanups. The patch should pass CI + with no overlay and must be reviewable (in a strict sense, as in looking for + bugs, not just as in "looks reasonable") +- "RM" is the release manager of Coq +- "PRM" are the release managers of the Coq platform +- "standard configuration" is a version of ocaml and other tools which are + agreed between Coq devs and the platform devs (dune, make, gmp, gtk...) + +# Drawbacks + +This new process identifies 3 groups of developers which need to talk to each +others: Coq dev, platform devs, and docker devs. This is a risk, but also an +advantage since the Coq release becomes more lightweight, leaving the RM +more time to focus on supporting the release with hotfixes. + +# Alternatives + +We consider docker as *the* platform upstream projects use for testing. +This may be a bit narrow, even if the docker stuff on coq-community is +pretty good IMO. + +# Unresolved questions + From 5ecfea14a68b99c82317a4eb2911a3a0d9e461fc Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Mon, 25 Jan 2021 11:45:58 +0100 Subject: [PATCH 02/16] typos, clarifications, bold text --- text/052-platform-release-cycle.md | 110 ++++++++++++++++------------- 1 file changed, 61 insertions(+), 49 deletions(-) diff --git a/text/052-platform-release-cycle.md b/text/052-platform-release-cycle.md index 06a953f0..744ca333 100644 --- a/text/052-platform-release-cycle.md +++ b/text/052-platform-release-cycle.md @@ -25,12 +25,12 @@ last: - in order to test Coq you are likely to need a bunch of Coq packages, and they are typically only available after the beta period is over -Moreover the "beta period" is also seen by devs as a time frame where they can -still change many things. As a results users are even less happy to spend time -working on a moving target. +Moreover the "beta period" has also been seen by devs as a time frame where +they can still change many things. As a results users are even less happy +to spend time working on a moving target. Finally, due to the cost of backporting breaking changes from the master -branch to the release branch, this only happenes very early in the release +branch to the release branch, this only happens very early in the release cycle (for example only 2 such changes were backported in the beta period for 8.12, 0 for 8.13). @@ -50,21 +50,22 @@ component of it. The new process' timeline: ``` - D D D D D + DO+ O O O O coq --+---(1)---+------(2)----+-----(3)----+---+--+---- vX branch/ | | | - X+rc tag/ | | - X.0 tag/ | - X.1 tag/ + VX+rc tag/ | | + VX.0 tag/ | + VX.1 tag/ - I I + DI DI platform -----------+----(4)------+--------(5)---------+ vX branch/ | | - X+beta tag/ | - X.0 tag/ + VX.0+beta tag/ | + VX.0.0 tag/ Artifacts: -- D = docker image for Coq (and opam package) -- I = binary installers for Coq platform (and opam packages and docker image) +- D = docker image for Coq (or Coq + the platform) +- O = OPAM package (O+ means for core-dev, otherwise it is for the main OPAM repo) +- I = binary installers for Coq platform ``` ## Coq @@ -72,62 +73,82 @@ Artifacts: On time based schedule the RM branches vX. 1. The RM shepherds the few PR which are ready and pins projects tracked by CI - (using commit hashes, not necessarily tags). Then he tags Coq. This should - take 10 days. No packages are built, just a git tag. A docker image is built, - so that project maintainers can use it in CI. No breaking change is allowed - from now on (unless a severe problem is found). -2. Doc is updated (eg. Changes file) and eventual fixes required by the platform - are done. Ideally no other change is done. This should take 10 days. + (using commit hashes, not necessarily tags), then the TM tags VX+rc. + This step should take no more than 10 days (2 working week). + No binary installers are built and published by the RM, just a git tag. + The RM writes an OPAM package, currently the policy is to upload it to + `core-dev`. + Possibly, the RM builds a docker image, so that project maintainers can use it + in CI during (4). + **No breaking change is allowed from now on, unless a severe problem is found.** +2. The documentation is updated (eg. the Changes file) and eventual fixes + required by the platform are done. Ideally no other change is done. + This step should take no more than 10 days. 3. In response to a severe bug report Coq devs make an hotfix in master which is backported to vX by the RM which then tags a point release, possibly as soon - as the fix is available and merged. + as the fix is available and merged. The RM writes an OPAM package for + the main OPAM repository. ## Platform -When Coq X+rc is tagged, the PRM branches vX +When Coq VX+rc is tagged, the PRM branches vX 4. Starting with the pins made by RM on Coq's CI all packages part of the platform (or its core) are pinned (in accordance with upstreams, which are notified about the ongoing process). Most, if not all, packages are in Coq's - CI so there should be no surprises, otherwise issues are reported to Coq - devs. When done a X+beta tag is done and packages made available to users. + CI or the Platform's CI so there should be no surprises. + When done a VX.0+beta tag is done and packages made available to users. A docker image with the entire platform prebuilt should be built. This should take 20 days. 5. As users pick up the platform and find severe bugs in Coq, the platform picks up point releases of Coq containing hotfixes and eventually extends packages beyond the core set. +### Platform versioning + +It is out of the scope of this CEP to chose a versioning schema for the +platform. In the diagram above we append a .digit to the Coq version (one +of the current proposals). + ## Synchronization points - The end of (1) starts the release cycle of the platform. - The end of (2) and (4) don't need to be done at the same time, but if they - are then the new release cycle coincides with the old one (up to the - renaming of X.0 into X+beta). -- Coq's X.0 tag can be made as soon as the doc is clear. This will stress the + are then the release cycle presented in this CEP roughly coincides with the + previous one. Normally (2) precedes (4), but if the doc is not ready yet + the platform can still release a beta. +- Coq's VX.0 tag can be made as soon as the doc is clear. This will stress the fact that upstreams can pin with no worries. ## Announces - Coq tags are only announced to devs - Coq platform pins are communicated to upstream devs, which may tag/release. -- Coq platform tags and packages are announced to the community - -## Coq CI - -- must test standard configurations -- must test all platform projects with ML parts -- must test a selection of platform scripts (to test the script themselves, - not the build of platform packages) -- should test platform projects with V files which are depended upon in the - platform +- Coq platform tags and packages **are announced to the community** (this is + when we party) + +## Coq's CI + +- must test **one configuration**: it cannot use one compiler version or + compiler flavor to test one project, and a different one to test another one, + since the platform can only have one +- must test **all platform projects with ML parts**. The platform devs must ensure + this invariant, since they are the ones adding packages to the platform +- must test a **selection of platform scripts** (to test the script themselves, + not the build of platform packages). Currently the `-extent=i` platform flag + makes it build only Coq+CoqIDE, that should be sufficient. +- should test **key platform projects** (projects which are heavily depended + upon in the platform, even if the are "pure .v projects", e.g. mathcomp). - can test anything else of course, including non standard configurations ## Platform CI -- on branch vX it should test all packages and build installers as artifacts -- on branch master it should take Coq master and its pins for the subset of - packages it covers and test all the packages, eventually report the - failures upstream +- on branch vX it must test all packages and build installers as artifacts. + This makes the platform release doable without specific hardware (e.g. a Mac + or a PC with windows). +- on branch master it should take Coq master and its upstream tracked branches + (for the subset of projects part of the platform) and eventually report the + failures upstream. Currently this activity is logged in dedicated issues. ### Terminology - "severe bug" is a bug which *blocks* many users with no decent workaround, @@ -147,12 +168,3 @@ This new process identifies 3 groups of developers which need to talk to each others: Coq dev, platform devs, and docker devs. This is a risk, but also an advantage since the Coq release becomes more lightweight, leaving the RM more time to focus on supporting the release with hotfixes. - -# Alternatives - -We consider docker as *the* platform upstream projects use for testing. -This may be a bit narrow, even if the docker stuff on coq-community is -pretty good IMO. - -# Unresolved questions - From bc1036ee5e7139b604e69fb8b520147cc2e07a7e Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Mon, 25 Jan 2021 11:57:44 +0100 Subject: [PATCH 03/16] fixes --- text/052-platform-release-cycle.md | 20 ++++++++++---------- 1 file changed, 10 insertions(+), 10 deletions(-) diff --git a/text/052-platform-release-cycle.md b/text/052-platform-release-cycle.md index 744ca333..1334f85e 100644 --- a/text/052-platform-release-cycle.md +++ b/text/052-platform-release-cycle.md @@ -9,9 +9,9 @@ We aim at a release process for Coq and the Coq platform which makes it easier for users to provide feedback and for developers to deliver fixes. -In a nutshell the Coq "beta period" is replaced by a Coq platform "beta period". +In a nutshell the *Coq "beta period"* is replaced by a **Coq platform "beta period"**. Coq devs tag an almost final version on top of which the Coq platform core is -built. Coq point release are then used to *quickly* deliver fixes +built. Coq point release are then used to quickly deliver fixes to the platform. # Motivation @@ -43,8 +43,8 @@ that selection of Coq packages on Windows, Mac and Linux from sources on the user's machine, and as well binary installers (prebuilt) for users to quickly get a working environment. -This product is what users will test in this new model; Coq is a core -component of it. +**The platform is the final product users will get** in this new model; +Coq is a core component of it. # Detailed design @@ -73,10 +73,10 @@ Artifacts: On time based schedule the RM branches vX. 1. The RM shepherds the few PR which are ready and pins projects tracked by CI - (using commit hashes, not necessarily tags), then the TM tags VX+rc. + (using commit hashes, not necessarily tags), then the RM **tags VX+rc**. This step should take no more than 10 days (2 working week). No binary installers are built and published by the RM, just a git tag. - The RM writes an OPAM package, currently the policy is to upload it to + The RM writes an **OPAM package**, currently the policy is to upload it to `core-dev`. Possibly, the RM builds a docker image, so that project maintainers can use it in CI during (4). @@ -97,8 +97,8 @@ When Coq VX+rc is tagged, the PRM branches vX platform (or its core) are pinned (in accordance with upstreams, which are notified about the ongoing process). Most, if not all, packages are in Coq's CI or the Platform's CI so there should be no surprises. - When done a VX.0+beta tag is done and packages made available to users. - A docker image with the entire platform prebuilt should be built. This + When done a **VX.0+beta tag** is done and **binary installers** made available to users. + A **docker image** with the entire platform prebuilt should be built. This should take 20 days. 5. As users pick up the platform and find severe bugs in Coq, the platform picks up point releases of Coq containing hotfixes and eventually extends packages @@ -143,10 +143,10 @@ of the current proposals). ## Platform CI -- on branch vX it must test all packages and build installers as artifacts. +- on branch **vX** it must test **all packages** and build **installers** as artifacts. This makes the platform release doable without specific hardware (e.g. a Mac or a PC with windows). -- on branch master it should take Coq master and its upstream tracked branches +- on branch **master** it should take Coq master and its **upstream tracked branches** (for the subset of projects part of the platform) and eventually report the failures upstream. Currently this activity is logged in dedicated issues. From 80ae9cf0546715c8b258d280341c422efd103f48 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Mon, 25 Jan 2021 14:35:05 +0100 Subject: [PATCH 04/16] corrections --- text/052-platform-release-cycle.md | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) diff --git a/text/052-platform-release-cycle.md b/text/052-platform-release-cycle.md index 1334f85e..a338f2a5 100644 --- a/text/052-platform-release-cycle.md +++ b/text/052-platform-release-cycle.md @@ -74,8 +74,8 @@ On time based schedule the RM branches vX. 1. The RM shepherds the few PR which are ready and pins projects tracked by CI (using commit hashes, not necessarily tags), then the RM **tags VX+rc**. - This step should take no more than 10 days (2 working week). - No binary installers are built and published by the RM, just a git tag. + This step should take no more than 2 weeks. + The RM **tags**, but produces no binary installers, see the platform release. The RM writes an **OPAM package**, currently the policy is to upload it to `core-dev`. Possibly, the RM builds a docker image, so that project maintainers can use it @@ -83,7 +83,7 @@ On time based schedule the RM branches vX. **No breaking change is allowed from now on, unless a severe problem is found.** 2. The documentation is updated (eg. the Changes file) and eventual fixes required by the platform are done. Ideally no other change is done. - This step should take no more than 10 days. + This step should take no more than 2 weeks. 3. In response to a severe bug report Coq devs make an hotfix in master which is backported to vX by the RM which then tags a point release, possibly as soon as the fix is available and merged. The RM writes an OPAM package for @@ -97,9 +97,9 @@ When Coq VX+rc is tagged, the PRM branches vX platform (or its core) are pinned (in accordance with upstreams, which are notified about the ongoing process). Most, if not all, packages are in Coq's CI or the Platform's CI so there should be no surprises. - When done a **VX.0+beta tag** is done and **binary installers** made available to users. - A **docker image** with the entire platform prebuilt should be built. This - should take 20 days. + When done the PRM makes the **VX.0+beta tag** and publishes the **binary installers**. + The PRM may also provide a **docker image** with the entire platform prebuilt. + This step should not take more than one month. 5. As users pick up the platform and find severe bugs in Coq, the platform picks up point releases of Coq containing hotfixes and eventually extends packages beyond the core set. From 94b02d3dcb94dfcd40b42ec10535d3ce16a09ff2 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Mon, 25 Jan 2021 15:49:50 +0100 Subject: [PATCH 05/16] deliverables --- text/052-platform-release-cycle.md | 26 +++++++++++++++----------- 1 file changed, 15 insertions(+), 11 deletions(-) diff --git a/text/052-platform-release-cycle.md b/text/052-platform-release-cycle.md index a338f2a5..0e4aa0b1 100644 --- a/text/052-platform-release-cycle.md +++ b/text/052-platform-release-cycle.md @@ -73,21 +73,25 @@ Artifacts: On time based schedule the RM branches vX. 1. The RM shepherds the few PR which are ready and pins projects tracked by CI - (using commit hashes, not necessarily tags), then the RM **tags VX+rc**. + (using commit hashes, not necessarily tags). This step should take no more than 2 weeks. - The RM **tags**, but produces no binary installers, see the platform release. - The RM writes an **OPAM package**, currently the policy is to upload it to - `core-dev`. - Possibly, the RM builds a docker image, so that project maintainers can use it - in CI during (4). + - The RM **tags** VX+rc, but produces no binary installers, see the platform release. + - The RM writes an **OPAM package**, currently the policy is to upload it to + `core-dev`. + - Possibly, the RM builds a docker image, so that project maintainers can use it + in CI during (4). + **No breaking change is allowed from now on, unless a severe problem is found.** 2. The documentation is updated (eg. the Changes file) and eventual fixes required by the platform are done. Ideally no other change is done. This step should take no more than 2 weeks. + - The RM **tags** the .0 release. + - The RM writes an **OPAM package** for the main OPAM repository. 3. In response to a severe bug report Coq devs make an hotfix in master which is - backported to vX by the RM which then tags a point release, possibly as soon - as the fix is available and merged. The RM writes an OPAM package for - the main OPAM repository. + backported to vX. + - The RM **tags** the point release, possibly as soon + as the fix is available and merged. + - The RM writes an **OPAM package** for the main OPAM repository. ## Platform @@ -97,9 +101,9 @@ When Coq VX+rc is tagged, the PRM branches vX platform (or its core) are pinned (in accordance with upstreams, which are notified about the ongoing process). Most, if not all, packages are in Coq's CI or the Platform's CI so there should be no surprises. - When done the PRM makes the **VX.0+beta tag** and publishes the **binary installers**. - The PRM may also provide a **docker image** with the entire platform prebuilt. This step should not take more than one month. + - The PRM **tags** VX.0+beta tag and publishes the **binary installers** + - The PRM may also provide a **docker image** with the entire platform prebuilt 5. As users pick up the platform and find severe bugs in Coq, the platform picks up point releases of Coq containing hotfixes and eventually extends packages beyond the core set. From a1105ddfc86bf14fa88154e9e2f7f3ddc7848b8e Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Mon, 25 Jan 2021 21:40:33 +0100 Subject: [PATCH 06/16] fix misleading diagram --- text/052-platform-release-cycle.md | 24 ++++++++++++------------ 1 file changed, 12 insertions(+), 12 deletions(-) diff --git a/text/052-platform-release-cycle.md b/text/052-platform-release-cycle.md index 0e4aa0b1..3dc7eebd 100644 --- a/text/052-platform-release-cycle.md +++ b/text/052-platform-release-cycle.md @@ -50,18 +50,18 @@ Coq is a core component of it. The new process' timeline: ``` - DO+ O O O O -coq --+---(1)---+------(2)----+-----(3)----+---+--+---- - vX branch/ | | | - VX+rc tag/ | | - VX.0 tag/ | - VX.1 tag/ - - DI DI -platform -----------+----(4)------+--------(5)---------+ - vX branch/ | | - VX.0+beta tag/ | - VX.0.0 tag/ + DO+ O O O O +coq --+---(1)---+------(2)----+----------(3)------------+---+--+---- + vX branch/ | | | + VX+rc tag/ | | + VX.0 tag/ | + VX.1 tag/ + + DI DI DI +platform -----------+----(4)------+--------(5)---------+-------+------- + vX branch/ | | | + VX.0+beta tag/ | | + VX.0.0 tag/ .../ Artifacts: - D = docker image for Coq (or Coq + the platform) - O = OPAM package (O+ means for core-dev, otherwise it is for the main OPAM repo) From dd36a464e7ddf5d9220c8688f22dcecc819e0b68 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Tue, 26 Jan 2021 10:40:42 +0100 Subject: [PATCH 07/16] Update text/052-platform-release-cycle.md MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Co-authored-by: Théo Zimmermann --- text/052-platform-release-cycle.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/text/052-platform-release-cycle.md b/text/052-platform-release-cycle.md index 3dc7eebd..c8a7ddcd 100644 --- a/text/052-platform-release-cycle.md +++ b/text/052-platform-release-cycle.md @@ -122,7 +122,7 @@ of the current proposals). previous one. Normally (2) precedes (4), but if the doc is not ready yet the platform can still release a beta. - Coq's VX.0 tag can be made as soon as the doc is clear. This will stress the - fact that upstreams can pin with no worries. + fact that upstreams can pin with no worries as soon as the rc is tagged. ## Announces From f0f5f381f4be728a298272d1a7c18259e1306e7b Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Tue, 26 Jan 2021 10:40:56 +0100 Subject: [PATCH 08/16] Update text/052-platform-release-cycle.md MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Co-authored-by: Théo Zimmermann --- text/052-platform-release-cycle.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/text/052-platform-release-cycle.md b/text/052-platform-release-cycle.md index c8a7ddcd..12808b35 100644 --- a/text/052-platform-release-cycle.md +++ b/text/052-platform-release-cycle.md @@ -72,7 +72,7 @@ Artifacts: On time based schedule the RM branches vX. -1. The RM shepherds the few PR which are ready and pins projects tracked by CI +1. The RM shepherds the few PR which are ready, ensures blocker issues are fixed and pins projects tracked by CI (using commit hashes, not necessarily tags). This step should take no more than 2 weeks. - The RM **tags** VX+rc, but produces no binary installers, see the platform release. From fc89e647164044ee8f1675d74713d58fe014dbc1 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Tue, 26 Jan 2021 11:27:25 +0100 Subject: [PATCH 09/16] rc1 --- text/052-platform-release-cycle.md | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/text/052-platform-release-cycle.md b/text/052-platform-release-cycle.md index 12808b35..d7c32090 100644 --- a/text/052-platform-release-cycle.md +++ b/text/052-platform-release-cycle.md @@ -53,7 +53,7 @@ The new process' timeline: DO+ O O O O coq --+---(1)---+------(2)----+----------(3)------------+---+--+---- vX branch/ | | | - VX+rc tag/ | | + VX+rc1 tag/ | | VX.0 tag/ | VX.1 tag/ @@ -75,7 +75,7 @@ On time based schedule the RM branches vX. 1. The RM shepherds the few PR which are ready, ensures blocker issues are fixed and pins projects tracked by CI (using commit hashes, not necessarily tags). This step should take no more than 2 weeks. - - The RM **tags** VX+rc, but produces no binary installers, see the platform release. + - The RM **tags** VX+rc1, but produces no binary installers, see the platform release. - The RM writes an **OPAM package**, currently the policy is to upload it to `core-dev`. - Possibly, the RM builds a docker image, so that project maintainers can use it @@ -95,7 +95,7 @@ On time based schedule the RM branches vX. ## Platform -When Coq VX+rc is tagged, the PRM branches vX +When Coq VX+rc1 is tagged, the PRM branches vX 4. Starting with the pins made by RM on Coq's CI all packages part of the platform (or its core) are pinned (in accordance with upstreams, which are From f1599781f4340b0ae5dbbee3a79b8d822471ee7b Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Tue, 26 Jan 2021 16:15:21 +0100 Subject: [PATCH 10/16] changelog --- text/052-platform-release-cycle.md | 7 +++++-- 1 file changed, 5 insertions(+), 2 deletions(-) diff --git a/text/052-platform-release-cycle.md b/text/052-platform-release-cycle.md index d7c32090..81f3af24 100644 --- a/text/052-platform-release-cycle.md +++ b/text/052-platform-release-cycle.md @@ -72,8 +72,11 @@ Artifacts: On time based schedule the RM branches vX. -1. The RM shepherds the few PR which are ready, ensures blocker issues are fixed and pins projects tracked by CI - (using commit hashes, not necessarily tags). +1. The RM shepherds the few PR which are ready, ensures blocker issues are fixed + and pins projects tracked by CI (using commit hashes, not necessarily tags). + The RM generates the Changelog file via the `generate-release-changelog.sh` + script, but leaves the release notes empty (it's the project leader which + fill them in before the .0 release). This step should take no more than 2 weeks. - The RM **tags** VX+rc1, but produces no binary installers, see the platform release. - The RM writes an **OPAM package**, currently the policy is to upload it to From 4e9b9124c5b9cffd69ea840a5cf10b8a59b4490e Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Tue, 26 Jan 2021 16:41:18 +0100 Subject: [PATCH 11/16] clarify CI --- text/052-platform-release-cycle.md | 35 ++++++++++++++++++++---------- 1 file changed, 24 insertions(+), 11 deletions(-) diff --git a/text/052-platform-release-cycle.md b/text/052-platform-release-cycle.md index 81f3af24..940af449 100644 --- a/text/052-platform-release-cycle.md +++ b/text/052-platform-release-cycle.md @@ -136,17 +136,28 @@ of the current proposals). ## Coq's CI -- must test **one configuration**: it cannot use one compiler version or - compiler flavor to test one project, and a different one to test another one, - since the platform can only have one -- must test **all platform projects with ML parts**. The platform devs must ensure - this invariant, since they are the ones adding packages to the platform -- must test a **selection of platform scripts** (to test the script themselves, - not the build of platform packages). Currently the `-extent=i` platform flag +For each project P included in the platform: + +- if P has ML code, then it must be tested using the **standard configuration**. + It can also be tested using another configuration. +- if P is pure .v code we have two cases + - if it is a core platform component (has many users in the platform) the it + must be tested using the standard configuration. It can also be tested using + another configuration. + - if it is not a core component, then it can be tested with any configuration, + or not tested at all (it must be tested by the platform's CI anyway) + +The decision of which is the "standard configuration" and the switch to a new +one is subject to discussion between the Coq developers and the platform ones, +and the switch should happen in a coordinated way. + +Moreover, Coq's CI must test: +- a **selection of platform scripts**, to test the script themselves, + not the build of platform packages. Currently the `-extent=i` platform flag makes it build only Coq+CoqIDE, that should be sufficient. -- should test **key platform projects** (projects which are heavily depended - upon in the platform, even if the are "pure .v projects", e.g. mathcomp). -- can test anything else of course, including non standard configurations + +Coq's CI can test anything else of course, including non standard +configurations and projects that are no in the platform. ## Platform CI @@ -167,7 +178,9 @@ of the current proposals). - "RM" is the release manager of Coq - "PRM" are the release managers of the Coq platform - "standard configuration" is a version of ocaml and other tools which are - agreed between Coq devs and the platform devs (dune, make, gmp, gtk...) + agreed between Coq devs and the platform devs (dune, make, gmp, gtk...) as + well as a set of configure options or env variables for Coq (eg enabling or + disabling native_compute, tuning OCaml's GC, tweaking the stack size) # Drawbacks From 70af1cc63f9f6395bbc5e0b52a6407ed4b17ab38 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Tue, 26 Jan 2021 16:43:37 +0100 Subject: [PATCH 12/16] reword task opam package --- text/052-platform-release-cycle.md | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/text/052-platform-release-cycle.md b/text/052-platform-release-cycle.md index 940af449..c3b66a0e 100644 --- a/text/052-platform-release-cycle.md +++ b/text/052-platform-release-cycle.md @@ -79,7 +79,7 @@ On time based schedule the RM branches vX. fill them in before the .0 release). This step should take no more than 2 weeks. - The RM **tags** VX+rc1, but produces no binary installers, see the platform release. - - The RM writes an **OPAM package**, currently the policy is to upload it to + - The RM ensures an **OPAM package** is available, currently the policy is to upload it to `core-dev`. - Possibly, the RM builds a docker image, so that project maintainers can use it in CI during (4). @@ -89,12 +89,12 @@ On time based schedule the RM branches vX. required by the platform are done. Ideally no other change is done. This step should take no more than 2 weeks. - The RM **tags** the .0 release. - - The RM writes an **OPAM package** for the main OPAM repository. + - The RM ensures an **OPAM package** is uploaded to the main OPAM repository. 3. In response to a severe bug report Coq devs make an hotfix in master which is backported to vX. - The RM **tags** the point release, possibly as soon as the fix is available and merged. - - The RM writes an **OPAM package** for the main OPAM repository. + - The RM ensures an **OPAM package** is uploaded to the main OPAM repository. ## Platform From 0be5379ca1b39e75e11661084caeda9b47251d08 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Wed, 27 Jan 2021 08:02:43 +0100 Subject: [PATCH 13/16] Apply suggestions from code review Co-authored-by: Erik Martin-Dorel --- text/052-platform-release-cycle.md | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/text/052-platform-release-cycle.md b/text/052-platform-release-cycle.md index c3b66a0e..65752e22 100644 --- a/text/052-platform-release-cycle.md +++ b/text/052-platform-release-cycle.md @@ -63,7 +63,7 @@ platform -----------+----(4)------+--------(5)---------+-------+------- VX.0+beta tag/ | | VX.0.0 tag/ .../ Artifacts: -- D = docker image for Coq (or Coq + the platform) +- D = Docker image for Coq (or Coq + the platform) - O = OPAM package (O+ means for core-dev, otherwise it is for the main OPAM repo) - I = binary installers for Coq platform ``` @@ -81,7 +81,7 @@ On time based schedule the RM branches vX. - The RM **tags** VX+rc1, but produces no binary installers, see the platform release. - The RM ensures an **OPAM package** is available, currently the policy is to upload it to `core-dev`. - - Possibly, the RM builds a docker image, so that project maintainers can use it + - Subsequently, the RM ensures a **Docker image** is available, so that project maintainers can use it in CI during (4). **No breaking change is allowed from now on, unless a severe problem is found.** @@ -106,7 +106,7 @@ When Coq VX+rc1 is tagged, the PRM branches vX CI or the Platform's CI so there should be no surprises. This step should not take more than one month. - The PRM **tags** VX.0+beta tag and publishes the **binary installers** - - The PRM may also provide a **docker image** with the entire platform prebuilt + - The PRM also ensures a **Docker image** is available with the entire platform prebuilt 5. As users pick up the platform and find severe bugs in Coq, the platform picks up point releases of Coq containing hotfixes and eventually extends packages beyond the core set. @@ -185,6 +185,6 @@ configurations and projects that are no in the platform. # Drawbacks This new process identifies 3 groups of developers which need to talk to each -others: Coq dev, platform devs, and docker devs. This is a risk, but also an +others: Coq dev, platform devs, and Docker devs. This is a risk, but also an advantage since the Coq release becomes more lightweight, leaving the RM more time to focus on supporting the release with hotfixes. From 93e1eeccf2f795721ee4b29b2c8b35f820431e15 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Mon, 8 Feb 2021 16:32:32 +0100 Subject: [PATCH 14/16] discussion about platform's versioning --- text/052-platform-release-cycle.md | 33 ++++++++++++++++++++---------- 1 file changed, 22 insertions(+), 11 deletions(-) diff --git a/text/052-platform-release-cycle.md b/text/052-platform-release-cycle.md index 65752e22..83b9c152 100644 --- a/text/052-platform-release-cycle.md +++ b/text/052-platform-release-cycle.md @@ -50,18 +50,18 @@ Coq is a core component of it. The new process' timeline: ``` - DO+ O O O O -coq --+---(1)---+------(2)----+----------(3)------------+---+--+---- + DO+ O O O O +coq --+---(1)---+------(2)----+----------(3)------------+------+-----+----- vX branch/ | | | VX+rc1 tag/ | | VX.0 tag/ | VX.1 tag/ - DI DI DI -platform -----------+----(4)------+--------(5)---------+-------+------- - vX branch/ | | | - VX.0+beta tag/ | | - VX.0.0 tag/ .../ + DI DI DI +platform -----------+----(4)------+--------(5)---------+---------------+------- + YYYY.MM branch/ | | | + YYYY.MM+beta tag/ | | + YYYY.MM.0 tag/ YYYY.MM.1 tag/ Artifacts: - D = Docker image for Coq (or Coq + the platform) - O = OPAM package (O+ means for core-dev, otherwise it is for the main OPAM repo) @@ -98,14 +98,14 @@ On time based schedule the RM branches vX. ## Platform -When Coq VX+rc1 is tagged, the PRM branches vX +When Coq VX+rc1 is tagged, the PRM branches YYYY.MM off 4. Starting with the pins made by RM on Coq's CI all packages part of the platform (or its core) are pinned (in accordance with upstreams, which are notified about the ongoing process). Most, if not all, packages are in Coq's CI or the Platform's CI so there should be no surprises. This step should not take more than one month. - - The PRM **tags** VX.0+beta tag and publishes the **binary installers** + - The PRM **tags** YY.MM+beta tag and publishes the **binary installers** - The PRM also ensures a **Docker image** is available with the entire platform prebuilt 5. As users pick up the platform and find severe bugs in Coq, the platform picks up point releases of Coq containing hotfixes and eventually extends packages @@ -161,10 +161,12 @@ configurations and projects that are no in the platform. ## Platform CI -- on branch **vX** it must test **all packages** and build **installers** as artifacts. +- on branch **YYYY.MM** it must test **all packages** and + build **installers** as artifacts. This makes the platform release doable without specific hardware (e.g. a Mac or a PC with windows). -- on branch **master** it should take Coq master and its **upstream tracked branches** +- on branch **master** it should take Coq master and its + **upstream tracked branches** (for the subset of projects part of the platform) and eventually report the failures upstream. Currently this activity is logged in dedicated issues. @@ -182,6 +184,15 @@ configurations and projects that are no in the platform. well as a set of configure options or env variables for Coq (eg enabling or disabling native_compute, tuning OCaml's GC, tweaking the stack size) + +### Notes about platform versioning + +It's essentially the Ubuntu scheme: +- YYYY.MM plays the role of a major version, as in Coq's 8.13 +- YYYY.MM.0, YYYY.MM.1 ... play the role of point releases, as Coq's 8.13.0 .. + +Hence, it is not YYYY.MM.DD byt rather YYYY.MM.XX. + # Drawbacks This new process identifies 3 groups of developers which need to talk to each From bf9fcf8d48799bc0722b5b3fe092903f048df42c Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Tue, 9 Feb 2021 14:26:54 +0100 Subject: [PATCH 15/16] Apply suggestions from code review MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Co-authored-by: Théo Zimmermann --- text/052-platform-release-cycle.md | 21 ++++++++------------- 1 file changed, 8 insertions(+), 13 deletions(-) diff --git a/text/052-platform-release-cycle.md b/text/052-platform-release-cycle.md index 83b9c152..ad89fb3d 100644 --- a/text/052-platform-release-cycle.md +++ b/text/052-platform-release-cycle.md @@ -11,7 +11,7 @@ easier for users to provide feedback and for developers to deliver fixes. In a nutshell the *Coq "beta period"* is replaced by a **Coq platform "beta period"**. Coq devs tag an almost final version on top of which the Coq platform core is -built. Coq point release are then used to quickly deliver fixes +built. Coq point releases are then used to quickly deliver fixes to the platform. # Motivation @@ -20,13 +20,13 @@ The beta testing period does not provide enough feedback to sensibly improve Coq between the `VX+beta1` and `VX.0` tags. The reasons are, most important last: - users have better things to do, frankly -- one month is short, especially with Christmas, summer holydays or conferences +- one month is short, especially with Christmas, summer holidays or conferences around (our beta period is December or May) - in order to test Coq you are likely to need a bunch of Coq packages, and they are typically only available after the beta period is over Moreover the "beta period" has also been seen by devs as a time frame where -they can still change many things. As a results users are even less happy +they can still change many things. As a result, users are even less happy to spend time working on a moving target. Finally, due to the cost of backporting breaking changes from the master @@ -72,11 +72,11 @@ Artifacts: On time based schedule the RM branches vX. -1. The RM shepherds the few PR which are ready, ensures blocker issues are fixed +1. The RM shepherds the few PRs which are ready, ensures blocker issues are fixed and pins projects tracked by CI (using commit hashes, not necessarily tags). The RM generates the Changelog file via the `generate-release-changelog.sh` - script, but leaves the release notes empty (it's the project leader which - fill them in before the .0 release). + script, but leaves the release notes empty (it's the project leader who + fills them in before the .0 release). This step should take no more than 2 weeks. - The RM **tags** VX+rc1, but produces no binary installers, see the platform release. - The RM ensures an **OPAM package** is available, currently the policy is to upload it to @@ -111,11 +111,6 @@ When Coq VX+rc1 is tagged, the PRM branches YYYY.MM off up point releases of Coq containing hotfixes and eventually extends packages beyond the core set. -### Platform versioning - -It is out of the scope of this CEP to chose a versioning schema for the -platform. In the diagram above we append a .digit to the Coq version (one -of the current proposals). ## Synchronization points @@ -141,7 +136,7 @@ For each project P included in the platform: - if P has ML code, then it must be tested using the **standard configuration**. It can also be tested using another configuration. - if P is pure .v code we have two cases - - if it is a core platform component (has many users in the platform) the it + - if it is a core platform component (has many users in the platform) then it must be tested using the standard configuration. It can also be tested using another configuration. - if it is not a core component, then it can be tested with any configuration, @@ -157,7 +152,7 @@ Moreover, Coq's CI must test: makes it build only Coq+CoqIDE, that should be sufficient. Coq's CI can test anything else of course, including non standard -configurations and projects that are no in the platform. +configurations and projects that are not in the platform. ## Platform CI From 230c2fa8e257122ed73946c7382d44d8c6a1180e Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Wed, 10 Feb 2021 17:10:00 +0100 Subject: [PATCH 16/16] Update text/052-platform-release-cycle.md --- text/052-platform-release-cycle.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/text/052-platform-release-cycle.md b/text/052-platform-release-cycle.md index ad89fb3d..b790ed16 100644 --- a/text/052-platform-release-cycle.md +++ b/text/052-platform-release-cycle.md @@ -186,7 +186,7 @@ It's essentially the Ubuntu scheme: - YYYY.MM plays the role of a major version, as in Coq's 8.13 - YYYY.MM.0, YYYY.MM.1 ... play the role of point releases, as Coq's 8.13.0 .. -Hence, it is not YYYY.MM.DD byt rather YYYY.MM.XX. +Hence, it is not YYYY.MM.DD but rather YYYY.MM.XX. # Drawbacks