Skip to content

Commit ea81ce6

Browse files
tb65536tb65536
committed
merge
2 parents 65e2375 + 3e81059 commit ea81ce6

120 files changed

Lines changed: 3380 additions & 948 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/actions/cache-trust-dispatch/action.yml‎

Lines changed: 58 additions & 26 deletions
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
# Single source of truth mapping (repo, branch) → (upload container,
1+
# Single source of truth mapping (repo, ref) → (upload container,
22
# read fallback chain) for Mathlib's multi-container cache.
33
#
44
# Called by build, upload_cache, and post_steps in build_template.yml so
@@ -14,7 +14,10 @@ inputs:
1414
description: GitHub repo full name (`owner/name`).
1515
required: true
1616
branch:
17-
description: Branch name (`github.head_ref || github.ref_name`).
17+
description: |
18+
Branch name (`github.head_ref || github.ref_name`); on tag-triggered
19+
runs this is the tag name, distinguished via `github.ref_type` inside
20+
the dispatch step.
1821
required: true
1922
head-sha:
2023
description: |
@@ -55,6 +58,10 @@ runs:
5558
REPO="${{ inputs.repo }}"
5659
BRANCH="${{ inputs.branch }}"
5760
HEAD_SHA="${{ inputs.head-sha }}"
61+
# Whether `branch` names a branch or a tag. Read from the run context
62+
# rather than an input: unlike `repo`/`branch`, the value does not
63+
# depend on which event shape (PR vs push) the caller handles.
64+
REF_TYPE="${{ github.ref_type }}"
5865
PRIMARY=""
5966
READ_CHAIN=""
6067
REPO_SCOPE=""
@@ -80,30 +87,55 @@ runs:
8087
else
8188
case "$REPO" in
8289
"leanprover-community/mathlib4")
83-
case "$BRANCH" in
84-
"master"|"staging")
85-
# Master / staging are the only writers that feed `master`
86-
# (`staging` is bors's merge candidate, which fast-forwards to
87-
# `master`). Read `master` only, not the default [master,
88-
# legacy]: files the read chain serves are skipped at stage
89-
# time, so keeping `legacy` would leave legacy-only files out of
90-
# `master` for good. Reading `master` alone turns them into
91-
# misses that get rebuilt and uploaded, so `master` fills itself
92-
# into a standalone cache. (Only PRIMARY=master does this; other
93-
# runs write to `forks` and keep the wider chain.)
94-
PRIMARY="master"
95-
READ_CHAIN="master"
96-
;;
97-
*)
98-
# `bors trying`, `ci-dev/*`, maintainer dev branches on the
99-
# canonical repo: trust level is fork-equivalent (the OIDC
100-
# token's RBAC scopes them to `forks`). Reads must widen
101-
# past the default [master, legacy] so the post-build
102-
# verification finds the just-uploaded fork-trust artifacts.
103-
PRIMARY="forks"
104-
READ_CHAIN="master,forks,legacy"
105-
;;
106-
esac
90+
if [ "$REF_TYPE" = "tag" ]; then
91+
case "$BRANCH" in
92+
v4.*)
93+
# `v4.*` release tags: release_cache.yml rebuilds off-master
94+
# release commits (patch releases, patched release
95+
# candidates) and publishes them into `master`, the container
96+
# canonical checkouts read. Tag creation is restricted to
97+
# release managers by a tag ruleset, and the
98+
# `cache-upload-master` environment admits `v4.*` tag refs,
99+
# so these builds carry master trust. Reads are `master`-only
100+
# for the same fill-in reason as the master/staging arm
101+
# below.
102+
PRIMARY="master"
103+
READ_CHAIN="master"
104+
;;
105+
*)
106+
# Other tags have no trust class of their own:
107+
# fork-equivalent, like the dev-branch arm below.
108+
PRIMARY="forks"
109+
READ_CHAIN="master,forks,legacy"
110+
;;
111+
esac
112+
else
113+
case "$BRANCH" in
114+
"master"|"staging")
115+
# Master, staging, and `v4.*` release tags (above) are the
116+
# only writers that feed `master` (`staging` is bors's merge
117+
# candidate, which fast-forwards to `master`). Read `master`
118+
# only, not the default [master, legacy]: files the read
119+
# chain serves are skipped at stage time, so keeping `legacy`
120+
# would leave legacy-only files out of `master` for good.
121+
# Reading `master` alone turns them into misses that get
122+
# rebuilt and uploaded, so `master` fills itself into a
123+
# standalone cache. (Only PRIMARY=master does this; other
124+
# runs write to `forks` and keep the wider chain.)
125+
PRIMARY="master"
126+
READ_CHAIN="master"
127+
;;
128+
*)
129+
# `bors trying`, `ci-dev/*`, maintainer dev branches on the
130+
# canonical repo: trust level is fork-equivalent (the OIDC
131+
# token's RBAC scopes them to `forks`). Reads must widen
132+
# past the default [master, legacy] so the post-build
133+
# verification finds the just-uploaded fork-trust artifacts.
134+
PRIMARY="forks"
135+
READ_CHAIN="master,forks,legacy"
136+
;;
137+
esac
138+
fi
107139
;;
108140
"leanprover-community/mathlib4-nightly-testing")
109141
case "$BRANCH" in

