max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

doc: expand PR creation guidelines in CLAUDE.md (#11835)

Browse source 
This PR expands the pull request creation section with detailed
formatting guidelines including title format (type prefixes, imperative
present tense) and body format requirements (starting with "This PR").
Adds a concrete example for reference.

All modifications were suggested by Claude.
This commit is contained in:
Leonardo de Moura 2025-12-29 09:42:28 -08:00 • committed by GitHub
parent 4e1a2487b7
commit f77ce8c669
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 15 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

17
.claude/CLAUDE.md
View file

@ -29,6 +29,19 @@ After rebuilding, LSP diagnostics may be stale until the user interacts with fil
If the user expresses frustration with you, stop and ask them to help update this `.claude/CLAUDE.md` file with missing guidance.
## Creating pull requests.
## Creating pull requests
All PRs must have a first paragraph starting with "This PR". This paragraph is automatically incorporated into release notes. Read `lean4/doc/dev/commit_convention.md` when making PRs.
Follow the commit convention in `doc/dev/commit_convention.md`.
**Title format:** `<type>: <subject>` where type is one of: `feat`, `fix`, `doc`, `style`, `refactor`, `test`, `chore`, `perf`.
Subject should use imperative present tense ("add" not "added"), no capitalization, no trailing period.
**Body format:** The first paragraph must start with "This PR". This paragraph is automatically incorporated into release notes. Use imperative present tense. Include motivation and contrast with previous behavior when relevant.
Example:
```
feat: add optional binder limit to `mkPatternFromTheorem`
This PR adds a `num?` parameter to `mkPatternFromTheorem` to control how many
leading quantifiers are stripped when creating a pattern.
```