Pull request title and description conventions #
We are using the following convention for writing pull request titles and descriptions.
Note: "Title:" and "Description:" do not actually appear
Title: <type>(<optional-scope>): <subject> Description: <body> <NEWLINE> <footer> <NEWLINE> <dependencies>
- feat (feature)
- fix (bug fix)
- doc (documentation)
- style (formatting, missing semicolons, ...)
- test (when adding missing tests)
- chore (maintain)
- perf (performance improvement, optimization, ...)
<optional-scope> is a name of module or a directory which contains changed modules.
This is not necessary to include, but may be useful if the
<subject> is insufficient.
Mathlib directory prefix is always omitted.
For instance, it could be
<subject> has the following constraints:
- use imperative, present tense: "change" not "changed" nor "changes"
- do not capitalize the first letter
- no dot(.) at the end
<body> has the following constraints:
- just as in
<subject>, use imperative, present tense
- include motivation for the change and contrast with previous behavior
<footer> is optional and may contain two items:
- Breaking changes: All breaking changes have to be mentioned in footer with the description of the change, justification and migration notes
- Referencing issues: Closed bugs should be listed on a separate line in the footer prefixed with "Closes" keyword like this: Closes #123, #456
<dependencies> if this PR depends on others, they should be listed
in checkbox format, i.e.,
- [ ] depends on: #XXXX
An example where
<scope> is not necessary might be:
feat: have library search use the whole range for replacement previously `apply? using h` would replace to `refine blah using h` rather than `refine blah`. This also changes the diagnostic message to be on the whole syntax `apply? using h` rather than just the `apply?` bit, which seems fine to me.
And an example where including
<scope> does add value:
docs(CategoryTheory/EssentialImage): typo and punctuation Fix a typo, add two periods.
an example with dependent PRs:
feat: The norm on `Unitization` is a C⋆-norm This shows that C⋆-algebras are always `RegularNormedAlgebra`s, so that their `Unitization` is equipped with a norm. Moreover, we show this norm is a C⋆-norm. - [ ] depends on: #5330 - [ ] depends on: #5741 - [ ] depends on: #5742 - [ ] depends on: #5743 ```