Skip to content

Commit 4b6ee3a

Browse files
j-loreauxj-loreaux
committed
Merge branch 'master' into j-loreaux/EMetric-UniformFun
2 parents 46e8938 + 8fea0ef commit 4b6ee3a

711 files changed

Lines changed: 17813 additions & 7955 deletions

File tree

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

‎.github/build.in.yml‎

Lines changed: 72 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -538,11 +538,13 @@ jobs:
538538
filterOutClosed: true
539539

540540
# Combine the output from the previous action with the metadata supplied by GitHub itself.
541+
# Note that if we fall back to github.event.pull_request data, the list of labels is generated when this workflow is triggered
542+
# and not updated afterwards!
541543
- id: PR
542544
shell: bash
543545
run: |
544-
echo "number=${{ steps.PR_from_push.outputs.number || github.event.pull_request.number }}" >> $GITHUB_OUTPUT
545-
echo "pr_labels=${{ steps.PR_from_push.outputs.pr_labels || join(github.event.pull_request.labels.*.name, ',') }}" >> $GITHUB_OUTPUT
546+
echo "number=${{ steps.PR_from_push.outputs.number || github.event.pull_request.number }}" | tee -a "$GITHUB_OUTPUT"
547+
echo "pr_labels=${{ steps.PR_from_push.outputs.pr_labels || join(github.event.pull_request.labels.*.name, ',') }}" | tee -a "$GITHUB_OUTPUT"
546548
547549
- if: contains(steps.PR.outputs.pr_labels, 'bench-after-CI')
548550
name: If `bench-after-CI` is present, add a `!bench` comment.
@@ -563,6 +565,74 @@ jobs:
563565
--header 'authorization: Bearer ${{ secrets.GITHUB_TOKEN }}'
564566
565567
- if: contains(steps.PR.outputs.pr_labels, 'auto-merge-after-CI')
568+
name: Get PR label timeline data
569+
# 'auto-merge-after-CI' must be within the last 100 labels added (could be increased to 250 if needed)
570+
# query from https://stackoverflow.com/a/67939355
571+
# unfortunately we cannot query only for 'auto-merge-after-CI' events
572+
# so we have to process this with jq in the next step
573+
id: get-timeline
574+
uses: octokit/graphql-action@8ad880e4d437783ea2ab17010324de1075228110 # v2.3.2
575+
with:
576+
query: |
577+
query($owner: String!, $name: String!, $number: Int!) {
578+
repository(owner: $owner, name: $name) {
579+
pullRequest(number: $number) {
580+
timelineItems(itemTypes: LABELED_EVENT, last: 100) {
581+
nodes {
582+
... on LabeledEvent {
583+
createdAt
584+
actor { login }
585+
label { name }
586+
}
587+
}
588+
}
589+
}
590+
}
591+
}
592+
owner: leanprover-community
593+
name: mathlib4
594+
number: ${{ steps.PR.outputs.number }}
595+
env:
596+
GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }}
597+
598+
- if: contains(steps.PR.outputs.pr_labels, 'auto-merge-after-CI')
599+
name: Extract label actor username
600+
id: get-label-actor
601+
run: |
602+
# Parse the GraphQL response and filter for the specific label
603+
echo '${{ steps.get-timeline.outputs.data }}'
604+
USERNAME=$(echo '${{ steps.get-timeline.outputs.data }}' | jq -r '
605+
.repository.pullRequest.timelineItems.nodes
606+
| map(select(.label.name == "auto-merge-after-CI"))
607+
| sort_by(.createdAt)
608+
| last
609+
| .actor.login // empty
610+
')
611+
612+
# Validate username format (GitHub usernames are alphanumeric + hyphens, max 39 chars)
613+
printf 'USERNAME: %s\n' "$USERNAME"
614+
if [[ -z "$USERNAME" ]]; then
615+
echo "Error: No actor found for the specified label"
616+
exit 1
617+
elif ! [[ "$USERNAME" =~ ^[a-zA-Z0-9-]{1,39}$ ]]; then
618+
echo "Error: Invalid username format: $USERNAME"
619+
exit 1
620+
fi
621+
622+
echo "username=$USERNAME" >> "$GITHUB_OUTPUT"
623+
echo "Found label actor: $USERNAME"
624+
625+
- if: contains(steps.PR.outputs.pr_labels, 'auto-merge-after-CI')
626+
name: check team membership
627+
uses: tspascoal/get-user-teams-membership@57e9f42acd78f4d0f496b3be4368fc5f62696662 # v3.0.0
628+
id: actorTeams
629+
with:
630+
organization: leanprover-community # optional. Default value ${{ github.repository_owner }}
631+
# Organization to get membership from.
632+
username: ${{ steps.get-label-actor.outputs.username }}
633+
GITHUB_TOKEN: ${{ secrets.MATHLIB_REVIEWERS_TEAM_KEY }} # (Requires scope: `read:org`)
634+
635+
- if: ${{ contains(steps.PR.outputs.pr_labels, 'auto-merge-after-CI') && (contains(steps.actorTeams.outputs.teams, 'mathlib-maintainers') || contains(steps.actorTeams.outputs.teams, 'bot-users')) }}
566636
name: If `auto-merge-after-CI` is present, add a `bors merge` comment.
567637
uses: GrantBirki/comment@608e41b19bc973020ec0e189ebfdae935d7fe0cc # v2.1.1
568638
with:

‎.github/workflows/PR_summary.yml‎

Lines changed: 21 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -110,23 +110,32 @@ jobs:
110110
run: |
111111
cd pr-branch
112112
touch moved_without_deprecation.txt
113+
touch extraneous_deprecated_module.txt
113114
git checkout ${{ github.base_ref }}
114115
while IFS= read -r file
115116
do
116117
if grep ^deprecated_module "${file}" ; then
117-
printf 'info: removed file %s contains a deprecation\n' "${file}"
118+
# shellcheck disable=SC2016
119+
printf '\n⚠️ **warning**: removed file `%s` contains a module deprecation: please add this in a follow-up PR instead\n' "${file}" |
120+
tee -a extraneous_deprecated_module.txt
118121
else
119122
# shellcheck disable=SC2016
120-
printf '\n⚠️ **warning**: file `%s` was removed without a module deprecation\n' "${file}" |
123+
printf '\nnote: file `%s` was removed.\nPlease create a follow-up pull request adding a module deprecation. Thanks!\n' "${file}" |
121124
tee -a moved_without_deprecation.txt
122125
fi
123126
done < removed_files.txt
124127
IFS=$'\n'
125128
while IFS= read -r file
126129
do
127-
# shellcheck disable=SC2016
128-
printf '\n⚠️ **warning**: file %s without a module deprecation\n' "${file}" |
129-
tee -a moved_without_deprecation.txt
130+
if grep ^deprecated_module "${file}" ; then
131+
# shellcheck disable=SC2016
132+
printf '\n⚠️ **warning**: renamed file `%s` contains a module deprecation: please add this in a follow-up PR instead\n' "${file}" |
133+
tee -a extraneous_deprecated_module.txt
134+
else
135+
# shellcheck disable=SC2016
136+
printf '\nnote: file `%s` without a module deprecation\nPlease create a follow-up pull request adding one. Thanks!\n' "${file}" |
137+
tee -a moved_without_deprecation.txt
138+
fi
130139
done < renamed_files.txt
131140
132141
# we return to the PR branch, since the next step wants it!
@@ -209,12 +218,18 @@ jobs:
209218
# store in a file, to avoid "long arguments" error.
210219
printf '%s [%s](%s)%s\n\n%s\n\n---\n\n%s\n\n---\n\n%s\n' "${title}" "$(git rev-parse --short HEAD)" "${hashURL}" "${high_percentages}" "${importCount}" "${declDiff}" "${techDebtVar}" > please_merge_master.md
211220
212-
echo "Include any errors about removed or renamed files without deprecation."
221+
echo "Include any errors about removed or renamed files without deprecation,"
222+
echo "as well as errors about extraneous deprecated_module additions."
213223
if [ -s moved_without_deprecation.txt ]
214224
then
215225
printf '\n\n---\n\n' >> please_merge_master.md
216226
cat moved_without_deprecation.txt >> please_merge_master.md
217227
fi
228+
if [ -s extraneous_deprecated_module.txt ]
229+
then
230+
printf '\n\n---\n\n' >> please_merge_master.md
231+
cat extraneous_deprecated_module.txt >> please_merge_master.md
232+
fi
218233
219234
cat please_merge_master.md
220235
../master-branch/scripts/update_PR_comment.sh please_merge_master.md "${title}" "${PR}"

‎.github/workflows/bors.yml‎

Lines changed: 72 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -548,11 +548,13 @@ jobs:
548548
filterOutClosed: true
549549

550550
# Combine the output from the previous action with the metadata supplied by GitHub itself.
551+
# Note that if we fall back to github.event.pull_request data, the list of labels is generated when this workflow is triggered
552+
# and not updated afterwards!
551553
- id: PR
552554
shell: bash
553555
run: |
554-
echo "number=${{ steps.PR_from_push.outputs.number || github.event.pull_request.number }}" >> $GITHUB_OUTPUT
555-
echo "pr_labels=${{ steps.PR_from_push.outputs.pr_labels || join(github.event.pull_request.labels.*.name, ',') }}" >> $GITHUB_OUTPUT
556+
echo "number=${{ steps.PR_from_push.outputs.number || github.event.pull_request.number }}" | tee -a "$GITHUB_OUTPUT"
557+
echo "pr_labels=${{ steps.PR_from_push.outputs.pr_labels || join(github.event.pull_request.labels.*.name, ',') }}" | tee -a "$GITHUB_OUTPUT"
556558
557559
- if: contains(steps.PR.outputs.pr_labels, 'bench-after-CI')
558560
name: If `bench-after-CI` is present, add a `!bench` comment.
@@ -573,6 +575,74 @@ jobs:
573575
--header 'authorization: Bearer ${{ secrets.GITHUB_TOKEN }}'
574576
575577
- if: contains(steps.PR.outputs.pr_labels, 'auto-merge-after-CI')
578+
name: Get PR label timeline data
579+
# 'auto-merge-after-CI' must be within the last 100 labels added (could be increased to 250 if needed)
580+
# query from https://stackoverflow.com/a/67939355
581+
# unfortunately we cannot query only for 'auto-merge-after-CI' events
582+
# so we have to process this with jq in the next step
583+
id: get-timeline
584+
uses: octokit/graphql-action@8ad880e4d437783ea2ab17010324de1075228110 # v2.3.2
585+
with:
586+
query: |
587+
query($owner: String!, $name: String!, $number: Int!) {
588+
repository(owner: $owner, name: $name) {
589+
pullRequest(number: $number) {
590+
timelineItems(itemTypes: LABELED_EVENT, last: 100) {
591+
nodes {
592+
... on LabeledEvent {
593+
createdAt
594+
actor { login }
595+
label { name }
596+
}
597+
}
598+
}
599+
}
600+
}
601+
}
602+
owner: leanprover-community
603+
name: mathlib4
604+
number: ${{ steps.PR.outputs.number }}
605+
env:
606+
GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }}
607+
608+
- if: contains(steps.PR.outputs.pr_labels, 'auto-merge-after-CI')
609+
name: Extract label actor username
610+
id: get-label-actor
611+
run: |
612+
# Parse the GraphQL response and filter for the specific label
613+
echo '${{ steps.get-timeline.outputs.data }}'
614+
USERNAME=$(echo '${{ steps.get-timeline.outputs.data }}' | jq -r '
615+
.repository.pullRequest.timelineItems.nodes
616+
| map(select(.label.name == "auto-merge-after-CI"))
617+
| sort_by(.createdAt)
618+
| last
619+
| .actor.login // empty
620+
')
621+
622+
# Validate username format (GitHub usernames are alphanumeric + hyphens, max 39 chars)
623+
printf 'USERNAME: %s\n' "$USERNAME"
624+
if [[ -z "$USERNAME" ]]; then
625+
echo "Error: No actor found for the specified label"
626+
exit 1
627+
elif ! [[ "$USERNAME" =~ ^[a-zA-Z0-9-]{1,39}$ ]]; then
628+
echo "Error: Invalid username format: $USERNAME"
629+
exit 1
630+
fi
631+
632+
echo "username=$USERNAME" >> "$GITHUB_OUTPUT"
633+
echo "Found label actor: $USERNAME"
634+
635+
- if: contains(steps.PR.outputs.pr_labels, 'auto-merge-after-CI')
636+
name: check team membership
637+
uses: tspascoal/get-user-teams-membership@57e9f42acd78f4d0f496b3be4368fc5f62696662 # v3.0.0
638+
id: actorTeams
639+
with:
640+
organization: leanprover-community # optional. Default value ${{ github.repository_owner }}
641+
# Organization to get membership from.
642+
username: ${{ steps.get-label-actor.outputs.username }}
643+
GITHUB_TOKEN: ${{ secrets.MATHLIB_REVIEWERS_TEAM_KEY }} # (Requires scope: `read:org`)
644+
645+
- if: ${{ contains(steps.PR.outputs.pr_labels, 'auto-merge-after-CI') && (contains(steps.actorTeams.outputs.teams, 'mathlib-maintainers') || contains(steps.actorTeams.outputs.teams, 'bot-users')) }}
576646
name: If `auto-merge-after-CI` is present, add a `bors merge` comment.
577647
uses: GrantBirki/comment@608e41b19bc973020ec0e189ebfdae935d7fe0cc # v2.1.1
578648
with:

‎.github/workflows/build.yml‎

Lines changed: 72 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -555,11 +555,13 @@ jobs:
555555
filterOutClosed: true
556556

557557
# Combine the output from the previous action with the metadata supplied by GitHub itself.
558+
# Note that if we fall back to github.event.pull_request data, the list of labels is generated when this workflow is triggered
559+
# and not updated afterwards!
558560
- id: PR
559561
shell: bash
560562
run: |
561-
echo "number=${{ steps.PR_from_push.outputs.number || github.event.pull_request.number }}" >> $GITHUB_OUTPUT
562-
echo "pr_labels=${{ steps.PR_from_push.outputs.pr_labels || join(github.event.pull_request.labels.*.name, ',') }}" >> $GITHUB_OUTPUT
563+
echo "number=${{ steps.PR_from_push.outputs.number || github.event.pull_request.number }}" | tee -a "$GITHUB_OUTPUT"
564+
echo "pr_labels=${{ steps.PR_from_push.outputs.pr_labels || join(github.event.pull_request.labels.*.name, ',') }}" | tee -a "$GITHUB_OUTPUT"
563565
564566
- if: contains(steps.PR.outputs.pr_labels, 'bench-after-CI')
565567
name: If `bench-after-CI` is present, add a `!bench` comment.
@@ -580,6 +582,74 @@ jobs:
580582
--header 'authorization: Bearer ${{ secrets.GITHUB_TOKEN }}'
581583
582584
- if: contains(steps.PR.outputs.pr_labels, 'auto-merge-after-CI')
585+
name: Get PR label timeline data
586+
# 'auto-merge-after-CI' must be within the last 100 labels added (could be increased to 250 if needed)
587+
# query from https://stackoverflow.com/a/67939355
588+
# unfortunately we cannot query only for 'auto-merge-after-CI' events
589+
# so we have to process this with jq in the next step
590+
id: get-timeline
591+
uses: octokit/graphql-action@8ad880e4d437783ea2ab17010324de1075228110 # v2.3.2
592+
with:
593+
query: |
594+
query($owner: String!, $name: String!, $number: Int!) {
595+
repository(owner: $owner, name: $name) {
596+
pullRequest(number: $number) {
597+
timelineItems(itemTypes: LABELED_EVENT, last: 100) {
598+
nodes {
599+
... on LabeledEvent {
600+
createdAt
601+
actor { login }
602+
label { name }
603+
}
604+
}
605+
}
606+
}
607+
}
608+
}
609+
owner: leanprover-community
610+
name: mathlib4
611+
number: ${{ steps.PR.outputs.number }}
612+
env:
613+
GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }}
614+
615+
- if: contains(steps.PR.outputs.pr_labels, 'auto-merge-after-CI')
616+
name: Extract label actor username
617+
id: get-label-actor
618+
run: |
619+
# Parse the GraphQL response and filter for the specific label
620+
echo '${{ steps.get-timeline.outputs.data }}'
621+
USERNAME=$(echo '${{ steps.get-timeline.outputs.data }}' | jq -r '
622+
.repository.pullRequest.timelineItems.nodes
623+
| map(select(.label.name == "auto-merge-after-CI"))
624+
| sort_by(.createdAt)
625+
| last
626+
| .actor.login // empty
627+
')
628+
629+
# Validate username format (GitHub usernames are alphanumeric + hyphens, max 39 chars)
630+
printf 'USERNAME: %s\n' "$USERNAME"
631+
if [[ -z "$USERNAME" ]]; then
632+
echo "Error: No actor found for the specified label"
633+
exit 1
634+
elif ! [[ "$USERNAME" =~ ^[a-zA-Z0-9-]{1,39}$ ]]; then
635+
echo "Error: Invalid username format: $USERNAME"
636+
exit 1
637+
fi
638+
639+
echo "username=$USERNAME" >> "$GITHUB_OUTPUT"
640+
echo "Found label actor: $USERNAME"
641+
642+
- if: contains(steps.PR.outputs.pr_labels, 'auto-merge-after-CI')
643+
name: check team membership
644+
uses: tspascoal/get-user-teams-membership@57e9f42acd78f4d0f496b3be4368fc5f62696662 # v3.0.0
645+
id: actorTeams
646+
with:
647+
organization: leanprover-community # optional. Default value ${{ github.repository_owner }}
648+
# Organization to get membership from.
649+
username: ${{ steps.get-label-actor.outputs.username }}
650+
GITHUB_TOKEN: ${{ secrets.MATHLIB_REVIEWERS_TEAM_KEY }} # (Requires scope: `read:org`)
651+
652+
- if: ${{ contains(steps.PR.outputs.pr_labels, 'auto-merge-after-CI') && (contains(steps.actorTeams.outputs.teams, 'mathlib-maintainers') || contains(steps.actorTeams.outputs.teams, 'bot-users')) }}
583653
name: If `auto-merge-after-CI` is present, add a `bors merge` comment.
584654
uses: GrantBirki/comment@608e41b19bc973020ec0e189ebfdae935d7fe0cc # v2.1.1
585655
with:

0 commit comments

Comments
 (0)