[Merged by Bors] - feat(CI): Zulip `:closed-pr:` emoji reaction #20902

adomani · 2025-01-21T08:42:39Z

Add a workflow that is triggered by closing a PR. If the PR does title not start with [Merged by Bors], then the script adds the :closed-pr: emoji reaction to messages on Zulip that link to the PR number.

github-actions · 2025-01-21T08:43:33Z

PR summary b44c5dbddb

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

Declarations diff

No declarations were harmed in the making of this PR! 🐙

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.

No changes to technical debt.

You can run this locally as

./scripts/technical-debt-metrics.sh pr_summary

The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

grunweg

Looks plausible at first side. The python changes LGTM (assuming one of them is just a type). I'd need to look at the workflow more closely and compare it to the others.

scripts/zulip_emoji_merge_delegate.py

grunweg

I took a look. Looks good in general; I think this can land soon.
I suspect there may be one or two bugs, but these should be easy to fix. (Did you test this locally? Or is the only way to test this to run it in production?)

Finally, I wonder if this does what we want.
Currently, this workflow only runs on closed PRs that were merged by bors. This means

it won't apply to PRs which are closed (because the PR is superseded, or not suitable for mathlib, or some other reasons) but unmerged
it does not run on merged PRs (these also exist, e.g. mathlib adaptation PRs, or somebody updating their personal fork). I think those PRs could also be nice to handle...

What do you think?
In any case: can you please document the intended behaviour in the workflow, say with a comment on top? Having merged PRs be "closed", not "merged", is a mathlib peculiarity: this might not be obvious for the readers of this file.

grunweg · 2025-01-21T13:02:07Z

.github/workflows/zulip_emoji_closed_pr.yaml

+          ZULIP_EMAIL: [email protected]
+          ZULIP_SITE: https://leanprover.zulipchat.com
+        run: |
+          python scripts/zulip_emoji_merge_delegate.py "$ZULIP_API_KEY" "$ZULIP_EMAIL" "$ZULIP_SITE" "closed" "${{ github.event.issue.number }}${{ github.event.pull_request.number }}"


Should this be the following?

Suggested change

python scripts/zulip_emoji_merge_delegate.py "$ZULIP_API_KEY" "$ZULIP_EMAIL" "$ZULIP_SITE" "closed" "${{ github.event.issue.number }}${{ github.event.pull_request.number }}"

python scripts/zulip_emoji_merge_delegate.py "$ZULIP_API_KEY" "$ZULIP_EMAIL" "$ZULIP_SITE" "closed" "${{ github.event.issue.number }}" "${{ github.event.pull_request.number }}"

I think that this is correct as is: at most one is defined, probably github.event.pull_request.number, but I won't know for sure until this gets tested and the previous CI step tells me what the numbers are! 😄

Fine. Can you either add a comment or follow up with a PR deleting the wrong one?

I was planning to follow up with PRs fixing this mistake (and the other ones that are likely present! 😄 )

Sure, works for me :-)

.github/workflows/zulip_emoji_closed_pr.yaml

adomani · 2025-01-21T13:32:23Z

Testing locally is hard, since GitHub will run this script only once it is in master. The idea is that we try our best, test it as soon as it enters mathlib and then fix the issues quickly! Since closing un-merged PRs is not common and the consequence of the script malfunctioning are adding a weird zulip reaction, there is not much at stake!

adomani · 2025-01-21T13:34:33Z

I took a look. Looks good in general; I think this can land soon. I suspect there may be one
Finally, I wonder if this does what we want. Currently, this workflow only runs on closed PRs that were merged by bors. This means

Why do you say that? I think that this will run on all closed PRs, regardless of who closed them. The ones that get closed by bors will have been renamed to [Merged by Bors] and a step of the script checks whether this is the case and ignores PRs that are closed and have title starting with [Merged by Bors].

The remaining PRs will likely

have been closed by a human,
have not been merged,
receive a reaction on Zulip!

grunweg · 2025-01-21T13:47:30Z

Indeed, I was tired and overlooked the negation 🤦‍♂️ Right, so this labels all closed PRs that have not been labelled by bors. This makes sense.

grunweg · 2025-01-21T13:59:11Z

The new changes look good. I'm still not sure about the cone option, but we can totally YOLO-deploy it and merge this PR. We need to test it live anyway.
maintainer merge

github-actions · 2025-01-21T13:59:33Z

🚀 Pull request has been placed on the maintainer queue by grunweg.

github-actions · 2025-01-21T13:59:46Z

🚀 Pull request has been placed on the maintainer queue by grunweg.

jcommelin · 2025-01-21T20:35:16Z

Thanks 🎉

bors merge

Add a workflow that is triggered by closing a PR. If the PR does title not start with `[Merged by Bors]`, then the script adds the `:closed-pr:` emoji reaction to messages on Zulip that link to the PR number.

mathlib-bors · 2025-01-21T20:43:50Z

Pull request successfully merged into master.