‎.github/workflows/build_template.yml‎

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,5 @@
1-
# Reusable workflow invoked by build.yml, bors.yml, build_fork.yml, and ci_dev.yml.
1+
# Reusable workflow invoked by build.yml, bors.yml, build_fork.yml, ci_dev.yml,
2+
# and release_cache.yml.
23

34
on:
45
workflow_call:

‎.github/workflows/release_cache.yml‎

Lines changed: 103 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,103 @@
1+
name: publish release cache
2+
3+
# Publishes the Mathlib cache for release tags whose commits are not on
4+
# `master`.
5+
#
6+
# Patch releases (`v4.X.Y` with Y ≥ 1) and patched release candidates (e.g.
7+
# `v4.32.0-rc1-patch1`) are committed on `bump_to_*` branches that never merge
8+
# back into `master`, so the master push build never caches them; their branch
9+
# CI writes only the fork-trust container, which a canonical checkout at the
10+
# tag never reads. This workflow rebuilds the tagged commit and publishes the
11+
# result to the `master` container, where every consumer finds it. Tags that
12+
# point at commits on `master` (plain release candidates and `.0` releases)
13+
# are already cached by the master push build, so the gate job skips them.
14+
#
15+
# Trust model:
16+
# - Creating a `v4.*` tag is restricted to release managers by a tag
17+
# ruleset, so a tag push is a deliberate release-manager action — and the
18+
# tagged tree is what runs here, including this workflow file. Tags cut
19+
# from lineages predating this file simply never trigger it.
20+
# - The upload job mints its OIDC token under the `cache-upload-master`
21+
# environment (inside build_template.yml); the environment's deployment
22+
# policy admits only `master`, `staging`, and `v4.*` tag refs.
23+
#
24+
# Retry: a spuriously failed run can simply be re-run ("Re-run failed jobs" /
25+
# `gh run rerun`) — same tag, same tree, no tag re-push involved. The
26+
# `workflow_dispatch` trigger covers what re-run cannot: a tag push that never
27+
# produced a run, or a re-run window that has expired. Dispatch it AT the tag
28+
# ref (`gh workflow run release_cache.yml --ref v4.X.Y`); the run then executes
29+
# the tag's own tree exactly as a tag push would.
30+
31+
on:
32+
push:
33+
tags:
34+
- 'v4.*'
35+
# Manual fallback; see the retry note above. The `tags` filter does not
36+
# apply to dispatches — the gate job's ref guards enforce it instead, so a
37+
# dispatch on a branch ref skips cleanly.
38+
workflow_dispatch:
39+
40+
# `v4.*` tags are immutable (the tag ruleset blocks updates), so this group
41+
# only ever collides on re-runs of the same tag; keep those queued rather
42+
# than cancelled.
43+
concurrency:
44+
group: ${{ github.workflow }}-${{ github.ref }}
45+
46+
# Read-only by default; the build job elevates for itself only.
47+
permissions:
48+
contents: read
49+
50+
jobs:
51+
gate:
52+
name: skip tags already on master
53+
# The ref guards double as the dispatch-path filter; on the push path the
54+
# `tags` trigger filter has already enforced them.
55+
if: ${{ github.repository == 'leanprover-community/mathlib4' && github.ref_type == 'tag' && startsWith(github.ref_name, 'v4.') }}
56+
runs-on: ubuntu-latest
57+
outputs:
58+
off_master: ${{ steps.check.outputs.off_master }}
59+
steps:
60+
- uses: actions/checkout@9c091bb21b7c1c1d1991bb908d89e4e9dddfe3e0 # v7.0.0
61+
with:
62+
# `merge-base` needs history, so fetch all of it.
63+
fetch-depth: 0
64+
65+
- name: check whether the tagged commit is on master
66+
id: check
67+
run: |
68+
if git merge-base --is-ancestor "$GITHUB_SHA" origin/master; then
69+
echo "Tag $GITHUB_REF_NAME points at a commit on master; the master push build covers its cache."
70+
echo "off_master=false" >> "$GITHUB_OUTPUT"
71+
else
72+
echo "Tag $GITHUB_REF_NAME is not on master; rebuilding it to publish its cache."
73+
echo "off_master=true" >> "$GITHUB_OUTPUT"
74+
fi
75+
76+
build:
77+
name: ci
78+
needs: gate
79+
if: ${{ needs.gate.outputs.off_master == 'true' }}
80+
# What build_template.yml needs, granted to this job only — the same set
81+
# build.yml grants it on push events. In particular, the OIDC token for
82+
# the cache upload can be minted here and nowhere else in this workflow.
83+
permissions:
84+
contents: read
85+
id-token: write
86+
actions: read # Allow get-tools to download the prebuilt tools artifact from master's publish_tools runs
87+
pull-requests: write # Only allow PR comments/labels
88+
uses: ./.github/workflows/build_template.yml
89+
with:
90+
concurrency_group: ${{ github.workflow }}-${{ github.ref }}
91+
pr_branch_ref: ${{ github.sha }}
92+
# Release tags publish to the `master` container under the master writer
93+
# identity; see the trust note above and cache-trust-dispatch, which
94+
# routes `v4.*` tag refs to that container.
95+
cache_application_id: ${{ vars.CACHE_MASTER_WRITER_AZURE_APP_ID }}
96+
cache_environment: cache-upload-master
97+
# The cache-snapshot warming artifact exists to seed master and PR
98+
# builds, which a release tag's snapshot cannot do.
99+
publish_cache: false
100+
# Skip the Post-CI job: it grooms PR labels, and a tag run has no PR.
101+
run_post_ci: false
102+
runs_on: pr
103+
secrets: inherit

