Skip to content

feat(workflows): automatically assign reviewers - #27698

Closed
grunweg wants to merge 12 commits into
leanprover-community:masterfrom
grunweg:MR-auto-assign-reviewers
Closed

feat(workflows): automatically assign reviewers#27698
grunweg wants to merge 12 commits into
leanprover-community:masterfrom
grunweg:MR-auto-assign-reviewers

Conversation

@grunweg

@grunweg grunweg commented Jul 30, 2025

Copy link
Copy Markdown
Contributor

Once per day, automatically assign all proposed reviewers from the automatic assignment algorithm.
These are initial suggestions; users are free to manually assign to somebody else (or to un-assign themselves; after a day, the algorithm will randomly choose a user again.)

To work around variable quoting issues, we follow a slightly roundabout approach: instead of parsing the json file using a shell script and calling the github API from bash in a loop, we use Python to parse the file, generate a shell script with the desired APIi calls, and execute that script instead.
(This has the advantage of making the output easily auditable; future rewrites are also welcome.)


See the github documentation for the assignment syntax used.

Open in Gitpod

grunweg and others added 12 commits May 9, 2025 13:06
@github-actions github-actions Bot added the CI Modifies the continuous integration setup or other automation label Jul 30, 2025
@grunweg
grunweg force-pushed the MR-auto-assign-reviewers branch from 2875248 to c7e6567 Compare July 30, 2025 19:55
@github-actions

github-actions Bot commented Jul 30, 2025

Copy link
Copy Markdown

PR summary 8635ef05f0

Import changes for modified files

No significant changes to the import graph

Import changes for all files
Files Import difference

Declarations diff

+ call(number:

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

grunweg commented Jul 30, 2025

Copy link
Copy Markdown
Contributor Author

Duplicate of #26109; this has fulfilled its purpose.

@grunweg grunweg closed this Jul 30, 2025
@grunweg
grunweg deleted the MR-auto-assign-reviewers branch July 30, 2025 19:58
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

CI Modifies the continuous integration setup or other automation

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant