Trigger CI for leanprover-community/batteries#1099

.github/build.in.yml

@@ -322,6 +322,15 @@ jobs:
           cp ../lean-toolchain .
           lake build
 
+      - name: Add the "awaiting-CI" label
+        if: always()
+        # we use curl rather than octokit/request-action so that the job won't fail
+        # (and send an annoying email) if the labels don't exist
+        run: |
+          curl --request ADD \
+            --url https://api.github.com/repos/${{ github.repository }}/issues/${{ github.event.issue.number }}/labels/awaiting-CI \
+            --header 'authorization: Bearer ${{ secrets.GITHUB_TOKEN }}'
+
   final:
     name: Post-CI jobJOB_NAME
     if: github.repository MAIN_OR_FORK 'leanprover-community/mathlib4'
@@ -339,6 +348,15 @@ jobs:
           # Only return if PR is still open
           filterOutClosed: true
 
+      - if: contains(steps.PR.outputs.pr_labels, 'bench-after-CI')
+        name: If `bench-after-CI` is present, add a `!bench` comment.
+        uses: GrantBirki/comment@v2
+        with:
+          token: ${{ secrets.AUTO_MERGE_TOKEN }}
+          issue-number: ${{ steps.PR.outputs.number }}
+          body: |
+            !bench
+
       - id: remove_labels
         name: Remove "awaiting-CI"
         # we use curl rather than octokit/request-action so that the job won't fail

.github/workflows/PR_summary.yml

@@ -121,7 +121,7 @@ jobs:
         techDebtVar="$(./scripts/technical-debt-metrics.sh pr_summary)"
 
         # store in a file, to avoid "long arguments" error.
-        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}" > messageFile.md
+        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
 
-        cat messageFile.md
-        ./scripts/update_PR_comment.sh messageFile.md "${title}" "${PR}"
+        cat please_merge_master.md
+        ./scripts/update_PR_comment.sh please_merge_master.md "${title}" "${PR}"

.github/workflows/bench_summary_comment.yml

@@ -33,3 +33,11 @@ jobs:
         env:
           PR:  ${{ github.event.issue.number }}
           GH_TOKEN: ${{secrets.GITHUB_TOKEN}}
+
+      - name: Remove "bench-after-CI"
+        # we use curl rather than octokit/request-action so that the job won't fail
+        # (and send an annoying email) if the labels don't exist
+        run: |
+          curl --request DELETE \
+            --url https://api.github.com/repos/${{ github.repository }}/issues/${{ github.event.issue.number }}/labels/bench-after-CI \
+            --header 'authorization: Bearer ${{ secrets.GITHUB_TOKEN }}'

.github/workflows/bors.yml

@@ -332,6 +332,15 @@ jobs:
           cp ../lean-toolchain .
           lake build
 
+      - name: Add the "awaiting-CI" label
+        if: always()
+        # we use curl rather than octokit/request-action so that the job won't fail
+        # (and send an annoying email) if the labels don't exist
+        run: |
+          curl --request ADD \
+            --url https://api.github.com/repos/${{ github.repository }}/issues/${{ github.event.issue.number }}/labels/awaiting-CI \
+            --header 'authorization: Bearer ${{ secrets.GITHUB_TOKEN }}'
+
   final:
     name: Post-CI job
     if: github.repository == 'leanprover-community/mathlib4'
@@ -349,6 +358,15 @@ jobs:
           # Only return if PR is still open
           filterOutClosed: true
 
+      - if: contains(steps.PR.outputs.pr_labels, 'bench-after-CI')
+        name: If `bench-after-CI` is present, add a `!bench` comment.
+        uses: GrantBirki/comment@v2
+        with:
+          token: ${{ secrets.AUTO_MERGE_TOKEN }}
+          issue-number: ${{ steps.PR.outputs.number }}
+          body: |
+            !bench
+
       - id: remove_labels
         name: Remove "awaiting-CI"
         # we use curl rather than octokit/request-action so that the job won't fail

.github/workflows/build.yml

@@ -339,6 +339,15 @@ jobs:
           cp ../lean-toolchain .
           lake build
 
+      - name: Add the "awaiting-CI" label
+        if: always()
+        # we use curl rather than octokit/request-action so that the job won't fail
+        # (and send an annoying email) if the labels don't exist
+        run: |
+          curl --request ADD \
+            --url https://api.github.com/repos/${{ github.repository }}/issues/${{ github.event.issue.number }}/labels/awaiting-CI \
+            --header 'authorization: Bearer ${{ secrets.GITHUB_TOKEN }}'
+
   final:
     name: Post-CI job
     if: github.repository == 'leanprover-community/mathlib4'