Build succeeded:

feat(CI): Zulip closed-pr emoji reaction

07e5673

github-actions bot added the CI Modifies the continuous integration / deployment setup label Jan 21, 2025

adomani added awaiting-author A reviewer has asked the author a question or requested changes and removed awaiting-author A reviewer has asked the author a question or requested changes labels Jan 21, 2025

grunweg reviewed Jan 21, 2025

View reviewed changes

scripts/zulip_emoji_merge_delegate.py Outdated Show resolved Hide resolved

Fix typo found by Michael!

4449f74

adomani changed the title ~~feat(CI): Zulip closed-pr emoji reaction~~ feat(CI): Zulip :closed-pr: emoji reaction Jan 21, 2025

grunweg reviewed Jan 21, 2025

View reviewed changes

grunweg added the awaiting-author A reviewer has asked the author a question or requested changes label Jan 21, 2025

add name to sparse-checkout step

6e51e44

adomani removed the awaiting-author A reviewer has asked the author a question or requested changes label Jan 21, 2025

add comment

23ca255

bryangingechen self-assigned this Jan 21, 2025

github-actions bot added the maintainer-merge label Jan 21, 2025

add delimiters

b44c5db

leanprover-community-mathlib4-bot added the ready-to-merge This PR has been sent to bors. label Jan 21, 2025

mathlib-bors bot changed the title ~~feat(CI): Zulip :closed-pr: emoji reaction~~ [Merged by Bors] - feat(CI): Zulip :closed-pr: emoji reaction Jan 21, 2025

mathlib-bors bot closed this Jan 21, 2025

mathlib-bors bot deleted the adomani/zulip_reaction_closed_pr branch January 21, 2025 20:43

adomani mentioned this pull request Jan 21, 2025

chore(CI): remove issue_number from :closed-pr: action #20925

Open

adomani mentioned this pull request Jan 21, 2025

feat(CI): remove :closed-pr: reaction, if PR is reopened #20926

Open

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

[Merged by Bors] - feat(CI): Zulip `:closed-pr:` emoji reaction #20902

[Merged by Bors] - feat(CI): Zulip `:closed-pr:` emoji reaction #20902

adomani commented Jan 21, 2025

github-actions bot commented Jan 21, 2025 •

edited

Loading

grunweg left a comment

grunweg left a comment

grunweg Jan 21, 2025

adomani Jan 21, 2025

grunweg Jan 21, 2025

adomani Jan 21, 2025

grunweg Jan 21, 2025

adomani commented Jan 21, 2025

adomani commented Jan 21, 2025 •

edited

Loading

grunweg commented Jan 21, 2025

grunweg commented Jan 21, 2025 •

edited

Loading

github-actions bot commented Jan 21, 2025

github-actions bot commented Jan 21, 2025

jcommelin commented Jan 21, 2025

mathlib-bors bot commented Jan 21, 2025

	python scripts/zulip_emoji_merge_delegate.py "$ZULIP_API_KEY" "$ZULIP_EMAIL" "$ZULIP_SITE" "closed" "${{ github.event.issue.number }}${{ github.event.pull_request.number }}"
	python scripts/zulip_emoji_merge_delegate.py "$ZULIP_API_KEY" "$ZULIP_EMAIL" "$ZULIP_SITE" "closed" "${{ github.event.issue.number }}" "${{ github.event.pull_request.number }}"

[Merged by Bors] - feat(CI): Zulip :closed-pr: emoji reaction #20902

[Merged by Bors] - feat(CI): Zulip :closed-pr: emoji reaction #20902

Conversation

adomani commented Jan 21, 2025

github-actions bot commented Jan 21, 2025 • edited Loading

PR summary b44c5dbddb

Import changes for modified files

Declarations diff

grunweg left a comment

Choose a reason for hiding this comment

grunweg left a comment

Choose a reason for hiding this comment

grunweg Jan 21, 2025

Choose a reason for hiding this comment

adomani Jan 21, 2025

Choose a reason for hiding this comment

grunweg Jan 21, 2025

Choose a reason for hiding this comment

adomani Jan 21, 2025

Choose a reason for hiding this comment

grunweg Jan 21, 2025

Choose a reason for hiding this comment

adomani commented Jan 21, 2025

adomani commented Jan 21, 2025 • edited Loading

grunweg commented Jan 21, 2025

grunweg commented Jan 21, 2025 • edited Loading

github-actions bot commented Jan 21, 2025

github-actions bot commented Jan 21, 2025

jcommelin commented Jan 21, 2025

mathlib-bors bot commented Jan 21, 2025

[Merged by Bors] - feat(CI): Zulip `:closed-pr:` emoji reaction #20902

[Merged by Bors] - feat(CI): Zulip `:closed-pr:` emoji reaction #20902

github-actions bot commented Jan 21, 2025 •

edited

Loading

adomani commented Jan 21, 2025 •

edited

Loading

grunweg commented Jan 21, 2025 •

edited

Loading