‎Archive/Imo/Imo2000Q2.lean‎

Lines changed: 45 additions & 60 deletions
Original file line numberDiff line numberDiff line change
@@ -17,21 +17,14 @@ We follow the first solution from
1717
<https://artofproblemsolving.com/wiki/index.php?title=2000_IMO_Problems/Problem_2>.
1818
1919
We parametrize `A = x / y`, `B = y / z`, `C = z / x` where `x, y, z > 0`.
20-
This reduces the problem to proving `(x - y + z)(y - z + x)(z - x + y) ≤ 8xyz`.
20+
This reduces the problem to proving `(x - y + z)(y - z + x)(z - x + y) ≤ xyz`.
2121
22-
We then reparametrize `x = q + r`, `y = r + p`, `z = p + q` where `p, q, r ∈ ℝ`,
23-
which transforms the inequality to `8pqr ≤ (q + r)(r + p)(p + q)`.
24-
25-
The proof splits into cases based on the signs of `p`, `q`, `r`.
26-
When all are positive, AM-GM gives the result.
27-
When at least one is negative or zero, the inequality is verified by sign analysis.
28-
29-
## Implementation notes
30-
31-
- The inequality is reduced via `A = x / y`, `B = y / z`, `C = z / x`, then the substitution
32-
`x = q + r`, `y = r + p`, `z = p + q`.
33-
- Helper lemmas prove `8pqr ≤ (p + q)(r + p)(q + r)` by AM-GM when `p, q, r > 0` and by sign
34-
analysis otherwise; the main proof closes with `grind`.
22+
Writing `u = x - y + z`, `v = y - z + x`, `w = z - x + y`, we have `u + v = 2x`,
23+
`v + w = 2y`, `w + u = 2z`, so any two of `u`, `v`, `w` have a positive sum and hence
24+
at most one of them can be nonpositive. If one is nonpositive the left-hand side is
25+
nonpositive and the inequality is clear. Otherwise all three are positive, and by AM-GM
26+
`uv ≤ ((u + v) / 2) ^ 2 = x ^ 2`, and similarly `vw ≤ y ^ 2` and `wu ≤ z ^ 2`; multiplying
27+
these gives `(uvw) ^ 2 ≤ (xyz) ^ 2`, from which the inequality follows.
3528
3629
## References
3730
@@ -41,48 +34,39 @@ When at least one is negative or zero, the inequality is verified by sign analys
4134

