Skip to content
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

Jump to bottom

feat(CI): check for badly formatted titles or missing/contradictory labels #16303

Open
wants to merge 7 commits into
base: master
Choose a base branch
from
Open

feat(CI): check for badly formatted titles or missing/contradictory labels #16303

wants to merge 7 commits into from
+321 −0

Conversation

grunweg
Copy link
Collaborator

@grunweg grunweg commented Aug 30, 2024 •
edited
Loading

The zulip workflow is entirely cargo-culted from #16296; please review carefully.

Open in Gitpod

@grunweg grunweg added WIP Work in progress CI Modifies the continuous integration / deployment setup labels Aug 30, 2024
@github-actions GitHub Actions
Copy link

github-actions bot commented Aug 30, 2024 •
edited
Loading

PR summary f18acca564

Import changes for modified files

No significant changes to the import graph

Import changes for all files
Files Import difference

Declarations diff

+ checkTitleLabels
+ checkTitleLabelsCLI
+ hasContradictoryLabels
+ main
+ splitAtPos
+ validateTitle

You can run this locally as follows 
## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for script/declarations_diff.sh contains some details about this script.

grunweg added a commit that referenced this pull request Aug 30, 2024
@grunweg
Cargo-cult fix from #16303
567eeb3
@grunweg
Copy link
Collaborator Author

grunweg commented Aug 30, 2024

Thanks again!

joneugster
joneugster reviewed Aug 30, 2024
View reviewed changes
scripts/check-title-labels.lean Outdated Show resolved Hide resolved
scripts/check-title-labels.lean Show resolved Hide resolved
scripts/check-title-labels.lean Outdated Show resolved Hide resolved
scripts/check-title-labels.lean Outdated Show resolved Hide resolved
scripts/check-title-labels.lean Outdated Show resolved Hide resolved
scripts/check-title-labels.lean Outdated Show resolved Hide resolved
scripts/check-title-labels.lean Outdated Show resolved Hide resolved
.github/workflows/build.yml.in Outdated Show resolved Hide resolved
@leanprover-community-bot-assistant leanprover-community-bot-assistant added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Sep 3, 2024
@grunweg grunweg changed the title feat(CI): check for badly formatting titles or missing/contradictory labels feat(CI): check for badly formatted titles or missing/contradictory labels Oct 8, 2024
@grunweg grunweg removed WIP Work in progress merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) labels Oct 8, 2024
grunweg
grunweg commented Oct 8, 2024
View reviewed changes
Copy link
Collaborator Author

@grunweg grunweg left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Thanks for your careful review! I just revamped the logic, which should be much more robust now.

scripts/check-title-labels.lean Show resolved Hide resolved
scripts/check-title-labels.lean Outdated Show resolved Hide resolved
bryangingechen
bryangingechen reviewed Oct 9, 2024
View reviewed changes
scripts/check-title-labels.lean Outdated Show resolved Hide resolved
.github/build.in.yml Outdated Show resolved Hide resolved
@bryangingechen bryangingechen self-assigned this Oct 9, 2024
@bryangingechen bryangingechen added awaiting-author A reviewer has asked the author a question or requested changes awaiting-CI labels Oct 9, 2024
@grunweg grunweg mentioned this pull request Oct 11, 2024
Open
grunweg and others added 6 commits October 11, 2024 17:24
@grunweg
feat: add a script to check for PR title and labelling
4a05ec2 
The script checks most items from the commit convention,
ensures that a feature PR has a topic/area label,
and errors if any two labels are contradictory.

Add detailed tests for the title validation.
@grunweg
wip: add ci workflow; untested yet
b186595
@grunweg @bryangingechen
Update .github/workflows/build.yml.in
da95e15 
Co-authored-by: Bryan Gin-ge Chen <[email protected]>
@grunweg
Synchronise workflows
74d4e99
@grunweg @joneugster
Skip if the PR is in draft stage
4206441 
Co-authored-by: Jon Eugster <[email protected]>
@grunweg
Does this help?
22998e8
@grunweg @github-actions
Synchronise
f18acca 
Co-authored-by: github-actions[bot] <41898282+github-actions[bot]@users.noreply.github.com>
@grunweg
Copy link
Collaborator Author

grunweg commented Oct 11, 2024

CI looks green now: I don't mind if this is reviewed together with #17649 or separately.

@grunweg grunweg removed the awaiting-author A reviewer has asked the author a question or requested changes label Oct 11, 2024
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@bryangingechen bryangingechen bryangingechen left review comments

@joneugster joneugster joneugster left review comments

Assignees

@bryangingechen bryangingechen

Labels
CI Modifies the continuous integration / deployment setup
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
4 participants
@grunweg @bryangingechen @joneugster @leanprover-community-bot-assistant