Trigger CI for leanprover/lean4#5684

.github/workflows/lean4checker.yml

@@ -70,21 +70,19 @@ jobs:
         run: |
           git clone https://github.com/leanprover/lean4checker
           cd lean4checker
-          git checkout v4.13.0-rc3
+          # This should be changed back to a version tag when
+          # anything subsequent to `v4.13.0-rc3` is released.
+          git checkout master
           # Now that the git hash is embedded in each olean,
           # we need to compile lean4checker on the same toolchain
           cp ../lean-toolchain .
           lake build
           ./test.sh
           cd ..
-          lake env lean4checker/.lake/build/bin/lean4checker
-
-      - id: ci_url
-        run: |
-          url=https://github.com/${{ github.repository }}/actions/runs/${{ github.run_id }}
-          curl -s "${url}" |
-            # extract the CI run number from the unique line that matches `  href=".../job/[job number]"`
-            awk -v url="${url}" -F'/' '/^ *href/ {gsub(/"/, "", $NF); printf("summary<<EOF\n%s/job/%s\nEOF", url, $NF)}' >> "$GITHUB_OUTPUT"
+          # After https://github.com/leanprover/lean4checker/pull/26
+          # lean4checker by default only runs on the current project
+          # so we explicitly check Batteries as well here.
+          lake env lean4checker/.lake/build/bin/lean4checker Batteries Mathlib
 
       - name: Post success message on Zulip
         if: success()
@@ -97,7 +95,7 @@ jobs:
           type: 'stream'
           topic: 'lean4checker'
           content: |
