Auto-resolved conflicts in lean-toolchain and lake-manifest.json

Author: mathlib4-bot

.github/workflows/label_new_contributor.yml

@@ -24,12 +24,14 @@ jobs:
       contents: read
     steps:
       - name: Label PR and report count
+        id: contributor-check
         uses: actions/github-script@ed597411d8f924073f98dfc5c65a23a2325f34cd # v8.0.0
         with:
           script: |
             const MIN_MERGED = 5;
             const creator = context.payload.sender.login;
             const { owner, repo } = context.repo;
+            core.setOutput('should_welcome', 'false');
 
             console.log(`Checking closed issues for user: ${creator}`);
 
@@ -77,47 +79,7 @@ jobs:
                 repo,
                 labels: ['new-contributor']
               });
-
-              // Check if we already posted a welcome comment (idempotency)
-              const WELCOME_MARKER = '<!-- mathlib-welcome-comment -->';
-              let alreadyWelcomed = false;
-              for await (const response of github.paginate.iterator(
-                github.rest.issues.listComments,
-                {
-                  issue_number: context.issue.number,
-                  owner,
-                  repo,
-                  per_page: 100,
-                }
-              )) {
-                if (response.data.some(c => c.body.includes(WELCOME_MARKER))) {
-                  alreadyWelcomed = true;
-                  break;
-                }
-              }
-
-              if (!alreadyWelcomed) {
-                console.log('Posting welcome comment for new contributor...');
-                const body = [
-                  WELCOME_MARKER,
-                  '## Welcome new contributor!',
-                  'Thank you for contributing to Mathlib! If you haven\'t done so already, please review our [contribution guidelines](https://leanprover-community.github.io/contribute/index.html), as well as the [style guide](https://leanprover-community.github.io/contribute/style.html) and [naming conventions](https://leanprover-community.github.io/contribute/naming.html).',
-                  '',
-                  'We use a [review queue](https://leanprover-community.github.io/queueboard/review_dashboard.html) to manage reviews. If your PR does not appear there, it is probably because it is not successfully building (i.e., it doesn\'t have a green checkmark), has the `awaiting-author` tag, or another reason described in the [Lifecycle of a PR](https://leanprover-community.github.io/contribute/index.html#lifecycle-of-a-pr).',
-                  '',
-                  'If you haven\'t already done so, please come to [https://leanprover.zulipchat.com/](https://leanprover.zulipchat.com/), introduce yourself, and mention your new PR.',
-                  '',
-                  'Thank you again for joining our community.',
-                ].join('\n');
-                await github.rest.issues.createComment({
-                  issue_number: context.issue.number,
-                  owner,
-                  repo,
-                  body,
-                });
-              } else {
-                console.log('Welcome comment already exists, skipping.');
-              }
+              core.setOutput('should_welcome', 'true');
             }
 
             console.log('Creating check run with a message about the PR count by this author...');
@@ -134,3 +96,18 @@ jobs:
                 summary: message,
               },
             });
+
+      - name: Post welcome comment for new contributor
+        if: steps.contributor-check.outputs.should_welcome == 'true'
+        uses: marocchino/sticky-pull-request-comment@773744901bac0e8cbb5a0dc842800d45e9b2b405 # v2.9.4
+        with:
+          header: 'New Contributor Welcome'
+          message: |
+            ## Welcome new contributor!
+            Thank you for contributing to Mathlib! If you haven't done so already, please review our [contribution guidelines](https://leanprover-community.github.io/contribute/index.html), as well as the [style guide](https://leanprover-community.github.io/contribute/style.html) and [naming conventions](https://leanprover-community.github.io/contribute/naming.html).
+
+            We use a [review queue](https://leanprover-community.github.io/queueboard/review_dashboard.html) to manage reviews. If your PR does not appear there, it is probably because it is not successfully building (i.e., it doesn't have a green checkmark), has the `awaiting-author` tag, or another reason described in the [Lifecycle of a PR](https://leanprover-community.github.io/contribute/index.html#lifecycle-of-a-pr).
+
+            If you haven't already done so, please come to [https://leanprover.zulipchat.com/](https://leanprover.zulipchat.com/), introduce yourself, and mention your new PR.
+
+            Thank you again for joining our community.

.github/workflows/nightly_bump_and_merge.yml

@@ -230,7 +230,7 @@ jobs:
           }
 
           # Find tags that are ancestors of this branch with the right format
