Skip to content

Commit 5e504e1

Browse files
leanprover-community-mathlib4-botleanprover-community-mathlib4-bot
committed
Update lean-toolchain for leanprover/lean4#10959 
2 parents fc2fe7a + 5acb797 commit 5e504e1

File tree

780 files changed

+16209
-5433
lines changed

Some content is hidden

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

780 files changed

+16209
-5433
lines changed

‎.github/build.in.yml‎

Lines changed: 20 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -15,8 +15,7 @@ env:
1515
concurrency:
1616
# label each workflow run; only the latest with each label will run
1717
# workflows on master get more expressive labels
18-
group: ${{ github.workflow }}-${{ github.ref }}.
19-
${{ ( contains(fromJSON( '["refs/heads/master", "refs/heads/staging"]'), github.ref ) && github.run_id) || ''}}
18+
group: ${{ github.workflow }}-${{ github.ref }}-${{ (contains(fromJSON('["refs/heads/master", "refs/heads/staging"]'), github.ref) && github.run_id) || '' }}
2019
# cancel any running workflow with the same label
2120
cancel-in-progress: true
2221

@@ -132,8 +131,23 @@ jobs:
132131
- name: set LEAN_SRC_PATH
133132
shell: bash
134133
run: |
135-
# Construct the LEAN_SRC_PATH using the toolchain directory
136-
LEAN_SRC_PATH=".:$TOOLCHAIN_DIR/src/lean/lake:.lake/packages/Cli:.lake/packages/batteries:.lake/packages/Qq:.lake/packages/aesop:.lake/packages/proofwidgets:.lake/packages/importGraph:.lake/packages/LeanSearchClient:.lake/packages/plausible:.lake/packages/requests:.lake/packages/openAI_client:.lake/packages/reap"
134+
cd pr-branch
135+
136+
# Start with the base paths
137+
LEAN_SRC_PATH=".:$TOOLCHAIN_DIR/src/lean/lake"
138+
139+
# Extract package names from lake-manifest.json and validate them
140+
# Only allow A-Z, a-z, 0-9, _, and - characters
141+
# Build the LEAN_SRC_PATH by appending each validated package
142+
PACKAGE_NAMES=$(jq -r '.packages[].name' lake-manifest.json)
143+
for pkg in $PACKAGE_NAMES; do
144+
if [[ "$pkg" =~ ^[A-Za-z0-9_-]+$ ]]; then
145+
LEAN_SRC_PATH="$LEAN_SRC_PATH:.lake/packages/$pkg"
146+
else
147+
echo "Warning: Skipping invalid package name: $pkg"
148+
fi
149+
done
150+
137151
echo "LEAN_SRC_PATH=$LEAN_SRC_PATH"
138152
139153
# Set it as an environment variable for subsequent steps
@@ -538,8 +552,9 @@ jobs:
538552

539553
- name: build everything
540554
# make sure everything is available for test/import_all.lean
555+
# and that miscellaneous executables still work
541556
run: |
542-
lake build Batteries Qq Aesop ProofWidgets Plausible
557+
lake build Batteries Qq Aesop ProofWidgets Plausible pole unused
543558
544559
# temporarily comment out
545560
# - name: build AesopTest (nightly-testing only)

‎.github/workflows/bors.yml‎

Lines changed: 20 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -25,8 +25,7 @@ env:
2525
concurrency:
2626
# label each workflow run; only the latest with each label will run
2727
# workflows on master get more expressive labels
28-
group: ${{ github.workflow }}-${{ github.ref }}.
29-
${{ ( contains(fromJSON( '["refs/heads/master", "refs/heads/staging"]'), github.ref ) && github.run_id) || ''}}
28+
group: ${{ github.workflow }}-${{ github.ref }}-${{ (contains(fromJSON('["refs/heads/master", "refs/heads/staging"]'), github.ref) && github.run_id) || '' }}
3029
# cancel any running workflow with the same label
3130
cancel-in-progress: true
3231

@@ -142,8 +141,23 @@ jobs:
142141
- name: set LEAN_SRC_PATH
143142
shell: bash
144143
run: |
145-
# Construct the LEAN_SRC_PATH using the toolchain directory
146-
LEAN_SRC_PATH=".:$TOOLCHAIN_DIR/src/lean/lake:.lake/packages/Cli:.lake/packages/batteries:.lake/packages/Qq:.lake/packages/aesop:.lake/packages/proofwidgets:.lake/packages/importGraph:.lake/packages/LeanSearchClient:.lake/packages/plausible:.lake/packages/requests:.lake/packages/openAI_client:.lake/packages/reap"
144+
cd pr-branch
145+
146+
# Start with the base paths
147+
LEAN_SRC_PATH=".:$TOOLCHAIN_DIR/src/lean/lake"
148+
149+
# Extract package names from lake-manifest.json and validate them
150+
# Only allow A-Z, a-z, 0-9, _, and - characters
151+
# Build the LEAN_SRC_PATH by appending each validated package
152+
PACKAGE_NAMES=$(jq -r '.packages[].name' lake-manifest.json)
153+
for pkg in $PACKAGE_NAMES; do
154+
if [[ "$pkg" =~ ^[A-Za-z0-9_-]+$ ]]; then
155+
LEAN_SRC_PATH="$LEAN_SRC_PATH:.lake/packages/$pkg"
156+
else
157+
echo "Warning: Skipping invalid package name: $pkg"
158+
fi
159+
done
160+
147161
echo "LEAN_SRC_PATH=$LEAN_SRC_PATH"
148162
149163
# Set it as an environment variable for subsequent steps
@@ -548,8 +562,9 @@ jobs:
548562

