chore: set up procedure for preparing release notes #4247
Merged
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
We are switching to a new system for preparing release notes. * Release notes will be compiled when creating a release candidate from all the commits that are part of that release. * PRs can include suggestions for release notes in PR messages. Please use language such as "release notes" and "breaking changes" to call attention to the suggestions. Release notes are user-centric rather than developer-centric. * For more complicated release notes, these can be put into the `releases_drafts` folder. This solves an issue where PRs that include release notes can, when merged, have those notes appear under the wrong Lean version, since they might have been created before a release but not merged until after. It also solves merge conflicts due to multiple PRs updating the release notes.
github-actions
bot
added
the
toolchain-available
|
Mathlib CI status (docs):
|
|
Where have the release notes for 4.8.0-rc2 gone? They aren't in the I think it is important to have release notes also for release candidates, as this is the first place to look for breaking changes when updating mathlib or a project depending on it. |
|
@digama0 They're in the release branch in RELEASES.md (that's the master copy for 4.8.0). I deleted them here because something went wrong with how they were merged into master, and I was going to copy them back in a future step. |
|
Oops, conflict to resolve. |
|
@semorrison I guess case-in-point for contention and weird merges! #3940 ended up somehow adding another v4.8.0 heading on |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
We are switching to a new system for preparing release notes.
releases_draftsfolder.This solves an issue where PRs that include release notes can, when merged, have those notes appear under the wrong Lean version, since they might have been created before a release but not merged until after. It also solves merge conflicts due to multiple PRs updating the release notes.