4235
namespace Imo2000Q2
4336

44-
/-- When `p`, `q`, `r > 0`, `8pqr ≤ (p + q)(r + p)(q + r)`, by writing the difference of squares as
45-
a sum of nonnegative squares. -/
46-
lemma eight_mul_le_prod_add_of_pos {p q r : ℝ} (p_pos : 0 < p)
47-
(q_pos : 0 < q) (r_pos : 0 < r) :
48-
8 * p * q * r ≤ (p + q) * (q + r) * (r + p) := by
49-
suffices 0 ≤ ((p + q) * (q + r) * (r + p)) ^ 2 - (8 * p * q * r) ^ 2 from
50-
le_of_sq_le_sq (le_of_sub_nonneg this) (by positivity)
51-
calc 0 ≤ (p * (q - r) ^ 2 + q * (r - p) ^ 2 + r * (p - q) ^ 2)
52-
* ((p + q) * (q + r) * (r + p) + 8 * p * q * r) := by positivity
53-
_ = ((p + q) * (q + r) * (r + p)) ^ 2 - (8 * p * q * r) ^ 2 := by ring
54-
55-
/-- When `p ≤ 0` but `q`, `r > 0` and both pairwise sums are positive, the left side is
56-
nonpositive so the inequality holds. -/
57-
lemma eight_mul_le_prod_add_of_nonpos {p q r : ℝ} (p_nonpos : p ≤ 0) (r_pos : 0 < r) (q_pos : 0 < q)
58-
(p_add_q_pos : 0 < p + q) (r_add_p_pos : 0 < r + p) :
59-
8 * p * q * r ≤ (p + q) * (r + p) * (q + r) := by
60-
calc 8 * p * q * r ≤ 0 := by grw [mul_nonpos_of_nonpos_of_nonneg ?_ (by positivity)]
61-
grw [mul_nonpos_of_nonpos_of_nonneg (by grind) (by positivity)]
62-
_ ≤ (p + q) * (r + p) * (q + r) := by positivity
63-
64-
/-- When all three pairwise sums `p + q`, `r + p`, `q + r` are positive, the inequality holds by
65-
casing on the signs of `p`, `q`, `r`. -/
66-
lemma eight_mul_le_prod_add_of_add_pos (p q r : ℝ)
67-
(hpq : 0 < p + q := by grind)
68-
(hqr : 0 < q + r := by grind)
69-
(hrp : 0 < r + p := by grind) :
70-
8 * p * q * r ≤ (p + q) * (q + r) * (r + p) := by
71-
rcases lt_or_ge 0 p with p_pos | p_nonpos <;>
72-
rcases lt_or_ge 0 q with q_pos | q_nonpos <;>
73-
rcases lt_or_ge 0 r with r_pos | r_nonpos
74-
-- At most one of `p`, `q`, `r` can be negative; otherwise some pairwise sum is nonpositive.
75-
· exact eight_mul_le_prod_add_of_pos p_pos q_pos r_pos
76-
· -- `r` is the unique nonpositive variable.
77-
convert eight_mul_le_prod_add_of_nonpos r_nonpos q_pos p_pos hrp hqr using 1 <;> ring
78-
· -- `q` is the unique nonpositive variable.
79-
convert eight_mul_le_prod_add_of_nonpos q_nonpos p_pos r_pos hqr hpq using 1 <;> ring
80-
· linarith
81-
· -- `p` is the unique nonpositive variable.
82-
convert eight_mul_le_prod_add_of_nonpos p_nonpos r_pos q_pos hpq hrp using 1; ring
83-
· linarith
84-
· linarith
85-
· linarith
37+
/-- For positive reals `x`, `y`, `z` we have `(x - y + z)(y - z + x)(z - x + y) ≤ xyz`. -/
38+
lemma prod_sub_add_le {x y z : ℝ} (hx : 0 < x) (hy : 0 < y) (hz : 0 < z) :
39+
(x - y + z) * (y - z + x) * (z - x + y) ≤ x * y * z := by
40+
-- At most one of the three factors can be nonpositive, since any two of them
41+
-- sum to twice one of `x`, `y`, `z`. If one is nonpositive, so is the product.
42+
rcases le_or_gt (x - y + z) 0 with hu | hu
43+
· have hv : 0 < y - z + x := by linarith
44+
have hw : 0 < z - x + y := by linarith
45+
calc (x - y + z) * (y - z + x) * (z - x + y)
46+
≤ 0 := mul_nonpos_of_nonpos_of_nonneg
47+
(mul_nonpos_of_nonpos_of_nonneg hu hv.le) hw.le
48+
_ ≤ x * y * z := by positivity
49+
rcases le_or_gt (y - z + x) 0 with hv | hv
50+
· have hw : 0 < z - x + y := by linarith
51+
calc (x - y + z) * (y - z + x) * (z - x + y)
52+
≤ 0 := mul_nonpos_of_nonpos_of_nonneg
53+
(mul_nonpos_of_nonneg_of_nonpos hu.le hv) hw.le
54+
_ ≤ x * y * z := by positivity
55+
rcases le_or_gt (z - x + y) 0 with hw | hw
56+
· calc (x - y + z) * (y - z + x) * (z - x + y)
57+
≤ 0 := mul_nonpos_of_nonneg_of_nonpos (mul_nonneg hu.le hv.le) hw
58+
_ ≤ x * y * z := by positivity
59+
-- All three factors are positive. By AM-GM each pairwise product is bounded by a square:
60+
have h1 : (x - y + z) * (y - z + x) ≤ x ^ 2 := by linarith [sq_nonneg (y - z)]
61+
have h2 : (y - z + x) * (z - x + y) ≤ y ^ 2 := by linarith [sq_nonneg (z - x)]
62+
have h3 : (z - x + y) * (x - y + z) ≤ z ^ 2 := by linarith [sq_nonneg (x - y)]
63+
-- Multiplying the three bounds gives the squared inequality, and both sides are positive.
64+
refine le_of_sq_le_sq ?_ (by positivity)
65+
calc ((x - y + z) * (y - z + x) * (z - x + y)) ^ 2
66+
= ((x - y + z) * (y - z + x)) * ((y - z + x) * (z - x + y))
67+
* ((z - x + y) * (x - y + z)) := by ring
68+
_ ≤ x ^ 2 * y ^ 2 * z ^ 2 := by gcongr
69+
_ = (x * y * z) ^ 2 := by ring
8670