549563
- name: build everything
550564
# make sure everything is available for test/import_all.lean
565+
# and that miscellaneous executables still work
551566
run: |
552-
lake build Batteries Qq Aesop ProofWidgets Plausible
567+
lake build Batteries Qq Aesop ProofWidgets Plausible pole unused
553568
554569
# temporarily comment out
555570
# - name: build AesopTest (nightly-testing only)

‎.github/workflows/build.yml‎

Lines changed: 20 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -32,8 +32,7 @@ env:
3232
concurrency:
3333
# label each workflow run; only the latest with each label will run
3434
# workflows on master get more expressive labels
35-
group: ${{ github.workflow }}-${{ github.ref }}.
36-
${{ ( contains(fromJSON( '["refs/heads/master", "refs/heads/staging"]'), github.ref ) && github.run_id) || ''}}
35+
group: ${{ github.workflow }}-${{ github.ref }}-${{ (contains(fromJSON('["refs/heads/master", "refs/heads/staging"]'), github.ref) && github.run_id) || '' }}
3736
# cancel any running workflow with the same label
3837
cancel-in-progress: true
3938

@@ -149,8 +148,23 @@ jobs:
149148
- name: set LEAN_SRC_PATH
150149
shell: bash
151150
run: |
152-
# Construct the LEAN_SRC_PATH using the toolchain directory
153-
LEAN_SRC_PATH=".:$TOOLCHAIN_DIR/src/lean/lake:.lake/packages/Cli:.lake/packages/batteries:.lake/packages/Qq:.lake/packages/aesop:.lake/packages/proofwidgets:.lake/packages/importGraph:.lake/packages/LeanSearchClient:.lake/packages/plausible:.lake/packages/requests:.lake/packages/openAI_client:.lake/packages/reap"
151+
cd pr-branch
152+
153+
# Start with the base paths
154+
LEAN_SRC_PATH=".:$TOOLCHAIN_DIR/src/lean/lake"
155+
156+
# Extract package names from lake-manifest.json and validate them
157+
# Only allow A-Z, a-z, 0-9, _, and - characters
158+
# Build the LEAN_SRC_PATH by appending each validated package
159+
PACKAGE_NAMES=$(jq -r '.packages[].name' lake-manifest.json)
160+
for pkg in $PACKAGE_NAMES; do
161+
if [[ "$pkg" =~ ^[A-Za-z0-9_-]+$ ]]; then
162+
LEAN_SRC_PATH="$LEAN_SRC_PATH:.lake/packages/$pkg"
163+
else
164+
echo "Warning: Skipping invalid package name: $pkg"
165+
fi
166+
done
167+
154168
echo "LEAN_SRC_PATH=$LEAN_SRC_PATH"
155169
156170
# Set it as an environment variable for subsequent steps
@@ -555,8 +569,9 @@ jobs:
555569

556570
- name: build everything
557571
# make sure everything is available for test/import_all.lean
572+
# and that miscellaneous executables still work
558573
run: |
559-
lake build Batteries Qq Aesop ProofWidgets Plausible
574+
lake build Batteries Qq Aesop ProofWidgets Plausible pole unused
560575
561576
# temporarily comment out
562577
# - name: build AesopTest (nightly-testing only)

‎.github/workflows/build_fork.yml‎

Lines changed: 20 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -29,8 +29,7 @@ env:
2929
concurrency:
3030
# label each workflow run; only the latest with each label will run
3131
# workflows on master get more expressive labels
32-
group: ${{ github.workflow }}-${{ github.ref }}.
33-
${{ ( contains(fromJSON( '["refs/heads/master", "refs/heads/staging"]'), github.ref ) && github.run_id) || ''}}
32+
group: ${{ github.workflow }}-${{ github.ref }}-${{ (contains(fromJSON('["refs/heads/master", "refs/heads/staging"]'), github.ref) && github.run_id) || '' }}
3433
# cancel any running workflow with the same label
3534
cancel-in-progress: true
3635

