Skip to content

Commit 1861a8f

Browse files
kim-emkim-em
committed
Merge remote-tracking branch 'upstream/master' into bump/v4.22.0
2 parents e8f765e + 5cdffe1 commit 1861a8f

File tree

126 files changed

+2081
-614
lines changed

Some content is hidden

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

126 files changed

+2081
-614
lines changed

‎.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/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:

‎.github/workflows/build_fork.yml‎

Lines changed: 72 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -552,11 +552,13 @@ jobs:
552552
filterOutClosed: true
553553

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

‎Archive/Imo/Imo2024Q5.lean‎

Lines changed: 5 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -562,6 +562,8 @@ lemma row2_mem_monsterCells_monsterData12 (hN : 2 ≤ N) {c₁ c₂ : Fin (N + 1
562562
exact (monsterData12_apply_row2 hN h).symm
563563

564564
lemma Strategy.not_forcesWinIn_two (s : Strategy N) (hN : 2 ≤ N) : ¬ s.ForcesWinIn 2 := by
565+
have : NeZero N := ⟨by omega⟩
566+
have : 0 < N := by omega
565567
simp only [ForcesWinIn, WinsIn, Set.mem_range, not_forall, not_exists, Option.ne_none_iff_isSome]
566568
let m1 : Cell N := (s Fin.elim0).findFstEq 1
567569
let m2 : Cell N := (s ![m1]).findFstEq 2
@@ -570,7 +572,6 @@ lemma Strategy.not_forcesWinIn_two (s : Strategy N) (hN : 2 ≤ N) : ¬ s.Forces
570572
have h2r : m2.1 = 2 := Path.findFstEq_fst _ _
571573
have h1 : m1 ∈ m.monsterCells := by
572574
convert row1_mem_monsterCells_monsterData12 hN m1.2 m2.2
573-
have h2 : ((2 : Fin (N + 2)) : ℕ) = 2 := Nat.mod_eq_of_lt (by omega : 2 < N + 2)
574575
refine ⟨m, fun i ↦ ?_⟩
575576
fin_cases i
576577
· simp only [Strategy.play_zero, Path.firstMonster_eq_of_findFstEq_mem h1, Option.isSome_some]
@@ -582,15 +583,13 @@ lemma Strategy.not_forcesWinIn_two (s : Strategy N) (hN : 2 ≤ N) : ¬ s.Forces
582583
· rw [Path.firstMonster_isSome]
583584
refine ⟨m1, ?_, h1⟩
584585
have h' : m1 = (⟨(((2 : Fin (N + 2)) : ℕ) - 1 : ℕ), by omega⟩, m2.2) := by
585-
simp [h2, Prod.ext_iff, h1r, h2r, h]
586+
simpa [Prod.ext_iff, h1r, h2r, h]
586587
nth_rw 2 [h']
587-
refine Path.findFstEq_fst_sub_one_mem _ ?_
588-
rw [ne_eq, Fin.ext_iff, h2]
589-
norm_num
588+
exact Path.findFstEq_fst_sub_one_mem _ two_ne_zero
590589
· rw [Path.firstMonster_isSome]
591590
refine ⟨m2, Path.findFstEq_mem_cells _ _, ?_⟩
592591
convert row2_mem_monsterCells_monsterData12 hN h using 1
593-
simp [Prod.ext_iff, h2r, Fin.ext_iff, h2]
592+
simpa [Prod.ext_iff, h2r, Fin.ext_iff]
594593

595594
lemma Strategy.ForcesWinIn.three_le {s : Strategy N} {k : ℕ} (hf : s.ForcesWinIn k)
596595
(hN : 2 ≤ N) : 3 ≤ k := by

0 commit comments

Comments
 (0)