Skip to content

ci: refactor maintainer_*.yml workflows to use new helper actions#35110

Open
bryangingechen wants to merge 3 commits intoleanprover-community:masterfrom
bryangingechen:refactor-maintainer-bors-merge
Open

ci: refactor maintainer_*.yml workflows to use new helper actions#35110
bryangingechen wants to merge 3 commits intoleanprover-community:masterfrom
bryangingechen:refactor-maintainer-bors-merge

Conversation

@bryangingechen
Copy link
Contributor

@bryangingechen bryangingechen commented Feb 11, 2026

The workflows maintainer_{bors,merge}.yml workflows were rewritten in #26288 so that they were split into two workflows. The first workflow is triggered by an issue comment, PR review, or PR review comment and does not have access to secrets. The second workflow is triggered by the successful completion of the first workflow and does the actual labeling of the PR using its access to secrets. Data about the PR and the triggering comment / review is passed between workflows by use of a workflow artifact. It turns out this is a fairly useful pattern, so I've created leanprover-community/privilege-escalation-brdge with some helper actions that we will be able to use in more workflows.

This PR refactors the abovementioned PRs to use the new actions. There is a slight change in behavior: previously PRs which were opened from a branch in this repo (as opposed to a branch in a fork) would just be handled using some steps in the first workflow (since the workflow does get access to secrets for such PRs) and the second workflow would not be triggered. Now all PRs are treated equally -- they all go through both workflows. This will slow down labeling for the (rare) PRs which are still opened from branches in this repo, however, I think that's outweighed by the resulting simplification of the workflows. Other than this though the behavior should be unchanged.

Prepared with codex.


Open in Gitpod

@github-actions github-actions bot added the CI Modifies the continuous integration setup or other automation label Feb 11, 2026
@github-actions
Copy link

github-actions bot commented Feb 11, 2026

PR summary 7e516e0ca6

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).


- if: ${{ ! steps.merge_or_delegate.outputs.mOrD == '' || ! steps.merge_or_delegate.outputs.removeLabels == '' }}
name: Emit bridge artifact
uses: leanprover-community/privilege-escalation-bridge/emit@v1
Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I will change this uses (and the reference in the other file to /consume) to point to a specific commit after I'm more confident that the actions are stable.

Copy link
Contributor Author

@bryangingechen bryangingechen left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Removed an unused variable BOT that shellcheck was complaning about and also removed the expected_head_sha checks from the consume inputs since that check is brittle (could depend on merge SHA which changes when master changes).

Copy link
Contributor

@joneugster joneugster left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Looks good, thanks!

I guess my only question is about how the existing workflow worked, not your reimplementation...

sparse-checkout: |
scripts/zulip_emoji_reactions.py

- name: update zulip emoji reactions
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I don't see where this has been moved to? Why is it that this used to be present in both workflows?

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Good catch! I need to add these back since they were used to add the :bors: and maintainer merge emoji reactions.

@joneugster joneugster self-assigned this Feb 18, 2026
@joneugster joneugster added the awaiting-author A reviewer has asked the author a question or requested changes. label Feb 18, 2026
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

awaiting-author A reviewer has asked the author a question or requested changes. CI Modifies the continuous integration setup or other automation

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants

Comments