@@ -146,8 +145,23 @@ jobs:
146145
- name: set LEAN_SRC_PATH
147146
shell: bash
148147
run: |
149-
# Construct the LEAN_SRC_PATH using the toolchain directory
150-
LEAN_SRC_PATH=".:$TOOLCHAIN_DIR/src/lean/lake:.lake/packages/Cli:.lake/packages/batteries:.lake/packages/Qq:.lake/packages/aesop:.lake/packages/proofwidgets:.lake/packages/importGraph:.lake/packages/LeanSearchClient:.lake/packages/plausible:.lake/packages/requests:.lake/packages/openAI_client:.lake/packages/reap"
148+
cd pr-branch
149+
150+
# Start with the base paths
151+
LEAN_SRC_PATH=".:$TOOLCHAIN_DIR/src/lean/lake"
152+
153+
# Extract package names from lake-manifest.json and validate them
154+
# Only allow A-Z, a-z, 0-9, _, and - characters
155+
# Build the LEAN_SRC_PATH by appending each validated package
156+
PACKAGE_NAMES=$(jq -r '.packages[].name' lake-manifest.json)
157+
for pkg in $PACKAGE_NAMES; do
158+
if [[ "$pkg" =~ ^[A-Za-z0-9_-]+$ ]]; then
159+
LEAN_SRC_PATH="$LEAN_SRC_PATH:.lake/packages/$pkg"
160+
else
161+
echo "Warning: Skipping invalid package name: $pkg"
162+
fi
163+
done
164+
151165
echo "LEAN_SRC_PATH=$LEAN_SRC_PATH"
152166
153167
# Set it as an environment variable for subsequent steps
@@ -552,8 +566,9 @@ jobs:
552566

553567
- name: build everything
554568
# make sure everything is available for test/import_all.lean
569+
# and that miscellaneous executables still work
555570
run: |
556-
lake build Batteries Qq Aesop ProofWidgets Plausible
571+
lake build Batteries Qq Aesop ProofWidgets Plausible pole unused
557572
558573
# temporarily comment out
559574
# - name: build AesopTest (nightly-testing only)

‎Archive/Imo/Imo1982Q1.lean‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -114,7 +114,7 @@ lemma imo1982_q1 {f : ℕ+ → ℕ} (hf : IsGood f) : f 1982 = 660 := by
114114
suffices h : 3334 ≤ 3333 by simp at h
115115
calc
116116
3334 = 5 * f 1982 + 29 * f 3 + f 2 := by rw [hf.f₃, hf.f₂, hr, add_zero, mul_one]
117-
(5 : ℕ+) * f 1982 + (29 : ℕ+) * f 3 + f 2 ≤ f (5 * 1982 + 29 * 3) + f 2 :=
118-
add_le_add_right hf.superlinear _
117+
(5 : ℕ+) * f 1982 + (29 : ℕ+) * f 3 + f 2 ≤ f (5 * 1982 + 29 * 3) + f 2 := by
118+
grw [hf.superlinear]
119119
_ ≤ f (5 * 1982 + 29 * 3 + 2) := hf.superadditive
120120
_ = 3333 := hf.f_9999

‎Archive/Imo/Imo1988Q6.lean‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -233,14 +233,14 @@ theorem imo1988_q6 {a b : ℕ} (h : a * b + 1 ∣ a ^ 2 + b ^ 2) :
233233
rw [← sub_eq_zero, ← h_root]
234234
ring
235235
rw [hzx] at hpos
236-
replace hpos : z * x + 1 > 0 := pos_of_mul_pos_left hpos (Int.ofNat_zero_le k)
236+
replace hpos : z * x + 1 > 0 := pos_of_mul_pos_left hpos (Int.natCast_nonneg k)
237237
replace hpos : z * x ≥ 0 := Int.le_of_lt_add_one hpos
238238
apply nonneg_of_mul_nonneg_left hpos (mod_cast hx)
239239
· contrapose! hV₀ with x_lt_z
240240
apply ne_of_gt
241241
calc
242242
z * y > x * x := by apply mul_lt_mul' <;> omega
243-
_ ≥ x * x - k := sub_le_self _ (Int.ofNat_zero_le k)
243+
_ ≥ x * x - k := sub_le_self _ (Int.natCast_nonneg k)
244244
· -- There is no base case in this application of Vieta jumping.
245245
simp
246246

