-
Notifications
You must be signed in to change notification settings - Fork 6
Commit, branch and release policies
Coq plugins are advised to use branch names that reflect Coq's branch names and
which track the corresponding version of Coq. In particular, the master branch
would track the development version of Coq, while the various v8.x branches
would track the corresponding stable version of Coq.
Indeed, at the current time, it is impossible for the Coq development team to provide a stable API.
Moreover, plugins are encouraged to join Coq's CI to get frequent compatibility updates from the Coq development team.
Tag and release numbering can use the scheme X.Y.Z+coqV.W where X.Y.Z is a
release number that corresponds to the features of the plugin (following
semantic versioning, Z is increased for bug-fix releases, Y is
increased when new features are added, and X is increased when there are breaking
changes) while coqV.W indicates with which version of Coq this version of the
plugin is compatible.
Coq libraries are advised to follow a math-comp-like compatibility
policy, i.e. to do all the development on a master branch and to keep this branch
compatible with a range of at least two Coq versions, including the latest stable
version of Coq.
The use of CI is very useful to ensure that this property is not broken, and thus very recommended. CI is updated whenever the range of supported Coq versions changes.
Tags and releases can use a simple X.Y.Z numbering scheme and simply indicate
which versions of Coq are supported in the release notes.
Coq packages that used to be maintained in https://github.com/coq-contribs, even when they are not plugins, usually followed the branch scheme recommended for plugins. Indeed, given that the Coq development team maintained a large number of contribs, uniformity was useful to handle all these packages in a systematic fashion. Furthermore, trying to maintain compatibility with a range of versions would have made the task even more complex.
When such historic v8.X branches exist, we recommend keeping them around, even if no
new such branches are created. When tags in V8.X.Y format were used as well, the new
tags should use higher version numbers. Jumping directly to V10.0.0 can be a way of
separating from the previous numbering scheme.
It is generally advised to use topic branches to conduct development. This will allow CI to run before merging the changes back in the main branch (removal of the topic branch is recommended after the branch's content has been merged). Going through a pull request may also help get reviews from other maintainers / contributors.
It is up to the project maintainer to decide which policy to adopt. GitHub's branch protection feature may be used to enforce this policy (required status checks, required review requests...).
The manifesto repository enforces the policy that all changes must go through pull requests and get at least one approved review (and no "request for changes") before getting merged.
It is advised that, as a minimum, OPAM packages for project releases are submitted to the released repository in the Coq OPAM archive. This ensures that a release can be easily installed by users of a stable Coq version.
Adding a new OPAM package is done by submitting pull requests to the Coq OPAM archive with an appropriate opam file. When submitting a package for a release, be sure to include the date of the release under the tags field in the opam file. For example, if the release of a project was on July 24, 2018, tags may be defined as:
tags: [
"keyword:canonical structures"
"keyword:proof automation"
"category:Computer Science/Data Types and Data Structures"
"date:2018-07-24"
"logpath:LemmaOverloading"
]