@@ -356,6 +365,15 @@ jobs:
           # Only return if PR is still open
           filterOutClosed: true
 
+      - if: contains(steps.PR.outputs.pr_labels, 'bench-after-CI')
+        name: If `bench-after-CI` is present, add a `!bench` comment.
+        uses: GrantBirki/comment@v2
+        with:
+          token: ${{ secrets.AUTO_MERGE_TOKEN }}
+          issue-number: ${{ steps.PR.outputs.number }}
+          body: |
+            !bench
+
       - id: remove_labels
         name: Remove "awaiting-CI"
         # we use curl rather than octokit/request-action so that the job won't fail

.github/workflows/build_fork.yml

@@ -336,6 +336,15 @@ jobs:
           cp ../lean-toolchain .
           lake build
 
+      - name: Add the "awaiting-CI" label
+        if: always()
+        # we use curl rather than octokit/request-action so that the job won't fail
+        # (and send an annoying email) if the labels don't exist
+        run: |
+          curl --request ADD \
+            --url https://api.github.com/repos/${{ github.repository }}/issues/${{ github.event.issue.number }}/labels/awaiting-CI \
+            --header 'authorization: Bearer ${{ secrets.GITHUB_TOKEN }}'
+
   final:
     name: Post-CI job (fork)
     if: github.repository != 'leanprover-community/mathlib4'
@@ -353,6 +362,15 @@ jobs:
           # Only return if PR is still open
           filterOutClosed: true
 
+      - if: contains(steps.PR.outputs.pr_labels, 'bench-after-CI')
+        name: If `bench-after-CI` is present, add a `!bench` comment.
+        uses: GrantBirki/comment@v2
+        with:
+          token: ${{ secrets.AUTO_MERGE_TOKEN }}
+          issue-number: ${{ steps.PR.outputs.number }}
+          body: |
+            !bench
+
       - id: remove_labels
         name: Remove "awaiting-CI"
         # we use curl rather than octokit/request-action so that the job won't fail

.github/workflows/daily.yml

@@ -37,6 +37,10 @@ jobs:
           ./elan-init -y --default-toolchain none
           echo "$HOME/.elan/bin" >> "${GITHUB_PATH}"
 
+      # Checkout repository, so that we can fetch tags to decide which branch we want.
+      - name: Checkout branch or tag
+        uses: actions/checkout@v4
+
       - name: Fetch latest tags (if nightly)
         if: matrix.branch_type == 'nightly'
         run: |
@@ -52,6 +56,7 @@ jobs:
             echo "BRANCH_REF=${{ env.LATEST_TAG }}" >> "$GITHUB_ENV"
           fi
 
+      # Checkout the branch or tag we want to test.
       - name: Checkout branch or tag
         uses: actions/checkout@v4
         with:

.github/workflows/maintainer_bors.yml

@@ -34,14 +34,19 @@ jobs:
           printf '%s' "${COMMENT}" | hexdump -cC
           printf 'Comment:"%s"\n' "${COMMENT}"
           m_or_d="$(printf '%s' "${COMMENT}" |
-            sed -n 's=^bors  *\(merge\|r+\) *$=ready-to-merge=p; s=^bors  *d.*=delegated=p' | head -1)"
+            sed -n 's=^bors  *\(merge\|r+\) *$=ready-to-merge=p; s=^bors  *\(delegate\|d+\|d\=\).*=delegated=p' | head -1)"
+
+          remove_labels="$(printf '%s' "${COMMENT}" |
+            sed -n 's=^bors  *\(merge\|r\|d\)- *$=remove-labels=p' | head -1)"
 
           printf $'"bors delegate" or "bors merge" found? \'%s\'\n' "${m_or_d}"
+          printf $'"bors r-" or "bors d-" found? \'%s\'\n' "${remove_labels}"
           printf $'AUTHOR: \'%s\'\n' "${AUTHOR}"
           printf $'PR_NUMBER: \'%s\'\n' "${{ github.event.issue.number }}${{ github.event.pull_request.number }}"
           printf $'%s' "${{ github.event.issue.number }}${{ github.event.pull_request.number }}" | hexdump -cC
 
           printf $'mOrD=%s\n' "${m_or_d}" >> "${GITHUB_OUTPUT}"
+          printf $'removeLabels=%s\n' "${remove_labels}" >> "${GITHUB_OUTPUT}"
           if [ "${AUTHOR}" == 'leanprover-community-mathlib4-bot' ] ||
              [ "${AUTHOR}" == 'leanprover-community-bot-assistant' ]
           then
