From 7610983e215b9ffe0a265eb2a25eaa2c58183ca7 Mon Sep 17 00:00:00 2001 From: adomani Date: Thu, 21 Nov 2024 09:46:51 +0000 Subject: [PATCH 01/12] remove zulip_emoji workflow, as it fails with an email --- .../workflows/zulip_emoji_merge_delegate.yaml | 35 ------------------- 1 file changed, 35 deletions(-) delete mode 100644 .github/workflows/zulip_emoji_merge_delegate.yaml diff --git a/.github/workflows/zulip_emoji_merge_delegate.yaml b/.github/workflows/zulip_emoji_merge_delegate.yaml deleted file mode 100644 index e44b4d07004d98..00000000000000 --- a/.github/workflows/zulip_emoji_merge_delegate.yaml +++ /dev/null @@ -1,35 +0,0 @@ -name: Zulip Emoji Merge Delegate - -on: - schedule: - - cron: '0 * * * *' # Runs every hour - -jobs: - zulip-emoji-merge-delegate: - runs-on: ubuntu-latest - - steps: - - name: Checkout mathlib repository - uses: actions/checkout@v4 - with: - sparse-checkout: | - scripts - - - name: Set up Python - uses: actions/setup-python@v5 - with: - python-version: '3.x' - - - name: Install dependencies - run: | - python -m pip install --upgrade pip - pip install zulip - - - name: Run Zulip Emoji Merge Delegate Script - env: - ZULIP_API_KEY: ${{ secrets.ZULIP_API_KEY }} - ZULIP_EMAIL: github-mathlib4-bot@leanprover.zulipchat.com - ZULIP_SITE: https://leanprover.zulipchat.com - GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }} - run: | - python scripts/zulip_emoji_merge_delegate.py "$ZULIP_API_KEY" "$ZULIP_EMAIL" "$ZULIP_SITE" "$GITHUB_TOKEN" From dda3fa2c603760031d9a76931aedb4aea2f9ea1c Mon Sep 17 00:00:00 2001 From: adomani Date: Thu, 21 Nov 2024 09:48:34 +0000 Subject: [PATCH 02/12] feat: add `first bench is free` workflow --- .github/workflows/first_bench_is_free.yml | 20 ++++++++++++++++++++ 1 file changed, 20 insertions(+) create mode 100644 .github/workflows/first_bench_is_free.yml diff --git a/.github/workflows/first_bench_is_free.yml b/.github/workflows/first_bench_is_free.yml new file mode 100644 index 00000000000000..4104b6ea543872 --- /dev/null +++ b/.github/workflows/first_bench_is_free.yml @@ -0,0 +1,20 @@ +name: Auto-bench + +on: + pull_request: + types: [opened] # This triggers the action when the PR is opened. + +jobs: + automatic_first_bench: + runs-on: ubuntu-latest + + steps: + - name: Add comment to PR + uses: GrantBirki/comment@v2 + with: + github-token: ${{ secrets.GITHUB_TOKEN }} + issue-number: ${{ github.event.pull_request.number }} + body: | + ! **mangled** bench + + This is an automated bench-marking that runs when a PR is opened. No need to repeat. From 88fc797cfa7059d00b8c5579e60cbaf288d26f91 Mon Sep 17 00:00:00 2001 From: adomani Date: Thu, 21 Nov 2024 10:36:35 +0000 Subject: [PATCH 03/12] run always --- .github/workflows/first_bench_is_free.yml | 15 ++++++++++----- 1 file changed, 10 insertions(+), 5 deletions(-) diff --git a/.github/workflows/first_bench_is_free.yml b/.github/workflows/first_bench_is_free.yml index 4104b6ea543872..17677343a65fd6 100644 --- a/.github/workflows/first_bench_is_free.yml +++ b/.github/workflows/first_bench_is_free.yml @@ -2,19 +2,24 @@ name: Auto-bench on: pull_request: - types: [opened] # This triggers the action when the PR is opened. + #types: [opened] # This triggers the action when the PR is opened. jobs: automatic_first_bench: runs-on: ubuntu-latest steps: + + - name: Produce bench message + id: bench_message + run: | + message='! **mangled** bench\n\nThis is an automated bench-marking that runs when a PR is opened. No need to repeat.\n' + printf '%s' "${message}" | hexdump -cC + printf 'message<> "${GITHUB_OUTPUT}" + - name: Add comment to PR uses: GrantBirki/comment@v2 with: github-token: ${{ secrets.GITHUB_TOKEN }} issue-number: ${{ github.event.pull_request.number }} - body: | - ! **mangled** bench - - This is an automated bench-marking that runs when a PR is opened. No need to repeat. + body: ${{ steps.bench_message.outputs.message }} From efee344864cebab6a03694f74753de5dbe6b5714 Mon Sep 17 00:00:00 2001 From: adomani Date: Thu, 21 Nov 2024 10:38:19 +0000 Subject: [PATCH 04/12] better quoting --- .github/workflows/first_bench_is_free.yml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.github/workflows/first_bench_is_free.yml b/.github/workflows/first_bench_is_free.yml index 17677343a65fd6..bc236e8c673329 100644 --- a/.github/workflows/first_bench_is_free.yml +++ b/.github/workflows/first_bench_is_free.yml @@ -13,7 +13,7 @@ jobs: - name: Produce bench message id: bench_message run: | - message='! **mangled** bench\n\nThis is an automated bench-marking that runs when a PR is opened. No need to repeat.\n' + message=$'!bench\n\nThis is an automated bench-marking that runs when a PR is opened. No need to repeat.\n' printf '%s' "${message}" | hexdump -cC printf 'message<> "${GITHUB_OUTPUT}" From e148e6e37549f0266429aa4603462902e624721c Mon Sep 17 00:00:00 2001 From: adomani Date: Mon, 25 Nov 2024 20:49:01 +0000 Subject: [PATCH 05/12] add zulip emoji script --- .github/workflows/zulip_api.yml | 77 ++++++++++++++++++++++++ zulip_emoji_merge_delegate.py | 101 ++++++++++++++++++++++++++++++++ 2 files changed, 178 insertions(+) create mode 100644 .github/workflows/zulip_api.yml create mode 100644 zulip_emoji_merge_delegate.py diff --git a/.github/workflows/zulip_api.yml b/.github/workflows/zulip_api.yml new file mode 100644 index 00000000000000..a9eb769e04b85b --- /dev/null +++ b/.github/workflows/zulip_api.yml @@ -0,0 +1,77 @@ +name: Add "ready-to-merge" and "delegated" label + +# triggers the action when +on: + push: + # the PR receives a comment + issue_comment: + types: [created] + # the PR receives a review + pull_request_review: + # whether or not it is accompanied by a comment + types: [submitted] + # the PR receives a review comment + pull_request_review_comment: + types: [created] + +jobs: + add_ready_to_merge_label: + # we set some variables. The ones of the form `${{ X }}${{ Y }}` are typically not + # both set simultaneously: depending on the event that triggers the PR, usually only one is set + env: + AUTHOR: ${{ github.event.comment.user.login }}${{ github.event.review.user.login }} + COMMENT_EVENT: ${{ github.event.comment.body }} + COMMENT_REVIEW: ${{ github.event.review.body }} + name: Add ready-to-merge or delegated label + runs-on: ubuntu-latest + steps: + - name: Find bors merge/delegate + id: merge_or_delegate + run: | + COMMENT="${COMMENT_EVENT}${COMMENT_REVIEW}" + # we strip `\r` since line endings from GitHub contain this character + COMMENT="${COMMENT//$'\r'/}" + # for debugging, we print some information + printf '%s' "${COMMENT}" | hexdump -cC + printf 'Comment:"%s"\n' "${COMMENT}" + m_or_d="$(printf '%s' "${COMMENT}" | + sed -n 's=^bors *\(merge\|r+\) *$=ready-to-merge=p; s=^bors *d.*=delegated=p' | head -1)" + + printf $'"bors delegate" or "bors merge" found? \'%s\'\n' "${m_or_d}" + printf $'AUTHOR: \'%s\'\n' "${AUTHOR}" + printf $'PR_NUMBER: \'%s\'\n' "${{ github.event.issue.number }}${{ github.event.pull_request.number }}" + printf $'%s' "${{ github.event.issue.number }}${{ github.event.pull_request.number }}" | hexdump -cC + + printf $'mOrD=%s\n' "${m_or_d}" >> "${GITHUB_OUTPUT}" + if [ "${AUTHOR}" == 'leanprover-community-mathlib4-bot' ] || + [ "${AUTHOR}" == 'leanprover-community-bot-assistant' ] + then + printf $'bot=true\n' + printf $'bot=true\n' >> "${GITHUB_OUTPUT}" + else + printf $'bot=false\n' + printf $'bot=false\n' >> "${GITHUB_OUTPUT}" + fi + + - name: Set up Python + uses: actions/setup-python@v5 + with: + python-version: '3.x' + + - name: Install dependencies + run: | + python -m pip install --upgrade pip + pip install zulip + + - uses: actions/checkout@v4 + with: + sparse-checkout: | + scripts/zulip_emoji_merge_delegate.py + + - name: Run Zulip Emoji Merge Delegate Script + env: + ZULIP_API_KEY: ${{ secrets.ZULIP_API_KEY }} + ZULIP_EMAIL: github-mathlib4-bot@leanprover.zulipchat.com + ZULIP_SITE: https://leanprover.zulipchat.com + run: | + python scripts/zulip_emoji_merge_delegate.py "$ZULIP_API_KEY" "$ZULIP_EMAIL" "$ZULIP_SITE" "${{ steps.merge_or_delegate.outputs.mOrD }}" "${{ github.event.issue.number }}${{ github.event.pull_request.number }}" diff --git a/zulip_emoji_merge_delegate.py b/zulip_emoji_merge_delegate.py new file mode 100644 index 00000000000000..7e16fa43f1d3c4 --- /dev/null +++ b/zulip_emoji_merge_delegate.py @@ -0,0 +1,101 @@ +#!/usr/bin/env python3 +import sys +import zulip +import re + +# Usage: +# python scripts/zulip_emoji_merge_delegate.py $ZULIP_API_KEY $ZULIP_EMAIL $ZULIP_SITE $LABEL $PR_NUMBER +# See .github/workflows/zulip_emoji_merge_delegate.yaml for the meaning of these variables + +ZULIP_API_KEY = sys.argv[1] +ZULIP_EMAIL = sys.argv[2] +ZULIP_SITE = sys.argv[3] +LABEL = sys.argv[4] +PR_NUMBER = sys.argv[5] + +print(f"LABEL: '{LABEL}'") +print(f"PR_NUMBER: '{PR_NUMBER}'") + +# Initialize Zulip client +client = zulip.Client( + email=ZULIP_EMAIL, + api_key=ZULIP_API_KEY, + site=ZULIP_SITE +) + +# Fetch the last 200 messages +response = client.get_messages({ + "operator": "search", + "operand": f"https://github\.com/leanprover-community/mathlib4/pull/{PR_NUMBER}", +}) + +print(f"response: {response}") + +''' +messages = response['messages'] +for message in messages: + content = message['content'] + print(f"matched: '{message}'") + # Check for emoji reactions + reactions = message['reactions'] + has_peace_sign = any(reaction['emoji_name'] == 'peace_sign' for reaction in reactions) + has_bors = any(reaction['emoji_name'] == 'bors' for reaction in reactions) + has_merge = any(reaction['emoji_name'] == 'merge' for reaction in reactions) + + pr_url = f"https://api.github.com/repos/leanprover-community/mathlib4/pulls/{PR_NUMBER}" + + print('Removing peace_sign') + result = client.remove_reaction({ + "message_id": message['id'], + "emoji_name": "peace_sign" + }) + print(f"result: '{result}'") + print('Removing bors') + result = client.remove_reaction({ + "message_id": message['id'], + "emoji_name": "bors" + }) + print(f"result: '{result}'") + + print('Removing merge') + result = client.remove_reaction({ + "message_id": message['id'], + "emoji_name": "merge" + }) + print(f"result: '{result}'") + + if 'delegated' == LABEL: + print('adding delegated') + + client.add_reaction({ + "message_id": message['id'], + "emoji_name": "peace_sign" + }) + elif 'ready-to-merge' == LABEL: + print('adding ready-to-merge') + if has_peace_sign: + client.remove_reaction({ + "message_id": message['id'], + "emoji_name": "peace_sign" + }) + client.add_reaction({ + "message_id": message['id'], + "emoji_name": "bors" + }) + elif LABEL.startswith("[Merged by Bors]"): + print('adding [Merged by Bors]') + if has_peace_sign: + client.remove_reaction({ + "message_id": message['id'], + "emoji_name": "peace_sign" + }) + if has_bors: + client.remove_reaction({ + "message_id": message['id'], + "emoji_name": "bors" + }) + client.add_reaction({ + "message_id": message['id'], + "emoji_name": "merge" + }) +''' From 72ca6daa715e9e7a7c3403ab98595f06dc855246 Mon Sep 17 00:00:00 2001 From: adomani Date: Mon, 25 Nov 2024 20:54:50 +0000 Subject: [PATCH 06/12] do no messages --- zulip_emoji_merge_delegate.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/zulip_emoji_merge_delegate.py b/zulip_emoji_merge_delegate.py index 7e16fa43f1d3c4..4d5582e226f67d 100644 --- a/zulip_emoji_merge_delegate.py +++ b/zulip_emoji_merge_delegate.py @@ -32,7 +32,7 @@ print(f"response: {response}") ''' -messages = response['messages'] +# messages = response['messages'] for message in messages: content = message['content'] print(f"matched: '{message}'") From 9b43781aacef343972a1327892c82963b45719ed Mon Sep 17 00:00:00 2001 From: adomani Date: Mon, 25 Nov 2024 20:58:56 +0000 Subject: [PATCH 07/12] cat script --- .github/workflows/zulip_api.yml | 1 + 1 file changed, 1 insertion(+) diff --git a/.github/workflows/zulip_api.yml b/.github/workflows/zulip_api.yml index a9eb769e04b85b..8db49cfb2ffb0e 100644 --- a/.github/workflows/zulip_api.yml +++ b/.github/workflows/zulip_api.yml @@ -74,4 +74,5 @@ jobs: ZULIP_EMAIL: github-mathlib4-bot@leanprover.zulipchat.com ZULIP_SITE: https://leanprover.zulipchat.com run: | + cat scripts/zulip_emoji_merge_delegate.py python scripts/zulip_emoji_merge_delegate.py "$ZULIP_API_KEY" "$ZULIP_EMAIL" "$ZULIP_SITE" "${{ steps.merge_or_delegate.outputs.mOrD }}" "${{ github.event.issue.number }}${{ github.event.pull_request.number }}" From 7376e586127ce508a40ba49d9b470d8e2a482aa9 Mon Sep 17 00:00:00 2001 From: adomani Date: Mon, 25 Nov 2024 21:00:27 +0000 Subject: [PATCH 08/12] checkout --- .github/workflows/zulip_api.yml | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/.github/workflows/zulip_api.yml b/.github/workflows/zulip_api.yml index 8db49cfb2ffb0e..dc570a14e03fb3 100644 --- a/.github/workflows/zulip_api.yml +++ b/.github/workflows/zulip_api.yml @@ -64,9 +64,9 @@ jobs: pip install zulip - uses: actions/checkout@v4 - with: - sparse-checkout: | - scripts/zulip_emoji_merge_delegate.py + #with: + # sparse-checkout: | + # scripts/zulip_emoji_merge_delegate.py - name: Run Zulip Emoji Merge Delegate Script env: From be8ac995e72747f4816c1100a69ad9b197bc5d18 Mon Sep 17 00:00:00 2001 From: adomani Date: Mon, 25 Nov 2024 21:05:39 +0000 Subject: [PATCH 09/12] cat boundaries --- .github/workflows/zulip_api.yml | 2 ++ 1 file changed, 2 insertions(+) diff --git a/.github/workflows/zulip_api.yml b/.github/workflows/zulip_api.yml index dc570a14e03fb3..85e7bded6ad646 100644 --- a/.github/workflows/zulip_api.yml +++ b/.github/workflows/zulip_api.yml @@ -74,5 +74,7 @@ jobs: ZULIP_EMAIL: github-mathlib4-bot@leanprover.zulipchat.com ZULIP_SITE: https://leanprover.zulipchat.com run: | + printf 'cat scripts/zulip_emoji_merge_delegate.py\n' cat scripts/zulip_emoji_merge_delegate.py + printf 'catted\n\n' python scripts/zulip_emoji_merge_delegate.py "$ZULIP_API_KEY" "$ZULIP_EMAIL" "$ZULIP_SITE" "${{ steps.merge_or_delegate.outputs.mOrD }}" "${{ github.event.issue.number }}${{ github.event.pull_request.number }}" From 79e3a814d6c2f2911675d5f8786ddc15e78c12c0 Mon Sep 17 00:00:00 2001 From: adomani Date: Mon, 25 Nov 2024 21:07:59 +0000 Subject: [PATCH 10/12] master ref --- .github/workflows/zulip_api.yml | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/.github/workflows/zulip_api.yml b/.github/workflows/zulip_api.yml index 85e7bded6ad646..ac37146967361a 100644 --- a/.github/workflows/zulip_api.yml +++ b/.github/workflows/zulip_api.yml @@ -64,7 +64,8 @@ jobs: pip install zulip - uses: actions/checkout@v4 - #with: + with: + ref: master # sparse-checkout: | # scripts/zulip_emoji_merge_delegate.py From 3b1fbb8f1523419e7bc83e99e7dd8f5f9ca480cc Mon Sep 17 00:00:00 2001 From: adomani Date: Mon, 25 Nov 2024 21:11:46 +0000 Subject: [PATCH 11/12] clean up more --- .github/workflows/zulip_api.yml | 27 --------------------------- 1 file changed, 27 deletions(-) diff --git a/.github/workflows/zulip_api.yml b/.github/workflows/zulip_api.yml index ac37146967361a..9fb6c45c37a634 100644 --- a/.github/workflows/zulip_api.yml +++ b/.github/workflows/zulip_api.yml @@ -25,33 +25,6 @@ jobs: name: Add ready-to-merge or delegated label runs-on: ubuntu-latest steps: - - name: Find bors merge/delegate - id: merge_or_delegate - run: | - COMMENT="${COMMENT_EVENT}${COMMENT_REVIEW}" - # we strip `\r` since line endings from GitHub contain this character - COMMENT="${COMMENT//$'\r'/}" - # for debugging, we print some information - printf '%s' "${COMMENT}" | hexdump -cC - printf 'Comment:"%s"\n' "${COMMENT}" - m_or_d="$(printf '%s' "${COMMENT}" | - sed -n 's=^bors *\(merge\|r+\) *$=ready-to-merge=p; s=^bors *d.*=delegated=p' | head -1)" - - printf $'"bors delegate" or "bors merge" found? \'%s\'\n' "${m_or_d}" - printf $'AUTHOR: \'%s\'\n' "${AUTHOR}" - printf $'PR_NUMBER: \'%s\'\n' "${{ github.event.issue.number }}${{ github.event.pull_request.number }}" - printf $'%s' "${{ github.event.issue.number }}${{ github.event.pull_request.number }}" | hexdump -cC - - printf $'mOrD=%s\n' "${m_or_d}" >> "${GITHUB_OUTPUT}" - if [ "${AUTHOR}" == 'leanprover-community-mathlib4-bot' ] || - [ "${AUTHOR}" == 'leanprover-community-bot-assistant' ] - then - printf $'bot=true\n' - printf $'bot=true\n' >> "${GITHUB_OUTPUT}" - else - printf $'bot=false\n' - printf $'bot=false\n' >> "${GITHUB_OUTPUT}" - fi - name: Set up Python uses: actions/setup-python@v5 From 8d2922e09b4cf28184375d47cb95a7f85616c86b Mon Sep 17 00:00:00 2001 From: adomani Date: Mon, 25 Nov 2024 21:12:36 +0000 Subject: [PATCH 12/12] add a new file --- Mathlib/New.lean | 1 + 1 file changed, 1 insertion(+) create mode 100644 Mathlib/New.lean diff --git a/Mathlib/New.lean b/Mathlib/New.lean new file mode 100644 index 00000000000000..4ba280517af592 --- /dev/null +++ b/Mathlib/New.lean @@ -0,0 +1 @@ +--