‎Archive/Imo/Imo1997Q3.lean‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -82,7 +82,7 @@ lemma sign_eq_of_contra
8282
rw [mem_compl, mem_insert, mem_singleton, not_or] at mj
8383
exact swap_apply_of_ne_of_ne mj.1 mj.2
8484
rw [cg, add_sub_add_right_eq_sub,
85-
sum_pair (castSucc_lt_succ _).ne, sum_pair (castSucc_lt_succ _).ne,
85+
sum_pair castSucc_lt_succ.ne, sum_pair castSucc_lt_succ.ne,
8686
Perm.mul_apply, Perm.mul_apply, ← hi, swap_apply_left, swap_apply_right,
8787
add_comm, add_sub_add_comm, ← sub_mul, ← sub_mul,
8888
val_succ, coe_castSucc, Nat.cast_add, Nat.cast_one, add_sub_cancel_left, sub_add_cancel_left,

‎Archive/Imo/Imo2013Q5.lean‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -178,7 +178,7 @@ theorem imo2013_q5 (f : ℚ → ℝ) (H1 : ∀ x y, 0 < x → 0 < y → f (x * y
178178
calc
179179
↑(pn + 2) * f x = (↑pn + 1 + 1) * f x := by norm_cast
180180
_ = (↑pn + 1) * f x + f x := by ring
181-
_ ≤ f (↑pn.succ * x) + f x := mod_cast add_le_add_right (hpn pn.succ_pos) (f x)
181+
_ ≤ f (↑pn.succ * x) + f x := by norm_cast; grw [hpn pn.succ_pos]
182182
_ ≤ f ((↑pn + 1) * x + x) := by exact_mod_cast H2 _ _ (mul_pos pn.cast_add_one_pos hx) hx
183183
_ = f ((↑pn + 1 + 1) * x) := by ring_nf
184184
_ = f (↑(pn + 2) * x) := by norm_cast

‎Archive/Imo/Imo2024Q5.lean‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -387,7 +387,7 @@ lemma Path.findFstEq_fst_sub_one_mem (p : Path N) {r : Fin (N + 2)} (hr : r ≠
387387
rw [← cells.takeWhile_append_dropWhile (p := fun c ↦ ! decide (r ≤ c.1)),
388388
List.isChain_append] at valid_move_seq
389389
have ha := valid_move_seq.2.2
390-
simp only [List.head?_eq_head hd', List.getLast?_eq_getLast ht, Option.mem_def,
390+
simp only [List.head?_eq_some_head hd', List.getLast?_eq_some_getLast ht, Option.mem_def,
391391
Option.some.injEq, forall_eq'] at ha
392392
nth_rw 1 [← cells.takeWhile_append_dropWhile (p := fun c ↦ ! decide (r ≤ c.1))]
393393
refine List.mem_append_left _ ?_

‎Archive/Wiedijk100Theorems/BallotProblem.lean‎

Lines changed: 8 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -114,15 +114,17 @@ theorem counted_succ_succ (p q : ℕ) :
114114
obtain ⟨hl₀, hl₁, hl₂⟩ := hl
115115
obtain hlast | hlast := hl₂ (l.head hlnil) (List.head_mem hlnil)
116116
· refine Or.inl ⟨l.tail, ⟨?_, ?_, ?_⟩, ?_⟩
117-
· rw [List.count_tail, hl₀, List.head?_eq_head hlnil, hlast, beq_self_eq_true, if_pos rfl,
118-
Nat.add_sub_cancel]
119-
· rw [List.count_tail, hl₁, List.head?_eq_head hlnil, hlast, if_neg (by decide), Nat.sub_zero]
117+
· rw [List.count_tail, hl₀, List.head?_eq_some_head hlnil, hlast, beq_self_eq_true,
118+
if_pos rfl, Nat.add_sub_cancel]
119+
· rw [List.count_tail, hl₁, List.head?_eq_some_head hlnil, hlast, if_neg (by decide),
120+
Nat.sub_zero]
120121
· exact fun x hx => hl₂ x (List.mem_of_mem_tail hx)
121122
· rw [← hlast, List.cons_head_tail]
122123
· refine Or.inr ⟨l.tail, ⟨?_, ?_, ?_⟩, ?_⟩
123-
· rw [List.count_tail, hl₀, List.head?_eq_head hlnil, hlast, if_neg (by decide), Nat.sub_zero]
124-
· rw [List.count_tail, hl₁, List.head?_eq_head hlnil, hlast, beq_self_eq_true, if_pos rfl,
125-
Nat.add_sub_cancel]
124+
· rw [List.count_tail, hl₀, List.head?_eq_some_head hlnil, hlast, if_neg (by decide),
125+
Nat.sub_zero]
126+
· rw [List.count_tail, hl₁, List.head?_eq_some_head hlnil, hlast, beq_self_eq_true,
127+
if_pos rfl, Nat.add_sub_cancel]
126128
· exact fun x hx => hl₂ x (List.mem_of_mem_tail hx)
127129
· rw [← hlast, List.cons_head_tail]
128130
· rintro (⟨t, ⟨ht₀, ht₁, ht₂⟩, rfl⟩ | ⟨t, ⟨ht₀, ht₁, ht₂⟩, rfl⟩)

0 commit comments

Comments
 (0)