@@ -54,7 +59,7 @@ jobs:
 
       - name: Check whether user is a mathlib admin
         id: user_permission
-        if: ${{ ! steps.merge_or_delegate.outputs.mOrD == '' }}
+        if: ${{ ! steps.merge_or_delegate.outputs.mOrD == '' || ! steps.merge_or_delegate.outputs.removeLabels == '' }}
         uses: actions-cool/check-user-permission@v2
         with:
           require: 'admin'
@@ -87,6 +92,18 @@ jobs:
               --header 'authorization: Bearer ${{ secrets.TRIAGE_TOKEN }}'
           done
 
+      - name: On bors r/d-, remove ready-to-merge or delegated label
+        if: ${{ ! steps.merge_or_delegate.outputs.removeLabels == '' &&
+          steps.user_permission.outputs.require-result == 'true' }}
+        # we use curl rather than octokit/request-action so that the job won't fail
+        # (and send an annoying email) if the labels don't exist
+        run: |
+          for label in ready-to-merge delegated; do
+            curl --request DELETE \
+              --url "https://api.github.com/repos/${{ github.repository }}/issues/${{ github.event.issue.number }}${{ github.event.pull_request.number }}/labels/${label}" \
+              --header 'authorization: Bearer ${{ secrets.TRIAGE_TOKEN }}'
+          done
+
       - name: Set up Python
         if: ${{ ! steps.merge_or_delegate.outputs.mOrD == '' &&
           ( steps.user_permission.outputs.require-result == 'true' ||

.github/workflows/stale.yml

@@ -18,8 +18,8 @@ jobs:
           close-pr-message: 'Comment on the staled PRs while closed'
           days-before-stale: 60
           days-before-close: 120
-          # search string from the Zulip #queue link at https://bit.ly/4eo6brN
-          # "is:open is:pr -is:draft base:master sort:updated-asc status:success -label:blocked-by-other-PR -label:merge-conflict -label:awaiting-CI -label:WIP -label:awaiting-author -label:delegated -label:auto-merge-after-CI -label:ready-to-merge -label:please-adopt -label:help-wanted -label:awaiting-zulip"
+          # search string from the Zulip #queue link at https://leanprover-community.github.io/queue-redirect
+          # "is:open is:pr -is:draft base:master sort:updated-asc status:success -label:blocked-by-other-PR -label:blocked-by-batt-PR -label:blocked-by-core-PR -label:blocked-by-qq-PR -label:merge-conflict -label:awaiting-author -label:awaiting-CI -label:awaiting-zulip -label:WIP -label:delegated -label:auto-merge-after-CI -label:ready-to-merge -label:please-adopt -label:help-wanted"
           # We want PRs _not_ on the queue, so we keep "is:pr -is:draft base:master" (is:open is added by the action by default) as a prefix for all queries and then negate the rest of the params in separate queries to simulate boolean OR (see https://github.com/actions/stale/pull/1145)
           # except for label:auto-merge-after-CI and label:ready-to-merge which presumably will be noticed before they go stale
-          only-matching-filter: '[ "is:pr -is:draft base:master -status:success", "is:pr -is:draft base:master label:blocked-by-other-PR", "is:pr -is:draft base:master label:merge-conflict", "is:pr -is:draft base:master label:awaiting-CI", "is:pr -is:draft base:master label:WIP", "is:pr -is:draft base:master label:awaiting-author", "is:pr -is:draft base:master label:delegated", "is:pr -is:draft base:master label:please-adopt", "is:pr -is:draft base:master label:help-wanted", "is:pr -is:draft base:master label:awaiting-zulip" ]'
+          only-matching-filter: '[ "is:pr -is:draft base:master -status:success", "is:pr -is:draft base:master label:blocked-by-other-PR", "is:pr -is:draft base:master label:blocked-by-batt-PR", "is:pr -is:draft base:master label:blocked-by-core-PR", "is:pr -is:draft base:master label:blocked-by-qq-PR", "is:pr -is:draft base:master label:merge-conflict", "is:pr -is:draft base:master label:awaiting-author", "is:pr -is:draft base:master label:awaiting-CI", "is:pr -is:draft base:master label:awaiting-zulip", "is:pr -is:draft base:master label:WIP", "is:pr -is:draft base:master label:delegated", "is:pr -is:draft base:master label:please-adopt", "is:pr -is:draft base:master label:help-wanted",  ]'

Archive/Arithcc.lean

@@ -3,7 +3,7 @@ Copyright (c) 2020 Xi Wang. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Xi Wang
 -/
-import Mathlib.Data.Nat.Defs
+import Mathlib.Data.Nat.Basic
 import Mathlib.Order.Basic
 import Mathlib.Tactic.Common
 
@@ -191,12 +191,12 @@ protected theorem StateEqRs.refl (t : Register) (ζ : State) : ζ ≃[t]/ac ζ :
 @[symm]
 protected theorem StateEqRs.symm {t : Register} (ζ₁ ζ₂ : State) :
     ζ₁ ≃[t]/ac ζ₂ → ζ₂ ≃[t]/ac ζ₁ := by
-  simp_all [StateEqRs] -- Porting note: was `finish [StateEqRs]`
+  simp_all [StateEqRs]
 
 @[trans]
 protected theorem StateEqRs.trans {t : Register} (ζ₁ ζ₂ ζ₃ : State) :
     ζ₁ ≃[t]/ac ζ₂ → ζ₂ ≃[t]/ac ζ₃ → ζ₁ ≃[t]/ac ζ₃ := by
-  simp_all [StateEqRs] -- Porting note: was `finish [StateEqRs]`
+  simp_all [StateEqRs]
 
 /-- Machine states ζ₁ and ζ₂ are equal except for registers {x | x ≥ t}. -/
 def StateEq (t : Register) (ζ₁ ζ₂ : State) : Prop :=
@@ -243,7 +243,7 @@ theorem stateEq_implies_write_eq {t : Register} {ζ₁ ζ₂ : State} (h : ζ₁
   intro r hr
   have hr : r ≤ t := Register.le_of_lt_succ hr
   rcases lt_or_eq_of_le hr with hr | hr
-  · cases' h with _ h
+  · obtain ⟨_, h⟩ := h
     specialize h r hr
     simp_all
   · simp_all
@@ -262,7 +262,7 @@ theorem write_eq_implies_stateEq {t : Register} {v : Word} {ζ₁ ζ₂ : State}
   simp [StateEq, StateEqRs] at *
   constructor; · exact h.1
   intro r hr
-  cases' h with _ h
+  obtain ⟨_, h⟩ := h
   specialize h r (lt_trans hr (Register.lt_succ_self _))
   rwa [if_neg (ne_of_lt hr)] at h
 
@@ -320,7 +320,7 @@ theorem compiler_correctness
     have hζ₃_ν₂ : ζ₃.ac = ν₂ := by simp_all [StateEq]
     have hζ₃_ν₁ : read t ζ₃ = ν₁ := by
       simp [StateEq, StateEqRs] at hζ₃ ⊢
-      cases' hζ₃ with _ hζ₃
+      obtain ⟨_, hζ₃⟩ := hζ₃
       specialize hζ₃ t (Register.lt_succ_self _)
       simp_all
     have hζ₄ : ζ₄ ≃[t + 1] { write t ν₁ η with ac := ν } := calc

Archive/Examples/PropEncodable.lean

@@ -34,13 +34,6 @@ inductive PropForm (α : Type*)
   | and : PropForm α → PropForm α → PropForm α
   | or : PropForm α → PropForm α → PropForm α
 
-/-!
-The next three functions make it easier to construct functions from a small
-`Fin`.
--/
-
--- Porting note: using `![_, _]` notation instead
-
 namespace PropForm
 
 private def Constructors (α : Type*) :=

Archive/Imo/Imo1962Q1.lean

@@ -37,7 +37,7 @@ abbrev ProblemPredicate' (c n : ℕ) : Prop :=
 
 lemma without_digits {n : ℕ} (hn : ProblemPredicate n) : ∃ c : ℕ, ProblemPredicate' c n := by
   use n / 10
-  cases' n with n
+  rcases n with - | n
   · have hpp : ¬ProblemPredicate 0 := by norm_num [ProblemPredicate]
     contradiction
   · rw [ProblemPredicate, digits_def' (by decide : 2 ≤ 10) n.succ_pos, List.headI, List.tail_cons,

Archive/Imo/Imo1975Q1.lean

@@ -3,7 +3,7 @@ Copyright (c) 2022 Mantas Bakšys. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mantas Bakšys
 -/
-import Mathlib.Algebra.BigOperators.Ring
+import Mathlib.Algebra.BigOperators.Ring.Finset
 import Mathlib.Algebra.Order.Rearrangement
 import Mathlib.Data.Real.Basic
 import Mathlib.Order.Interval.Finset.Nat

Archive/Imo/Imo1982Q1.lean

@@ -64,11 +64,9 @@ lemma f₁ : f 1 = 0 := by
   · cases Nat.succ_ne_zero _ h₂.symm
 
 lemma f₃ : f 3 = 1 := by
-    have h : f 3 = f 2 + f 1 ∨ f 3  = f 2 + f 1 + 1 := by apply hf.rel 2 1
-    rw [hf.f₁, hf.f₂, add_zero, zero_add] at h
-    have not_left : ¬ f 3 = 0 := by apply ne_of_gt hf.hf₃
-    rw [or_iff_right (not_left)] at h
-    exact h
+  have h : f 3 = f 2 + f 1 ∨ f 3 = f 2 + f 1 + 1 := hf.rel 2 1
+  rw [hf.f₁, hf.f₂, add_zero, zero_add] at h
+  exact h.resolve_left hf.hf₃.ne'
 
 lemma superadditive {m n : ℕ+} : f m + f n ≤ f (m + n) := by
   have h := hf.rel m n
@@ -98,7 +96,7 @@ lemma part_1 : 660 ≤ f (1980) := by
 
 lemma part_2 : f 1980 ≤ 660 := by
   have h : 5 * f 1980 + 33 * f 3 ≤ 5 * 660 + 33 := by
-    calc (5 : ℕ+) * f 1980 + (33 : ℕ+) * f 3 ≤  f (5 * 1980 + 33 * 3) := by apply hf.superlinear
+    calc (5 : ℕ+) * f 1980 + (33 : ℕ+) * f 3 ≤ f (5 * 1980 + 33 * 3) := by apply hf.superlinear
     _ = f 9999 := by rfl
     _ = 5 * 660 + 33 := by rw [hf.f_9999]
   rw [hf.f₃, mul_one] at h

Archive/Imo/Imo1987Q1.lean

@@ -5,7 +5,6 @@ Authors: Yury Kudryashov
 -/
 import Mathlib.Data.Fintype.BigOperators
 import Mathlib.Data.Fintype.Perm
-import Mathlib.Data.Fintype.Prod
 import Mathlib.Dynamics.FixedPoints.Basic
 
 /-!
@@ -96,6 +95,6 @@ theorem main₀ (n : ℕ) : ∑ k ∈ range (n + 1), k * p (Fin n) k = n * (n -
 
 /-- Main statement for permutations of `Fin n`. -/
 theorem main {n : ℕ} (hn : 1 ≤ n) : ∑ k ∈ range (n + 1), k * p (Fin n) k = n ! := by
-  rw [main₀, Nat.mul_factorial_pred (zero_lt_one.trans_le hn)]
+  rw [main₀, Nat.mul_factorial_pred hn]
 
 end Imo1987Q1

Archive/Imo/Imo1988Q6.lean

@@ -158,7 +158,7 @@ theorem constant_descent_vieta_jumping (x y : ℕ) {claim : Prop} {H : ℕ → 
   rw [mul_comm] at hV₂
   have Hc := H_desc hmx mx_lt_my h_base hHm c h_root hV₁ hV₂
   -- This means that we may assume that c ≥ 0 and c ≤ m_x.
-  cases' Hc with c_nonneg c_lt
+  obtain ⟨c_nonneg, c_lt⟩ := Hc
   -- In other words, c is a natural number.
   lift c to ℕ using c_nonneg
   -- Recall that we are trying find a point (a,b) such that b ∈ S and b < m.

Archive/Imo/Imo1994Q1.lean

@@ -32,7 +32,7 @@ open Finset
 namespace Imo1994Q1
 
 theorem tedious (m : ℕ) (k : Fin (m + 1)) : m - ((m + 1 - ↑k) + m) % (m + 1) = ↑k := by
-  cases' k with k hk
+  obtain ⟨k, hk⟩ := k
   rw [Nat.lt_succ_iff, le_iff_exists_add] at hk
   rcases hk with ⟨c, rfl⟩
   have : (k + c + 1 - k) + (k + c) = c + (k + c + 1) := by omega
@@ -83,7 +83,7 @@ theorem imo1994_q1 (n : ℕ) (m : ℕ) (A : Finset ℕ) (hm : #A = m + 1)
     have h1 : a i + a (Fin.last m - k) ≤ n := by unfold a; linarith only [h, a.monotone hi]
     have h2 : a i + a (Fin.last m - k) ∈ A := hadd _ (ha _) _ (ha _) h1
     rw [← mem_coe, ← range_orderEmbOfFin A hm, Set.mem_range] at h2
-    cases' h2 with j hj
+    obtain ⟨j, hj⟩ := h2
     refine ⟨j, ⟨?_, Fin.le_last j⟩, hj⟩
     rw [← a.strictMono.lt_iff_lt, hj]
     simpa using (hrange (a i) (ha i)).1