m,erge master

Author: kim-em

.github/build.in.yml

@@ -267,7 +267,11 @@ jobs:
         uses: actions/upload-artifact@ea165f8d65b6e75b540449e92b4886f43607fa02 # v4.6.2
         with:
           name: mathlib4_artifact
-          path: pr-branch/
+          include-hidden-files: true
+          # we exclude .git since there may be secrets in there
+          path: |
+            pr-branch/
+            !pr-branch/.git/
 
       # The cache secrets are available here, so we must not run any untrusted code.
       - name: upload cache

.github/workflows/bors.yml

@@ -277,7 +277,11 @@ jobs:
         uses: actions/upload-artifact@ea165f8d65b6e75b540449e92b4886f43607fa02 # v4.6.2
         with:
           name: mathlib4_artifact
-          path: pr-branch/
+          include-hidden-files: true
+          # we exclude .git since there may be secrets in there
+          path: |
+            pr-branch/
+            !pr-branch/.git/
 
       # The cache secrets are available here, so we must not run any untrusted code.
       - name: upload cache

.github/workflows/build.yml

@@ -284,7 +284,11 @@ jobs:
         uses: actions/upload-artifact@ea165f8d65b6e75b540449e92b4886f43607fa02 # v4.6.2
         with:
           name: mathlib4_artifact
-          path: pr-branch/
+          include-hidden-files: true
+          # we exclude .git since there may be secrets in there
+          path: |
+            pr-branch/
+            !pr-branch/.git/
 
       # The cache secrets are available here, so we must not run any untrusted code.
       - name: upload cache

.github/workflows/build_fork.yml

@@ -281,7 +281,11 @@ jobs:
         uses: actions/upload-artifact@ea165f8d65b6e75b540449e92b4886f43607fa02 # v4.6.2
         with:
           name: mathlib4_artifact
-          path: pr-branch/
+          include-hidden-files: true
+          # we exclude .git since there may be secrets in there
+          path: |
+            pr-branch/
+            !pr-branch/.git/
 
       # The cache secrets are available here, so we must not run any untrusted code.
       - name: upload cache

.github/workflows/zulip_emoji_labelling.yaml

@@ -40,6 +40,7 @@ jobs:
         PR_NUMBER: ${{ github.event.number}}
         LABEL_STATUS: ${{ github.event.action }}
         LABEL_NAME: ${{ github.event.label.name }}
+        PR_LABELS: ${{ toJSON(github.event.pull_request.labels.*.name) }}
       run: |
-        printf $'Running the python script with pr "%s"\n' "$PR_NUMBER" "$LABEL_STATUS" "$LABEL"
-        python scripts/zulip_emoji_reactions.py "$ZULIP_API_KEY" "$ZULIP_EMAIL" "$ZULIP_SITE" "$LABEL_STATUS" "$LABEL_NAME" "$PR_NUMBER"
+        printf $'Running the python script with:\nPR number: "%s"\nlabel status: "%s"\nlabel: "%s"\nPR labels: "%s"\n' "$PR_NUMBER" "$LABEL_STATUS" "$LABEL" "$PR_LABELS"
+        python scripts/zulip_emoji_reactions.py "$ZULIP_API_KEY" "$ZULIP_EMAIL" "$ZULIP_SITE" "$LABEL_STATUS" "$LABEL_NAME" "$PR_NUMBER" "$PR_LABELS"

Archive/Examples/Eisenstein.lean

@@ -35,7 +35,7 @@ example : Irreducible (X ^ 4 - 10 * X ^ 2 + 1 : ℤ[X]) := by
   have hq_deg : q.natDegree = 2 := by unfold q; compute_degree!
   have hq_monic : q.Monic := by unfold q; monicity!
   have hfq : f = q ^ 2 - 12 * q + 12 := by ring
-   -- On the other hand, `f %ₘ q = 12`, which is not a multiple of `9`.
+  -- On the other hand, `f %ₘ q = 12`, which is not a multiple of `9`.
   apply generalizedEisenstein (K := ZMod 3) (q := q) (p := 2)
   · set q₃ : (ZMod 3)[X] := X ^ 2 + 1
     have hdeg_q₃ : q₃.natDegree = 2 := by unfold q₃; compute_degree!

Archive/Imo/Imo1982Q3.lean

@@ -3,8 +3,7 @@ Copyright (c) 2024 Violeta Hernández Palacios. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Violeta Hernández Palacios, Alex Brodbelt
 -/
-import Mathlib.Algebra.Order.BigOperators.Ring.Finset
-import Mathlib.Algebra.GeomSum
+import Mathlib.Algebra.Order.Field.GeomSum
 import Mathlib.Data.NNReal.Basic
 
 /-!

Archive/Imo/Imo2013Q5.lean

@@ -3,7 +3,9 @@ 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.GeomSum
+import Mathlib.Algebra.Order.BigOperators.Group.Finset
+import Mathlib.Algebra.Ring.GeomSum
+import Mathlib.Algebra.Ring.Regular
 import Mathlib.Data.Real.Archimedean
 import Mathlib.Tactic.Positivity
 import Mathlib.Tactic.LinearCombination

Archive/MiuLanguage/DecisionSuf.lean

@@ -328,7 +328,7 @@ theorem ind_hyp_suf (k : ℕ) (ys : Miustr) (hu : count U ys = succ k) (hdec : D
 -/
 theorem der_of_decstr {en : Miustr} (h : Decstr en) : Derivable en := by
   /- The next three lines have the effect of introducing `count U en` as a variable that can be used
-   for induction -/
+  for induction -/
   have hu : ∃ n, count U en = n := exists_eq'
   obtain ⟨n, hu⟩ := hu
   induction n generalizing en with

Archive/Wiedijk100Theorems/PerfectNumbers.lean

@@ -5,8 +5,6 @@ Authors: Aaron Anderson
 -/
 import Mathlib.NumberTheory.ArithmeticFunction
 import Mathlib.NumberTheory.LucasLehmer
-import Mathlib.Algebra.GeomSum
-import Mathlib.RingTheory.Multiplicity
 import Mathlib.Tactic.NormNum.Prime
 
 /-!