8771
/-- **IMO 2000 Q2**. If `A`, `B`, `C > 0` and `ABC = 1`, then
8872
`(A - 1 + 1 / B)(B - 1 + 1 / C)(C - 1 + 1 / A) ≤ 1`. -/
@@ -92,9 +76,10 @@ theorem imo2000_q2 {A B C : ℝ}
9276
obtain ⟨x, y, z, x_pos, y_pos, z_pos, rfl, rfl, rfl⟩ :
9377
∃ x y z, 0 < x ∧ 0 < y ∧ 0 < z ∧ A = x / y ∧ B = y / z ∧ C = z / x :=
9478
⟨A, 1, 1 / B, by grind only [inv_pos]⟩
95-
-- If `x = q + r`, `y = r + p`, `z = p + q`, it suffices to show `8pqr ≤ (q + r)(r + p)(p + q)`.
96-
have := eight_mul_le_prod_add_of_add_pos ((y + z - x) / 2) ((z + x - y) / 2) ((x + y - z) / 2)
97-
field_simp
98-
grind
79+
have key : (x / y - 1 + 1 / (y / z)) * (y / z - 1 + 1 / (z / x)) * (z / x - 1 + 1 / (x / y))
80+
= (x - y + z) * (y - z + x) * (z - x + y) / (x * y * z) := by
81+
field_simp
82+
rw [key, div_le_one (by positivity)]
83+
exact prod_sub_add_le x_pos y_pos z_pos
9984

