From 26e028756d558d03936563a6623427422a980634 Mon Sep 17 00:00:00 2001 From: Bryan Gin-ge Chen Date: Mon, 1 Sep 2025 07:49:19 -0400 Subject: [PATCH 1/5] fix(post_issue_on_zulip.py): filter out draft PRs The draft data is not included in the issues object, so we need to make another request for PR objects. --- post_issue_on_zulip.py | 38 ++++++++++++++++++++++++-------------- 1 file changed, 24 insertions(+), 14 deletions(-) diff --git a/post_issue_on_zulip.py b/post_issue_on_zulip.py index 3e48fb1..e46f468 100644 --- a/post_issue_on_zulip.py +++ b/post_issue_on_zulip.py @@ -30,25 +30,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): From 455c151b6d6e33bb89c758d9e74ce62fbeeee586 Mon Sep 17 00:00:00 2001 From: Bryan Gin-ge Chen Date: Mon, 1 Sep 2025 07:56:32 -0400 Subject: [PATCH 2/5] Update random_issue.yml --- .github/workflows/random_issue.yml | 8 +++++++- 1 file changed, 7 insertions(+), 1 deletion(-) diff --git a/.github/workflows/random_issue.yml b/.github/workflows/random_issue.yml index 6ac83bc..4b9d0bc 100644 --- a/.github/workflows/random_issue.yml +++ b/.github/workflows/random_issue.yml @@ -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: @@ -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(inputs.send_zulip_message) }}" workflow-keepalive: if: github.event_name == 'schedule' From 9d927458a3d3fa64cd8146439f39b68e0afd415a Mon Sep 17 00:00:00 2001 From: Bryan Gin-ge Chen Date: Mon, 1 Sep 2025 07:57:20 -0400 Subject: [PATCH 3/5] Update monitor_runners.yml --- .github/workflows/monitor_runners.yml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.github/workflows/monitor_runners.yml b/.github/workflows/monitor_runners.yml index f37962f..f8a9cba 100644 --- a/.github/workflows/monitor_runners.yml +++ b/.github/workflows/monitor_runners.yml @@ -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 From 16bf4b9ec0c809c287927fe87331ba6ba5d6d418 Mon Sep 17 00:00:00 2001 From: Bryan Gin-ge Chen Date: Mon, 1 Sep 2025 08:03:42 -0400 Subject: [PATCH 4/5] Update post_issue_on_zulip.py --- post_issue_on_zulip.py | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/post_issue_on_zulip.py b/post_issue_on_zulip.py index e46f468..7a67aec 100644 --- a/post_issue_on_zulip.py +++ b/post_issue_on_zulip.py @@ -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") @@ -86,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') From a40664fa2ebf78525dd2cb7158f9736385cb417b Mon Sep 17 00:00:00 2001 From: Bryan Gin-ge Chen Date: Mon, 1 Sep 2025 08:04:41 -0400 Subject: [PATCH 5/5] Update random_issue.yml --- .github/workflows/random_issue.yml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.github/workflows/random_issue.yml b/.github/workflows/random_issue.yml index 4b9d0bc..a935329 100644 --- a/.github/workflows/random_issue.yml +++ b/.github/workflows/random_issue.yml @@ -31,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 }}" "${{ toJSON(inputs.send_zulip_message) }}" + 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'