-            ✅ lean4checker [succeeded](${{ steps.ci_url.outputs.summary }}) on ${{ github.sha }}
+            ✅ lean4checker [succeeded](https://github.com/${{ github.repository }}/actions/runs/${{ github.run_id }}) on ${{ github.sha }}
 
       - name: Post failure message on Zulip
         if: failure()
@@ -110,7 +108,7 @@ jobs:
           type: 'stream'
           topic: 'lean4checker failure'
           content: |
-            ❌ lean4checker [failed](${{ steps.ci_url.outputs.summary }}) on ${{ github.sha }}
+            ❌ lean4checker [failed](https://github.com/${{ github.repository }}/actions/runs/${{ github.run_id }}) on ${{ github.sha }}
         continue-on-error: true
 
       - name: Post failure message on Zulip main topic
@@ -124,5 +122,5 @@ jobs:
           type: 'stream'
           topic: 'lean4checker'
           content: |
-            ❌ lean4checker failed on ${{ github.sha }}
+            ❌ lean4checker [failed](https://github.com/${{ github.repository }}/actions/runs/${{ github.run_id }}) on ${{ github.sha }}
         continue-on-error: true

.github/workflows/nightly_detect_failure.yml

@@ -212,14 +212,25 @@ jobs:
             payload = f"🛠️: it looks like it's time to create a new bump/nightly-{current_version} branch from nightly-testing (specifically {sha}), and then PR that to {bump_branch}. "
             payload += "To do so semi-automatically, run the following script from mathlib root:\n\n"
             payload += f"```bash\n./scripts/create-adaptation-pr.sh --bumpversion={bump_branch_suffix} --nightlydate={current_version} --nightlysha={sha}\n```\n"
-            # Post the reminder message
-            request = {
-                'type': 'stream',
-                'to': 'nightly-testing',
-                'topic': 'Mathlib bump branch reminders',
-                'content': payload
-            }
-            result = client.send_message(request)
-            print(result)
+            # Only post if the message is different
+            # We compare the first 160 characters, since that includes the date and bump version
+            if not messages or messages[0]['content'][:160] != payload[:160]:
+                # Log messages, because the bot seems to repeat itself...
+                if messages:
+                    print("###### Last message:")
+                    print(messages[0]['content'])
+                    print("###### Current message:")
+                    print(payload)
+                else:
+                    print('The strings match!')
+                # Post the reminder message
+                request = {
+                    'type': 'stream',
+                    'to': 'nightly-testing',
+                    'topic': 'Mathlib bump branch reminders',
+                    'content': payload
+                }
+                result = client.send_message(request)
+                print(result)
         else:
             print('No action needed.')

.github/workflows/stale.yml

@@ -0,0 +1,25 @@
+name: 'Close stale issues and PRs'
+on:
+  schedule:
+    - cron: '30 1 * * *' # every day at 01:30 UTC
+  workflow_dispatch:
+
+jobs:
+  stale:
+    runs-on: ubuntu-latest
+    steps:
+      # until https://github.com/actions/stale/pull/1145 is merged
+      - uses: asterisk/github-actions-stale@main-only-matching-filter
+        with:
+          debug-only: 'true' # TODO: remove in follow-up PR after testing is done!
+          stale-pr-label: 'stale'
+          stale-pr-message: 'Message to comment on stale PRs.'
+          close-pr-label: 'closed-due-to-inactivity'
+          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"
+          # 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" ]'

Archive/Imo/Imo1998Q2.lean

@@ -5,7 +5,7 @@ Authors: Oliver Nash
 -/
 import Mathlib.Algebra.Order.BigOperators.Group.Finset
 import Mathlib.Algebra.Order.Field.Basic
-import Mathlib.Algebra.Ring.Int
+import Mathlib.Algebra.Order.Field.Rat
 import Mathlib.GroupTheory.GroupAction.Ring
 import Mathlib.Tactic.NoncommRing
 import Mathlib.Tactic.Ring

Archive/Imo/Imo2013Q1.lean

@@ -3,12 +3,11 @@ Copyright (c) 2021 David Renshaw. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: David Renshaw
 -/
-import Mathlib.Algebra.BigOperators.Pi
-import Mathlib.Algebra.Order.Ring.Abs
-import Mathlib.Data.PNat.Basic
-import Mathlib.Tactic.Ring
+import Mathlib.Algebra.BigOperators.Group.Finset
+import Mathlib.Algebra.Order.Field.Rat
 import Mathlib.Tactic.FieldSimp
 import Mathlib.Tactic.Positivity.Basic
+import Mathlib.Tactic.Ring
 
 /-!
 # IMO 2013 Q1

Archive/Imo/Imo2019Q4.lean

@@ -37,14 +37,14 @@ namespace Imo2019Q4
 theorem upper_bound {k n : ℕ} (hk : k > 0)
     (h : (k ! : ℤ) = ∏ i ∈ range n, ((2:ℤ) ^ n - (2:ℤ) ^ i)) : n < 6 := by
   have h2 : ∑ i ∈ range n, i < k := by
-    suffices multiplicity 2 (k ! : ℤ) = ↑(∑ i ∈ range n, i : ℕ) by
-      rw [← PartENat.coe_lt_coe, ← this]; change multiplicity ((2 : ℕ) : ℤ) _ < _
-      simp_rw [Int.natCast_multiplicity, multiplicity_two_factorial_lt hk.lt.ne.symm]
-    rw [h, multiplicity.Finset.prod Int.prime_two, Nat.cast_sum]
+    suffices emultiplicity 2 (k ! : ℤ) = ↑(∑ i ∈ range n, i : ℕ) by
+      rw [← Nat.cast_lt (α := ℕ∞), ← this]; change emultiplicity ((2 : ℕ) : ℤ) _ < _
+      simp_rw [Int.natCast_emultiplicity, emultiplicity_two_factorial_lt hk.lt.ne.symm]
+    rw [h, Finset.emultiplicity_prod Int.prime_two, Nat.cast_sum]
     apply sum_congr rfl; intro i hi
-    rw [multiplicity_sub_of_gt, multiplicity_pow_self_of_prime Int.prime_two]
-    rwa [multiplicity_pow_self_of_prime Int.prime_two, multiplicity_pow_self_of_prime Int.prime_two,
-      PartENat.coe_lt_coe, ← mem_range]
+    rw [emultiplicity_sub_of_gt, emultiplicity_pow_self_of_prime Int.prime_two]
+    rwa [emultiplicity_pow_self_of_prime Int.prime_two,
+      emultiplicity_pow_self_of_prime Int.prime_two, Nat.cast_lt, ← mem_range]
   rw [← not_le]; intro hn
   apply _root_.ne_of_gt _ h
   calc ∏ i ∈ range n, ((2:ℤ) ^ n - (2:ℤ) ^ i) ≤ ∏ __ ∈ range n, (2:ℤ) ^ n := ?_

Archive/MiuLanguage/DecisionNec.lean

@@ -5,9 +5,7 @@ Authors: Gihan Marasingha
 -/
 import Archive.MiuLanguage.Basic
 import Mathlib.Data.List.Basic
-import Mathlib.Data.List.Count
 import Mathlib.Data.Nat.ModEq
-import Mathlib.Tactic.Ring
 
 /-!
 # Decision procedure: necessary condition

Archive/Wiedijk100Theorems/BallotProblem.lean

@@ -3,7 +3,7 @@ Copyright (c) 2022 Bhavik Mehta, Kexing Ying. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Bhavik Mehta, Kexing Ying
 -/
-import Mathlib.Probability.CondCount
+import Mathlib.Probability.UniformOn
 
 /-!
 # Ballot problem
@@ -188,21 +188,21 @@ theorem count_countedSequence : ∀ p q : ℕ, count (countedSequence p q) = (p
 
 theorem first_vote_pos :
     ∀ p q,
-      0 < p + q → condCount (countedSequence p q : Set (List ℤ)) {l | l.headI = 1} = p / (p + q)
+      0 < p + q → uniformOn (countedSequence p q : Set (List ℤ)) {l | l.headI = 1} = p / (p + q)
   | p + 1, 0, _ => by
-    rw [counted_right_zero, condCount_singleton]
+    rw [counted_right_zero, uniformOn_singleton]
     simp [ENNReal.div_self _ _, List.replicate_succ]
   | 0, q + 1, _ => by
-    rw [counted_left_zero, condCount_singleton]
+    rw [counted_left_zero, uniformOn_singleton]
     simp only [List.replicate, Nat.add_eq, add_zero, mem_setOf_eq, List.headI_cons, Nat.cast_zero,
       ENNReal.zero_div, ite_eq_right_iff]
     decide
   | p + 1, q + 1, _ => by
     simp_rw [counted_succ_succ]
-    rw [← condCount_disjoint_union ((countedSequence_finite _ _).image _)
+    rw [← uniformOn_disjoint_union ((countedSequence_finite _ _).image _)
         ((countedSequence_finite _ _).image _) (disjoint_bits _ _),
       ← counted_succ_succ,
-      condCount_eq_one_of ((countedSequence_finite p (q + 1)).image _)
+      uniformOn_eq_one_of ((countedSequence_finite p (q + 1)).image _)
         ((countedSequence_nonempty _ _).image _)]
     · have : List.cons (-1) '' countedSequence (p + 1) q ∩ {l : List ℤ | l.headI = 1} = ∅ := by
         ext
@@ -215,7 +215,7 @@ theorem first_vote_pos :
           List.cons 1 '' countedSequence p (q + 1) := by
         rw [inter_eq_right, counted_succ_succ]
         exact subset_union_left
-      rw [(condCount_eq_zero_iff <| (countedSequence_finite _ _).image _).2 this, condCount,
+      rw [(uniformOn_eq_zero_iff <| (countedSequence_finite _ _).image _).2 this, uniformOn,
         cond_apply _ list_int_measurableSet, hint, count_injective_image List.cons_injective,
         count_countedSequence, count_countedSequence, one_mul, zero_mul, add_zero,
         Nat.cast_add, Nat.cast_one, mul_comm, ← div_eq_mul_inv, ENNReal.div_eq_div_iff]
@@ -230,27 +230,27 @@ theorem headI_mem_of_nonempty {α : Type*} [Inhabited α] : ∀ {l : List α} (_
   | x::l, _ => List.mem_cons_self x l
 
 theorem first_vote_neg (p q : ℕ) (h : 0 < p + q) :
-    condCount (countedSequence p q) {l | l.headI = 1}ᶜ = q / (p + q) := by
+    uniformOn (countedSequence p q) {l | l.headI = 1}ᶜ = q / (p + q) := by
   have h' : (p + q : ℝ≥0∞) ≠ 0 := mod_cast h.ne'
-  have := condCount_compl
+  have := uniformOn_compl
     {l : List ℤ | l.headI = 1}ᶜ (countedSequence_finite p q) (countedSequence_nonempty p q)
   rw [compl_compl, first_vote_pos _ _ h] at this
   rw [ENNReal.eq_sub_of_add_eq _ this, ENNReal.eq_div_iff, ENNReal.mul_sub, mul_one,
     ENNReal.mul_div_cancel', ENNReal.add_sub_cancel_left]
   all_goals simp_all [ENNReal.div_eq_top]
 
-theorem ballot_same (p : ℕ) : condCount (countedSequence (p + 1) (p + 1)) staysPositive = 0 := by
-  rw [condCount_eq_zero_iff (countedSequence_finite _ _), eq_empty_iff_forall_not_mem]
+theorem ballot_same (p : ℕ) : uniformOn (countedSequence (p + 1) (p + 1)) staysPositive = 0 := by
+  rw [uniformOn_eq_zero_iff (countedSequence_finite _ _), eq_empty_iff_forall_not_mem]
   rintro x ⟨hx, t⟩
   apply ne_of_gt (t x _ x.suffix_refl)
   · simpa using sum_of_mem_countedSequence hx
   · refine List.ne_nil_of_length_pos ?_
     rw [length_of_mem_countedSequence hx]
     exact Nat.add_pos_left (Nat.succ_pos _) _
 
-theorem ballot_edge (p : ℕ) : condCount (countedSequence (p + 1) 0) staysPositive = 1 := by
+theorem ballot_edge (p : ℕ) : uniformOn (countedSequence (p + 1) 0) staysPositive = 1 := by
   rw [counted_right_zero]
-  refine condCount_eq_one_of (finite_singleton _) (singleton_nonempty _) ?_
+  refine uniformOn_eq_one_of (finite_singleton _) (singleton_nonempty _) ?_
   refine singleton_subset_iff.2 fun l hl₁ hl₂ => List.sum_pos _ (fun x hx => ?_) hl₁
   rw [List.eq_of_mem_replicate (hl₂.mem hx)]
   norm_num
@@ -267,9 +267,9 @@ theorem countedSequence_int_pos_counted_succ_succ (p q : ℕ) :
       norm_num
 
 theorem ballot_pos (p q : ℕ) :
-    condCount (countedSequence (p + 1) (q + 1) ∩ {l | l.headI = 1}) staysPositive =
-      condCount (countedSequence p (q + 1)) staysPositive := by
-  rw [countedSequence_int_pos_counted_succ_succ, condCount, condCount,
+    uniformOn (countedSequence (p + 1) (q + 1) ∩ {l | l.headI = 1}) staysPositive =
+      uniformOn (countedSequence p (q + 1)) staysPositive := by
+  rw [countedSequence_int_pos_counted_succ_succ, uniformOn, uniformOn,
     cond_apply _ list_int_measurableSet, cond_apply _ list_int_measurableSet,
     count_injective_image List.cons_injective]
   congr 1
@@ -294,9 +294,9 @@ theorem countedSequence_int_neg_counted_succ_succ (p q : ℕ) :
       norm_num
 
 theorem ballot_neg (p q : ℕ) (qp : q < p) :
-    condCount (countedSequence (p + 1) (q + 1) ∩ {l | l.headI = 1}ᶜ) staysPositive =
-      condCount (countedSequence (p + 1) q) staysPositive := by
-  rw [countedSequence_int_neg_counted_succ_succ, condCount, condCount,
+    uniformOn (countedSequence (p + 1) (q + 1) ∩ {l | l.headI = 1}ᶜ) staysPositive =
+      uniformOn (countedSequence (p + 1) q) staysPositive := by
+  rw [countedSequence_int_neg_counted_succ_succ, uniformOn, uniformOn,
     cond_apply _ list_int_measurableSet, cond_apply _ list_int_measurableSet,
     count_injective_image List.cons_injective]
   congr 1
@@ -310,7 +310,7 @@ theorem ballot_neg (p q : ℕ) (qp : q < p) :
   exact List.cons_injective
 
 theorem ballot_problem' :
-    ∀ q p, q < p → (condCount (countedSequence p q) staysPositive).toReal = (p - q) / (p + q) := by
+    ∀ q p, q < p → (uniformOn (countedSequence p q) staysPositive).toReal = (p - q) / (p + q) := by
   classical
   apply Nat.diag_induction
   · intro p
@@ -322,12 +322,12 @@ theorem ballot_problem' :
     rw [div_self]
     exact Nat.cast_add_one_ne_zero p
   · intro q p qp h₁ h₂
-    haveI := condCount_isProbabilityMeasure
+    haveI := uniformOn_isProbabilityMeasure
       (countedSequence_finite p (q + 1)) (countedSequence_nonempty _ _)
-    haveI := condCount_isProbabilityMeasure
+    haveI := uniformOn_isProbabilityMeasure
       (countedSequence_finite (p + 1) q) (countedSequence_nonempty _ _)
     have h₃ : p + 1 + (q + 1) > 0 := Nat.add_pos_left (Nat.succ_pos _) _
-    rw [← condCount_add_compl_eq {l : List ℤ | l.headI = 1} _ (countedSequence_finite _ _),
+    rw [← uniformOn_add_compl_eq {l : List ℤ | l.headI = 1} _ (countedSequence_finite _ _),
       first_vote_pos _ _ h₃, first_vote_neg _ _ h₃, ballot_pos, ballot_neg _ _ qp]
     rw [ENNReal.toReal_add, ENNReal.toReal_mul, ENNReal.toReal_mul, ← Nat.cast_add,
       ENNReal.toReal_div, ENNReal.toReal_div, ENNReal.toReal_nat, ENNReal.toReal_nat,
@@ -349,12 +349,12 @@ theorem ballot_problem' :
 
 /-- The ballot problem. -/
 theorem ballot_problem :
-    ∀ q p, q < p → condCount (countedSequence p q) staysPositive = (p - q) / (p + q) := by
+    ∀ q p, q < p → uniformOn (countedSequence p q) staysPositive = (p - q) / (p + q) := by
   intro q p qp
   haveI :=
-    condCount_isProbabilityMeasure (countedSequence_finite p q) (countedSequence_nonempty _ _)
+    uniformOn_isProbabilityMeasure (countedSequence_finite p q) (countedSequence_nonempty _ _)
   have :
-    (condCount (countedSequence p q) staysPositive).toReal =
+    (uniformOn (countedSequence p q) staysPositive).toReal =
       ((p - q) / (p + q) : ℝ≥0∞).toReal := by
     rw [ballot_problem' q p qp]
     rw [ENNReal.toReal_div, ← Nat.cast_add, ← Nat.cast_add, ENNReal.toReal_nat,

Archive/Wiedijk100Theorems/BirthdayProblem.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Eric Rodriguez
 -/
 import Mathlib.Data.Fintype.CardEmbedding
-import Mathlib.Probability.CondCount
+import Mathlib.Probability.UniformOn
 import Mathlib.Probability.Notation
 
 /-!
@@ -52,15 +52,15 @@ instance : MeasurableSingletonClass (Fin m) :=
 /- We then endow the space with a canonical measure, which is called ℙ.
 We define this to be the conditional counting measure. -/
 noncomputable instance : MeasureSpace (Fin n → Fin m) :=
-  ⟨condCount Set.univ⟩
+  ⟨uniformOn Set.univ⟩
 
 -- The canonical measure on `Fin n → Fin m` is a probability measure (except on an empty space).
 instance : IsProbabilityMeasure (ℙ : Measure (Fin n → Fin (m + 1))) :=
-  condCount_isProbabilityMeasure Set.finite_univ Set.univ_nonempty
+  uniformOn_isProbabilityMeasure Set.finite_univ Set.univ_nonempty
 
 theorem FinFin.measure_apply {s : Set <| Fin n → Fin m} :
     ℙ s = |s.toFinite.toFinset| / ‖Fin n → Fin m‖ := by
-  erw [condCount_univ, Measure.count_apply_finite]
+  erw [uniformOn_univ, Measure.count_apply_finite]
 
 /-- **Birthday Problem**: first probabilistic interpretation. -/
 theorem birthday_measure :

Archive/Wiedijk100Theorems/BuffonsNeedle.lean

@@ -201,7 +201,7 @@ include hd hB hBₘ in
 lemma buffon_integral :
     𝔼[N l B] = (d * π) ⁻¹ *
       ∫ (θ : ℝ) in Set.Icc 0 π,
-      ∫ (x : ℝ) in Set.Icc (-d / 2) (d / 2) ∩ Set.Icc (-θ.sin * l / 2) (θ.sin * l / 2), 1 := by
+      ∫ (_ : ℝ) in Set.Icc (-d / 2) (d / 2) ∩ Set.Icc (-θ.sin * l / 2) (θ.sin * l / 2), 1 := by
   simp_rw [N, Function.comp_apply]
   rw [
     ← MeasureTheory.integral_map hBₘ.aemeasurable

Archive/Wiedijk100Theorems/Partition.lean

@@ -216,7 +216,7 @@ theorem partialGF_prop (α : Type*) [CommSemiring α] (n : ℕ) (s : Finset ℕ)
         intro a; exact Nat.lt_irrefl 0 (hs 0 (hp₂.2 0 a))
       intro a; exact Nat.lt_irrefl 0 (hs 0 (hp₁.2 0 a))
     · rw [← mul_left_inj' hi]
-      rw [Function.funext_iff] at h
+      rw [funext_iff] at h
       exact h.2 i
   · simp only [φ, mem_filter, mem_finsuppAntidiag, mem_univ, exists_prop, true_and, and_assoc]
     rintro f ⟨hf, hf₃, hf₄⟩
@@ -329,7 +329,7 @@ theorem partialDistinctGF_prop [CommSemiring α] (n m : ℕ) :
 -/
 theorem distinctGF_prop [CommSemiring α] (n m : ℕ) (h : n < m + 1) :
     ((Nat.Partition.distincts n).card : α) = coeff α n (partialDistinctGF m) := by
-  erw [← partialDistinctGF_prop, Nat.Partition.distincts]
+  rw [← partialDistinctGF_prop, Nat.Partition.distincts]
   congr with p
   apply (and_iff_left _).symm
   intro i hi