Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
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
2 changes: 1 addition & 1 deletion .github/workflows/monitor_runners.yml
Original file line number Diff line number Diff line change
Expand Up @@ -223,7 +223,7 @@ jobs:

# Check if this is a weekly report trigger
is_weekly_report="false"
if [ "${{ github.event.schedule }}" = "0 9 * * 1" ] || [ "${{ inputs.send_weekly_report }}" = "true" ]; then
if [ "${{ github.event.schedule }}" = "0 9 * * 1" ] || [ "${{ toJSON(inputs.send_weekly_report) }}" = "true" ]; then
is_weekly_report="true"
fi

Expand Down
8 changes: 7 additions & 1 deletion .github/workflows/random_issue.yml
Original file line number Diff line number Diff line change
Expand Up @@ -4,6 +4,12 @@ on:
schedule:
- cron: '0 14 * * *'
workflow_dispatch:
inputs:
send_zulip_message:
description: 'Send message to Zulip'
required: false
default: false
type: boolean

jobs:
post_issues:
Expand All @@ -25,7 +31,7 @@ jobs:
pip install PyGithub zulip

- name: Post issue on Zulip
run: python post_issue_on_zulip.py "${{ secrets.RANDOM_ISSUE_BOT_ZULIP_TOKEN }}" "${{ secrets.LCB_TOKEN }}"
run: python post_issue_on_zulip.py "${{ secrets.RANDOM_ISSUE_BOT_ZULIP_TOKEN }}" "${{ secrets.LCB_TOKEN }}" "${{ toJSON(github.event_name == 'schedule' || inputs.send_zulip_message) }}"

workflow-keepalive:
if: github.event_name == 'schedule'
Expand Down
42 changes: 27 additions & 15 deletions post_issue_on_zulip.py
Original file line number Diff line number Diff line change
Expand Up @@ -10,6 +10,7 @@

zulip_token = sys.argv[1]
gh_token = sys.argv[2]
should_send_to_zulip = sys.argv[3]

zulip_client = zulip.Client(email="random-issue-bot@zulipchat.com", api_key=zulip_token, site="https://leanprover.zulipchat.com")

Expand All @@ -30,25 +31,35 @@ def message_date(id):
gh = github.Github(login_or_token=gh_token)
mathlib = gh.get_repo('leanprover-community/mathlib4')

open_items = mathlib.get_issues(state='open')
open_prs = []
now = datetime.datetime.now(tz=datetime.timezone.utc)
delta = datetime.timedelta(days=7)
min_age = now - delta

open_issues_raw = mathlib.get_issues(state='open')
open_issues = []
open_prs_raw = mathlib.get_pulls(state='open')
open_prs = []

print(f'Found {open_items.totalCount} open item(s) (PRs and issues).')
print(f'Found {open_prs_raw.totalCount} open PR(s) and {open_issues_raw.totalCount} open issue(s).')

for i in open_items:
now = datetime.datetime.now(tz=datetime.timezone.utc)
delta = datetime.timedelta(days=7)
min_age = now - delta
if i.updated_at < min_age \
and 'blocked-by-other-PR' not in [l.name for l in i.labels] \
and not (i.number in posted_topics and datetime.datetime.fromtimestamp(posted_topics[i.number], tz=datetime.timezone.utc) > min_age):
if i.pull_request:
open_prs.append(i)
else:
open_issues.append(i)
# Process issues (need to filter out PRs since get_issues returns both)
for issue in open_issues_raw:
if not issue.pull_request: # Only process actual issues
if issue.updated_at < min_age \
and 'blocked-by-other-PR' not in [l.name for l in issue.labels] \
and not (issue.number in posted_topics and datetime.datetime.fromtimestamp(posted_topics[issue.number], tz=datetime.timezone.utc) > min_age):
open_issues.append(issue)

print(f'Found {len(open_issues)} open issue(s) after filtering.')

# Process PRs
for pr in open_prs_raw:
if pr.updated_at < min_age \
and 'blocked-by-other-PR' not in [l.name for l in pr.labels] \
and not (pr.number in posted_topics and datetime.datetime.fromtimestamp(posted_topics[pr.number], tz=datetime.timezone.utc) > min_age) \
and not pr.draft:
open_prs.append(pr)

print(f'Found {len(open_prs)} open PR(s) after filtering.')

def post_random(select_from, kind):
Expand Down Expand Up @@ -76,7 +87,8 @@ def post_random(select_from, kind):

print(content)

zulip_client.send_message(post)
if should_send_to_zulip != "false":
zulip_client.send_message(post)

post_random(open_issues, 'issue')
post_random(open_prs, 'PR')