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.
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
[Merged by Bors] - ci(.github/workflows/dependent-issues.yml): automation for "blocked-by-other-PR" label #5261
Conversation
…y-other-PR" label
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
LGTM, thanks for experimenting with this!
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Thanks for looking into this! Just clarification questions.
- reopened | ||
- synchronize | ||
schedule: | ||
- cron: '15 * * * *' # schedule hourly check for external dependencies |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
What's the scenario where this is needed?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
One of our PRs might depend on a issue / PR in an external repo (e.g. community Lean) so this will make sure those are checked once an hour. I was hoping the comment would make this clear, so let me know if you can think of a way to improve it.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Ah, I just realized that this also manages the PRs which were opened before this was merged.
name: Dependent Issues | ||
|
||
on: | ||
issues: |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
issues
includes pull requests, right? Since we disable check_issues
below, is it enough to just have pull_request_target
? Or alternatively do we need pull_request_target
if issues
includes PRs? I'm not clear on the details here. Do we need to watch issues in case a PR depends on an issue?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Yeah, we have to watch issues in case a PR depends on an issue.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
This part of the workflow file is just copied from the example in the dependent-issues README, so I'm trusting that these triggers are the correct / minimal ones.
Let's go ahead and try it out then! bors merge |
…y-other-PR" label (#5261) When a PR or issue is updated, the [dependent-issues](https://github.com/z0al/dependent-issues) action will do the following on all PRs which are marked as dependent on it (with the text `- [ ] depends on: #blah` that we're already using): - add / remove the "blocked-by-other-PR" label - post / edit a comment with the current status of its dependencies (this is slightly redundant, given that we have another action which checks off the dependent PRs in the PR comments, but the extra notifications might be useful). - it also adds a new status check which is pending (yellow) until all dependencies are closed.
Pull request successfully merged into master. Build succeeded: |
When a PR or issue is updated, the dependent-issues action will do the following on all PRs which are marked as dependent on it (with the text
- [ ] depends on: #blah
that we're already using):I did some testing in my mathlib fork. If you want to play around with it there, ping me and I can give you edit access.