Skip to content

Commit c25fea8

Browse files
kim-emkim-em
committed
Merge remote-tracking branch 'origin/master' into finRange_def
2 parents 988ed4b + b965444 commit c25fea8

111 files changed

Lines changed: 2322 additions & 1789 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/workflows/bench_summary_comment.yml‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -27,7 +27,7 @@ jobs:
2727
run: |
2828
{
2929
cat scripts/bench_summary.lean
30-
printf $'run_cmd BenchAction.addBenchSummaryComment %s "leanprover-community/mathlib4"' "${PR}"
30+
printf $'run_cmd BenchAction.addBenchSummaryComment %s "leanprover-community/mathlib4" %s' "${PR}" "${{ github.run_id }}"
3131
} |
3232
lake env lean --stdin
3333
env:

‎.github/workflows/discover-lean-pr-testing.yml‎

Lines changed: 15 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -4,6 +4,8 @@ on:
44
push:
55
branches:
66
- nightly-testing
7+
paths:
8+
- lean-toolchain
79

810
jobs:
911
discover-lean-pr-testing:
@@ -36,8 +38,10 @@ jobs:
3638
# The "./" in front of the path is important for `git show`
3739
OLD=$(git show "$PREV_COMMIT":./lean-toolchain | cut -f2 -d:)
3840
39-
echo "new=$NEW" >> "$GITHUB_OUTPUT"
41+
echo "old=$OLD"
42+
echo "new=$NEW"
4043
echo "old=$OLD" >> "$GITHUB_OUTPUT"
44+
echo "new=$NEW" >> "$GITHUB_OUTPUT"
4145
4246
- name: Clone lean4 repository and get PRs
4347
id: get-prs
@@ -63,7 +67,10 @@ jobs:
6367
# This will only fetch commits newer than previously fetched commits (ie $OLD)
6468
git fetch origin tag "$NEW" --no-tags
6569
66-
PRS=$(git log --oneline "$OLD..$NEW" | sed 's/.*(#\([0-9]\+\))$/\1/')
70+
# Find all commits to lean4 between the $OLD and $NEW toolchains
71+
# and extract the github PR numbers
72+
# (drop anything that doesn't look like a PR number from the final result)
73+
PRS=$(git log --oneline "$OLD..$NEW" | sed 's/.*(#\([0-9]\+\))$/\1/' | grep -E '^[0-9]+$')
6774
6875
# Output the PRs
6976
echo "$PRS"
@@ -74,12 +81,14 @@ jobs:
7481
run: |
7582
# Use the PRs from the previous step
7683
PRS="${{ steps.get-prs.outputs.prs }}"
84+
echo "=== PRS ========================="
7785
echo "$PRS"
78-
echo "===================="
7986
echo "$PRS" | tr ' ' '\n' > prs.txt
87+
echo "=== prs.txt ====================="
88+
cat prs.txt
8089
MATCHING_BRANCHES=$(git branch -r | grep -f prs.txt)
90+
echo "=== MATCHING_BRANCHES ==========="
8191
echo "$MATCHING_BRANCHES"
82-
echo "===================="
8392
8493
# Initialize an empty variable to store branches with relevant diffs
8594
RELEVANT_BRANCHES=""
@@ -92,11 +101,12 @@ jobs:
92101
# Check if the diff contains files other than the specified ones
93102
if echo "$DIFF_FILES" | grep -v -e 'lake-manifest.json' -e 'lakefile.lean' -e 'lean-toolchain'; then
94103
# If it does, add the branch to RELEVANT_BRANCHES
95-
RELEVANT_BRANCHES="$RELEVANT_BRANCHES\n- $BRANCH"
104+
RELEVANT_BRANCHES="$RELEVANT_BRANCHES"$'\n- '"$BRANCH"
96105
fi
97106
done
98107
99108
# Output the relevant branches
109+
echo "=== RELEVANT_BRANCHES ==========="
100110
echo "'$RELEVANT_BRANCHES'"
101111
printf "branches<<EOF\n%s\nEOF" "$RELEVANT_BRANCHES" >> "$GITHUB_OUTPUT"
102112

‎.github/workflows/maintainer_bors.yml‎

Lines changed: 33 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -84,4 +84,36 @@ jobs:
8484
curl --request DELETE \
8585
--url "https://api.github.com/repos/${{ github.repository }}/issues/${{ github.event.issue.number }}${{ github.event.pull_request.number }}/labels/awaiting-author" \
8686
--header 'authorization: Bearer ${{ secrets.TRIAGE_TOKEN }}'
87-
# comment uses ${{ secrets.GITHUB_TOKEN }}
87+
88+
- name: Set up Python
89+
if: ${{ ! steps.merge_or_delegate.outputs.mOrD == '' &&
90+
( steps.user_permission.outputs.require-result == 'true' ||
91+
steps.merge_or_delegate.outputs.bot == 'true' ) }}
92+
uses: actions/setup-python@v5
93+
with:
94+
python-version: '3.x'
95+
96+
- name: Install dependencies
97+
if: ${{ ! steps.merge_or_delegate.outputs.mOrD == '' &&
98+
( steps.user_permission.outputs.require-result == 'true' ||
99+
steps.merge_or_delegate.outputs.bot == 'true' ) }}
100+
run: |
101+
python -m pip install --upgrade pip
102+
pip install zulip
103+
104+
- uses: actions/checkout@v4
105+
with:
106+
ref: master
107+
sparse-checkout: |
108+
scripts/zulip_emoji_merge_delegate.py
109+
110+
- name: Run Zulip Emoji Merge Delegate Script
111+
if: ${{ ! steps.merge_or_delegate.outputs.mOrD == '' &&
112+
( steps.user_permission.outputs.require-result == 'true' ||
113+
steps.merge_or_delegate.outputs.bot == 'true' ) }}
114+
env:
115+
ZULIP_API_KEY: ${{ secrets.ZULIP_API_KEY }}
116+
ZULIP_EMAIL: github-mathlib4-bot@leanprover.zulipchat.com
117+
ZULIP_SITE: https://leanprover.zulipchat.com
118+
run: |
119+
python scripts/zulip_emoji_merge_delegate.py "$ZULIP_API_KEY" "$ZULIP_EMAIL" "$ZULIP_SITE" "${{ steps.merge_or_delegate.outputs.mOrD }}" "${{ github.event.issue.number }}${{ github.event.pull_request.number }}"

‎.github/workflows/zulip_emoji_merge_delegate.yaml‎

Lines changed: 14 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -1,19 +1,19 @@
11
name: Zulip Emoji Merge Delegate
22

33
on:
4-
schedule:
5-
- cron: '0 * * * *' # Runs every hour
4+
push:
5+
branches:
6+
- master
67

78
jobs:
8-
zulip-emoji-merge-delegate:
9+
zulip-emoji-merged:
910
runs-on: ubuntu-latest
1011

1112
steps:
1213
- name: Checkout mathlib repository
1314
uses: actions/checkout@v4
1415
with:
15-
sparse-checkout: |
16-
scripts
16+
fetch-depth: 0 # donwload the full repository
1717

1818
- name: Set up Python
1919
uses: actions/setup-python@v5
@@ -30,6 +30,13 @@ jobs:
3030
ZULIP_API_KEY: ${{ secrets.ZULIP_API_KEY }}
3131
ZULIP_EMAIL: github-mathlib4-bot@leanprover.zulipchat.com
3232
ZULIP_SITE: https://leanprover.zulipchat.com
33-
GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }}
3433
run: |
35-
python scripts/zulip_emoji_merge_delegate.py "$ZULIP_API_KEY" "$ZULIP_EMAIL" "$ZULIP_SITE" "$GITHUB_TOKEN"
34+
# scan the commits of the past 10 minutes, assuming that the timezone of the current machine
35+
# is the same that performed the commit
36+
git log --since="10 minutes ago" --pretty=oneline
37+
38+
printf $'Scanning commits:\n%s\n\nContinuing\n' "$(git log --since="10 minutes ago" --pretty=oneline)"
39+
while read -r pr_number; do
40+
printf $'Running the python script with pr "%s"\n' "${pr_number}"
41+
python scripts/zulip_emoji_merge_delegate.py "$ZULIP_API_KEY" "$ZULIP_EMAIL" "$ZULIP_SITE" "[Merged by Bors]" "${pr_number}"
42+
done < <(git log --oneline -n 10 | awk -F# '{ gsub(/)$/, ""); print $NF}')

‎Counterexamples/DirectSumIsInternal.lean‎

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -12,10 +12,10 @@ import Mathlib.Tactic.FinCases
1212
# Not all complementary decompositions of a module over a semiring make up a direct sum
1313
1414
This shows that while `ℤ≤0` and `ℤ≥0` are complementary `ℕ`-submodules of `ℤ`, which in turn
15-
implies as a collection they are `CompleteLattice.Independent` and that they span all of `ℤ`, they
15+
implies as a collection they are `iSupIndep` and that they span all of `ℤ`, they
1616
do not form a decomposition into a direct sum.
1717
18-
This file demonstrates why `DirectSum.isInternal_submodule_of_independent_of_iSup_eq_top` must
18+
This file demonstrates why `DirectSum.isInternal_submodule_of_iSupIndep_of_iSup_eq_top` must
1919
take `Ring R` and not `Semiring R`.
2020
-/
2121

@@ -57,9 +57,9 @@ theorem withSign.isCompl : IsCompl ℤ≥0 ℤ≤0 := by
5757
· exact Submodule.mem_sup_left (mem_withSign_one.mpr hp)
5858
· exact Submodule.mem_sup_right (mem_withSign_neg_one.mpr hn)
5959

60-
def withSign.independent : CompleteLattice.Independent withSign := by
60+
def withSign.independent : iSupIndep withSign := by
6161
apply
62-
(CompleteLattice.independent_pair UnitsInt.one_ne_neg_one _).mpr withSign.isCompl.disjoint
62+
(iSupIndep_pair UnitsInt.one_ne_neg_one _).mpr withSign.isCompl.disjoint
6363
intro i
6464
fin_cases i <;> simp
6565

‎Mathlib.lean‎

Lines changed: 7 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -287,14 +287,18 @@ import Mathlib.Algebra.Group.Nat.Even
287287
import Mathlib.Algebra.Group.Nat.TypeTags
288288
import Mathlib.Algebra.Group.Nat.Units
289289
import Mathlib.Algebra.Group.NatPowAssoc
290+
import Mathlib.Algebra.Group.Operations
290291
import Mathlib.Algebra.Group.Opposite
291292
import Mathlib.Algebra.Group.PNatPowAssoc
292293
import Mathlib.Algebra.Group.Pi.Basic
293294
import Mathlib.Algebra.Group.Pi.Lemmas
294295
import Mathlib.Algebra.Group.Pointwise.Finset.Basic
295296
import Mathlib.Algebra.Group.Pointwise.Finset.Interval
296297
import Mathlib.Algebra.Group.Pointwise.Set.Basic
298+
import Mathlib.Algebra.Group.Pointwise.Set.BigOperators
297299
import Mathlib.Algebra.Group.Pointwise.Set.Card
300+
import Mathlib.Algebra.Group.Pointwise.Set.Finite
301+
import Mathlib.Algebra.Group.Pointwise.Set.ListOfFn
298302
import Mathlib.Algebra.Group.Prod
299303
import Mathlib.Algebra.Group.Semiconj.Basic
300304
import Mathlib.Algebra.Group.Semiconj.Defs
@@ -515,6 +519,7 @@ import Mathlib.Algebra.Module.Equiv.Basic
515519
import Mathlib.Algebra.Module.Equiv.Defs
516520
import Mathlib.Algebra.Module.Equiv.Opposite
517521
import Mathlib.Algebra.Module.FinitePresentation
522+
import Mathlib.Algebra.Module.FreeLocus
518523
import Mathlib.Algebra.Module.GradedModule
519524
import Mathlib.Algebra.Module.Hom
520525
import Mathlib.Algebra.Module.Injective
@@ -661,6 +666,7 @@ import Mathlib.Algebra.Order.Group.OrderIso
661666
import Mathlib.Algebra.Order.Group.PiLex
662667
import Mathlib.Algebra.Order.Group.Pointwise.Bounds
663668
import Mathlib.Algebra.Order.Group.Pointwise.CompleteLattice
669+
import Mathlib.Algebra.Order.Group.Pointwise.Interval
664670
import Mathlib.Algebra.Order.Group.PosPart
665671
import Mathlib.Algebra.Order.Group.Prod
666672
import Mathlib.Algebra.Order.Group.Synonym
@@ -2820,11 +2826,7 @@ import Mathlib.Data.Set.Operations
28202826
import Mathlib.Data.Set.Opposite
28212827
import Mathlib.Data.Set.Pairwise.Basic
28222828
import Mathlib.Data.Set.Pairwise.Lattice
2823-
import Mathlib.Data.Set.Pointwise.BigOperators
2824-
import Mathlib.Data.Set.Pointwise.Finite
2825-
import Mathlib.Data.Set.Pointwise.Interval
28262829
import Mathlib.Data.Set.Pointwise.Iterate
2827-
import Mathlib.Data.Set.Pointwise.ListOfFn
28282830
import Mathlib.Data.Set.Pointwise.SMul
28292831
import Mathlib.Data.Set.Pointwise.Support
28302832
import Mathlib.Data.Set.Prod
@@ -3952,6 +3954,7 @@ import Mathlib.Order.Filter.ENNReal
39523954
import Mathlib.Order.Filter.EventuallyConst
39533955
import Mathlib.Order.Filter.Extr
39543956
import Mathlib.Order.Filter.FilterProduct
3957+
import Mathlib.Order.Filter.Finite
39553958
import Mathlib.Order.Filter.Germ.Basic
39563959
import Mathlib.Order.Filter.Germ.OrderedMonoid
39573960
import Mathlib.Order.Filter.IndicatorFunction

‎Mathlib/Algebra/Algebra/Operations.lean‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -6,9 +6,9 @@ Authors: Kenny Lau
66
import Mathlib.Algebra.Algebra.Bilinear
77
import Mathlib.Algebra.Algebra.Opposite
88
import Mathlib.Algebra.Group.Pointwise.Finset.Basic
9+
import Mathlib.Algebra.Group.Pointwise.Set.BigOperators
910
import Mathlib.Algebra.GroupWithZero.NonZeroDivisors
1011
import Mathlib.Algebra.Module.Submodule.Pointwise
11-
import Mathlib.Data.Set.Pointwise.BigOperators
1212
import Mathlib.Data.Set.Semiring
1313
import Mathlib.GroupTheory.GroupAction.SubMulAction.Pointwise
1414

0 commit comments

Comments
 (0)