-          LATEST_TAG=$(git tag --merged HEAD | grep "nightly-testing-[0-9]\{4\}-[0-9]\{2\}-[0-9]\{2\}" | sort -r | head -n 1)
+          LATEST_TAG=$(git tag --merged HEAD | grep "nightly-testing-[0-9]\{4\}-[0-9]\{2\}-[0-9]\{2\}\(-rev[0-9]\+\)\?" | sort -rV | head -n 1)
           echo "Latest tag found for $BRANCH: ${LATEST_TAG:-none}"
 
           # Return to nightly-testing branch

.github/workflows/nightly_detect_failure.yml

@@ -274,7 +274,7 @@ jobs:
           core.setOutput('toolchain_content', content);
           core.setOutput('branch_name', branchName);
 
-          const match = content.match(/leanprover\/lean4:nightly-(\d{4}-\d{2}-\d{2})/);
+          const match = content.match(/leanprover\/lean4:nightly-(\d{4}-\d{2}-\d{2}(?:-rev\d+)?)/);
           if (!match) {
             core.setFailed('Toolchain pattern did not match');
             return null;
@@ -292,7 +292,7 @@ jobs:
         type: 'stream'
         topic: 'Mathlib status updates'
         content: |
-          ⚠️ Warning: The lean-toolchain file in bump branch `${{ steps.bump_version.outputs.branch_name }}` does not match the expected pattern 'leanprover/lean4:nightly-YYYY-MM-DD'.
+          ⚠️ Warning: The lean-toolchain file in bump branch `${{ steps.bump_version.outputs.branch_name }}` does not match the expected pattern 'leanprover/lean4:nightly-YYYY-MM-DD(-revK)'.
 
           **Branch:** `${{ steps.bump_version.outputs.branch_name }}`
           **File URL:** https://github.com/${{ github.repository }}/blob/${{ steps.bump_version.outputs.branch_sha }}/lean-toolchain
@@ -418,7 +418,7 @@ jobs:
             if last_bot_message:
                 last_content = last_bot_message['content']
                 # Extract nightly date and bump branch from last bot message
-                date_match = re.search(r'bump/nightly-(\d{4}-\d{2}-\d{2})', last_content)
+                date_match = re.search(r'bump/nightly-(\d{4}-\d{2}-\d{2}(?:-rev\d+)?)', last_content)
                 branch_match = re.search(r'PR that to (bump/v[\d.]+)', last_content)
                 if date_match and branch_match:
                     last_date = date_match.group(1)

Mathlib.lean

@@ -2122,6 +2122,7 @@ public import Mathlib.Analysis.PSeriesComplex
 public import Mathlib.Analysis.Polynomial.Basic
 public import Mathlib.Analysis.Polynomial.CauchyBound
 public import Mathlib.Analysis.Polynomial.Factorization
+public import Mathlib.Analysis.Polynomial.Fourier
 public import Mathlib.Analysis.Polynomial.MahlerMeasure
 public import Mathlib.Analysis.Polynomial.Norm
 public import Mathlib.Analysis.Quaternion
@@ -5569,6 +5570,7 @@ public import Mathlib.Order.ConditionallyCompleteLattice.Defs
 public import Mathlib.Order.ConditionallyCompleteLattice.Finset
 public import Mathlib.Order.ConditionallyCompleteLattice.Group
 public import Mathlib.Order.ConditionallyCompleteLattice.Indexed
+public import Mathlib.Order.ConditionallyCompletePartialOrder.Defs
 public import Mathlib.Order.Copy
 public import Mathlib.Order.CountableDenseLinearOrder
 public import Mathlib.Order.Cover
@@ -5658,6 +5660,7 @@ public import Mathlib.Order.Hom.CompleteLattice
 public import Mathlib.Order.Hom.Lattice
 public import Mathlib.Order.Hom.Lex
 public import Mathlib.Order.Hom.Order
+public import Mathlib.Order.Hom.PowersetCard
 public import Mathlib.Order.Hom.Set
 public import Mathlib.Order.Hom.WithTopBot
 public import Mathlib.Order.Ideal
@@ -7478,6 +7481,7 @@ public import Mathlib.Topology.Order.ProjIcc
 public import Mathlib.Topology.Order.Real
 public import Mathlib.Topology.Order.Rolle
 public import Mathlib.Topology.Order.ScottTopology
+public import Mathlib.Topology.Order.SuccPred
 public import Mathlib.Topology.Order.T5
 public import Mathlib.Topology.Order.UpperLowerSetTopology
 public import Mathlib.Topology.Order.WithTop

Mathlib/Algebra/BigOperators/Finprod.lean

@@ -10,7 +10,6 @@ public import Mathlib.Algebra.Group.Indicator
 public import Mathlib.Algebra.Group.Support
 public import Mathlib.Algebra.Module.Torsion.Free
 public import Mathlib.Algebra.Notation.FiniteSupport
-public import Mathlib.Algebra.Order.BigOperators.Group.Finset
 public import Mathlib.Algebra.Order.Ring.Defs
 public import Mathlib.Data.Set.Finite.Lattice
 

Mathlib/Algebra/BigOperators/Group/Finset/Gaps.lean

@@ -5,8 +5,8 @@ Authors: Yizheng Zhu
 -/
 module
 
-public import Mathlib.Algebra.BigOperators.Fin
 public import Mathlib.Order.Interval.Finset.Gaps
+public import Mathlib.Algebra.BigOperators.Group.Finset.Basic
 /-!
 # Sum of gaps
 

Mathlib/Algebra/BigOperators/GroupWithZero/Action.lean

@@ -10,6 +10,7 @@ public import Mathlib.Algebra.GroupWithZero.Action.Defs
 public import Mathlib.Algebra.Order.Group.Multiset
 public import Mathlib.Data.Finset.Basic
 public import Mathlib.Algebra.Group.Action.Basic
+public import Mathlib.Algebra.Group.Units.Equiv
 
 /-!
 # Lemmas about group actions on big operators

Mathlib/Algebra/Category/ModuleCat/Ext/DimensionShifting.lean

@@ -5,14 +5,12 @@ Authors: Nailin Guan
 -/
 module
 
-public import Mathlib.Algebra.Category.Grp.Zero
-public import Mathlib.Algebra.Category.ModuleCat.EnoughInjectives
 public import Mathlib.Algebra.Category.ModuleCat.Ext.HasExt
 public import Mathlib.Algebra.Homology.DerivedCategory.Ext.EnoughInjectives
-public import Mathlib.Algebra.Homology.DerivedCategory.Ext.Linear
 public import Mathlib.Algebra.Homology.ShortComplex.ModuleCat
-public import Mathlib.LinearAlgebra.Dimension.Finite
-public import Mathlib.RingTheory.Noetherian.Basic
+public import Mathlib.Data.Nat.Totient
+public import Mathlib.Data.Rat.Floor
+public import Mathlib.Tactic.Continuity
 
 /-!
 

Mathlib/Algebra/Category/ModuleCat/Ext/Finite.lean

@@ -5,11 +5,9 @@ Authors: Nailin Guan
 -/
 module
 
-public import Mathlib.Algebra.Category.Grp.Zero
 public import Mathlib.Algebra.Category.ModuleCat.Ext.DimensionShifting
 public import Mathlib.Algebra.Homology.DerivedCategory.Ext.Linear
 public import Mathlib.Algebra.Homology.ShortComplex.ModuleCat
-public import Mathlib.LinearAlgebra.Dimension.Finite
 public import Mathlib.RingTheory.Noetherian.Basic
 
 /-!

Mathlib/Algebra/Category/ModuleCat/Sheaf/Generators.lean

@@ -75,6 +75,11 @@ lemma opEpi_id (σ : M.GeneratingSections) :
 lemma opEpi_comp (σ : M.GeneratingSections) (p : M ⟶ N) (q : N ⟶ P) [Epi p] [Epi q] :
     σ.ofEpi (p ≫ q) = (σ.ofEpi p).ofEpi q := rfl
 
+@[simp]
+lemma ofEpi_π (σ : M.GeneratingSections) (p : M ⟶ N) [Epi p] :
+    (σ.ofEpi p).π = σ.π ≫ p := by
+  simp [ofEpi, freeHomEquiv_symm_comp]
+
 /-- Two isomorphic sheaves of modules have equivalent families of generating sections. -/
 def equivOfIso (e : M ≅ N) :
     M.GeneratingSections ≃ N.GeneratingSections where