10085
end Imo2000Q2

‎Cache/SECURITY.md‎

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -21,7 +21,7 @@ CI job and assigned a trust level:
2121

2222
| Container | Who may write | Trust |
2323
|-----------------------|--------------------------------------------------------|--------|
24-
| `master` | mathlib4 `master`/`staging` | high |
24+
| `master` | mathlib4 `master`/`staging`, `v4.*` release tags | high |
2525
| `forks` | mathlib4 PR builds, non-master branches, `bors try` | medium |
2626
| `nightly-testing` | nightly-testing's trusted branches | medium |
2727
| `pr-toolchain-tests` | nightly-testing's experimental toolchain branches | low |
@@ -148,5 +148,5 @@ The trust model does not attempt to defend against:
148148
| Trust property tests | [`Cache/Test.lean`](Test.lean) |
149149
| User-facing CLI surface, env vars | [`Cache/Main.lean`](Main.lean), [`Cache/README.md`](README.md) |
150150
| OIDC mint + per-job dispatch | [`.github/workflows/build_template.yml`](../.github/workflows/build_template.yml) (`upload_cache` job) |
151-
| (repo, branch) → trust class policy table | [`.github/actions/cache-trust-dispatch/action.yml`](../.github/actions/cache-trust-dispatch/action.yml) |
152-
| Caller `cache_application_id` ternaries | [`.github/workflows/build.yml`](../.github/workflows/build.yml), [`bors.yml`](../.github/workflows/bors.yml), [`build_fork.yml`](../.github/workflows/build_fork.yml), [`ci_dev.yml`](../.github/workflows/ci_dev.yml) |
151+
| (repo, ref) → trust class policy table | [`.github/actions/cache-trust-dispatch/action.yml`](../.github/actions/cache-trust-dispatch/action.yml) |
152+
| Caller `cache_application_id` wiring | [`.github/workflows/build.yml`](../.github/workflows/build.yml), [`bors.yml`](../.github/workflows/bors.yml), [`build_fork.yml`](../.github/workflows/build_fork.yml), [`ci_dev.yml`](../.github/workflows/ci_dev.yml), [`release_cache.yml`](../.github/workflows/release_cache.yml) |

‎Counterexamples/AharoniKorman.lean‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -794,7 +794,7 @@ theorem apply_eq_of_line_eq (f : SpinalMap C) {n : ℕ} (hC : IsChain (· ≤ ·
794794
have hy : y ∈ level n := ordConnected_level.out hlo.2 hhi.2 ⟨h₂l, h₂h⟩
795795
induction hx using induction_on_level with | h x₁ y₁ =>
796796
induction hy using induction_on_level with | h x₂ y₂ =>
797-
simp only [] at hxy
797+
simp only at hxy
798798
simp only [line_toHollom] at h
799799
obtain ⟨k, rfl⟩ := exists_add_of_le hxy
800800
obtain rfl : y₂ = y₁ + k := by lia

0 commit comments

Comments
 (0)