Skip to content

Update commit message guidelines in contribute.md #753

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.

Sign up for GitHub

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

Open
marwahaha wants to merge 1 commit into
base: lean4
Choose a base branch
from
Open

Update commit message guidelines in contribute.md #753

Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
19 changes: 13 additions & 6 deletions templates/contribute/commit.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -4,18 +4,19 @@ We are using the following convention for writing pull request titles and descri

## Format

Note: "Title:" and "Description:" do not actually appear

The title of the PR will be the title of the commit after the PR is merged. It should have the following format:
```markdown
Title:
<type>(<optional-scope>): <subject>
```

Description:
The description of the PR, before the `---`, will be the description of the commit after the PR is merged. It should have the following format:
```markdown
<body>
<NEWLINE>
<footer>
<NEWLINE>
<dependencies>
---
<anything else, including dependencies>
```

`<type>` is:
Expand Down Expand Up @@ -68,7 +69,9 @@ An example where `<scope>` is not necessary might be:

```markdown
feat: have library search use the whole range for replacement
```

```markdown
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.
Expand All @@ -78,15 +81,19 @@ And an example where including `<scope>` does add value:

```markdown
docs(CategoryTheory/EssentialImage): typo and punctuation
```

```markdown
Fix a typo, add two periods.
```

An example with dependent PRs:
An example with dependent PRs. These will not be in the commit message description.

```markdown
feat: The norm on `Unitization` is a C⋆-norm
```

```markdown
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.

---
Expand Down