Merge remote-tracking branch 'origin/master' into theory_implies

.github/build.in.yml

@@ -1,4 +1,8 @@
-# This is the master file for autogenerating `.github/workflows/{bors, build_fork, build }.yml`.
+### NB: This is the master file for autogenerating
+### NB: `.github/workflows/{bors, build_fork, build}.yml`.
+### NB: If you need to edit any of those files, you should edit this file instead,
+### NB: and regenerate those files by manually running
+### NB: .github/workflows/mk_build_yml.sh
 
 jobs:
   # Cancels previous runs of jobs in this file
@@ -132,13 +136,25 @@ jobs:
           lake exe cache get Mathlib.Init
           lake build --no-build Mathlib.Init && lake exe cache get || echo "No cache for 'Mathlib.Init' available"
 
+      - name: update {Mathlib, Tactic, Counterexamples, Archive}.lean
+        id: mk_all
+        run: |
+
+          if ! lake exe mk_all --check
+          then
+            echo "Not all lean files are in the import all files"
+            echo "mk_all=false" >> "${GITHUB_OUTPUT}"
+          else
+            echo "mk_all=true" >> "${GITHUB_OUTPUT}"
+          fi
+
       - name: build mathlib
         id: build
         uses: liskin/gh-problem-matcher-wrap@v3
         with:
           linters: gcc
           run: |
-            bash -o pipefail -c "lake exe mk_all || echo \"There are unaccounted for files, but I am not failing yet\!\"; env LEAN_ABORT_ON_PANIC=1 lake build --wfail -KCI"
+            bash -o pipefail -c "env LEAN_ABORT_ON_PANIC=1 lake build --wfail -KCI"
 
       - name: upload cache
         # We only upload the cache if the build started (whether succeeding, failing, or cancelled)
@@ -194,8 +210,13 @@ jobs:
           MATHLIB_CACHE_SAS: ${{ secrets.MATHLIB_CACHE_SAS }}
           MATHLIB_CACHE_S3_TOKEN: ${{ secrets.MATHLIB_CACHE_S3_TOKEN }}
 
-      - name: update {Mathlib, Tactic, Counterexamples, Archive}.lean
-        run: lake exe mk_all --check
+      - name: Check {Mathlib, Tactic, Counterexamples, Archive}.lean
+        run: |
+          if [ ${{ steps.mk_all.outputs.mk_all }} == "false" ]
+          then
+            echo "Please run 'lake exe mk_all' to regenerate the import all files"
+            exit 1
+          fi
 
       - name: check for noisy stdout lines
         id: noisy

.github/workflows/add_label_from_diff.yaml

@@ -0,0 +1,42 @@
+name: Autolabel PRs
+
+on:
+  pull_request:
+    types: [opened]
+  push:
+    paths:
+      - scripts/autolabel.lean
+      - .github/workflows/add_label_from_diff.yaml
+
+jobs:
+  add_topic_label:
+    name: Add topic label
+    runs-on: ubuntu-latest
+    # Don't run on forks, where we wouldn't have permissions to add the label anyway.
+    if: github.repository == 'leanprover-community/mathlib4'
+    permissions:
+      issues: write
+      checks: write
+      pull-requests: write
+      contents: read
+    steps:
+      - name: Checkout code
+        uses: actions/checkout@v4
+        with:
+          fetch-depth: 0
+      - name: install elan
+        run: |
+          set -o pipefail
+          curl -sSfL https://github.com/leanprover/elan/releases/download/v3.1.1/elan-x86_64-unknown-linux-gnu.tar.gz | tar xz
+          ./elan-init -y --default-toolchain none
+          echo "$HOME/.elan/bin" >> "${GITHUB_PATH}"
+      - name: lake exe autolabel
+        run: |
+          # the checkout dance, to avoid a detached head
+          git checkout master
+          git checkout -
+          lake exe autolabel "$NUMBER"
+        env:
+          GH_TOKEN: ${{ secrets.GITHUB_TOKEN }}
+          GH_REPO: ${{ github.repository }}
+          NUMBER: ${{ github.event.number }}

.github/workflows/bors.yml

@@ -1,7 +1,8 @@
 # DO NOT EDIT THIS FILE!!!
 
 # This file is automatically generated by mk_build_yml.sh
-# Edit .github/build.in.yml instead and run mk_build_yml.sh to update.
+# Edit .github/build.in.yml instead and run
+# .github/workflows/mk_build_yml.sh to update.
 
 # Forks of mathlib and other projects should be able to use build_fork.yml directly
 # The jobs in this file run on self-hosted workers and will not be run from external forks
@@ -145,13 +146,25 @@ jobs:
           lake exe cache get Mathlib.Init
           lake build --no-build Mathlib.Init && lake exe cache get || echo "No cache for 'Mathlib.Init' available"
 
+      - name: update {Mathlib, Tactic, Counterexamples, Archive}.lean
+        id: mk_all
+        run: |
+
+          if ! lake exe mk_all --check
+          then
+            echo "Not all lean files are in the import all files"
+            echo "mk_all=false" >> "${GITHUB_OUTPUT}"
+          else
+            echo "mk_all=true" >> "${GITHUB_OUTPUT}"
+          fi
+
       - name: build mathlib
         id: build
         uses: liskin/gh-problem-matcher-wrap@v3
         with:
           linters: gcc
           run: |
-            bash -o pipefail -c "lake exe mk_all || echo \"There are unaccounted for files, but I am not failing yet\!\"; env LEAN_ABORT_ON_PANIC=1 lake build --wfail -KCI"
+            bash -o pipefail -c "env LEAN_ABORT_ON_PANIC=1 lake build --wfail -KCI"
 
       - name: upload cache
         # We only upload the cache if the build started (whether succeeding, failing, or cancelled)
@@ -207,8 +220,13 @@ jobs:
           MATHLIB_CACHE_SAS: ${{ secrets.MATHLIB_CACHE_SAS }}
           MATHLIB_CACHE_S3_TOKEN: ${{ secrets.MATHLIB_CACHE_S3_TOKEN }}
 
-      - name: update {Mathlib, Tactic, Counterexamples, Archive}.lean
-        run: lake exe mk_all --check
+      - name: Check {Mathlib, Tactic, Counterexamples, Archive}.lean
+        run: |
+          if [ ${{ steps.mk_all.outputs.mk_all }} == "false" ]
+          then
+            echo "Please run 'lake exe mk_all' to regenerate the import all files"
+            exit 1
+          fi
 
       - name: check for noisy stdout lines
         id: noisy

.github/workflows/build.yml

@@ -1,7 +1,8 @@
 # DO NOT EDIT THIS FILE!!!
 
 # This file is automatically generated by mk_build_yml.sh
-# Edit .github/build.in.yml instead and run mk_build_yml.sh to update.
+# Edit .github/build.in.yml instead and run
+# .github/workflows/mk_build_yml.sh to update.
 
 # Forks of mathlib and other projects should be able to use build_fork.yml directly
 # The jobs in this file run on self-hosted workers and will not be run from external forks
@@ -152,13 +153,25 @@ jobs:
           lake exe cache get Mathlib.Init
           lake build --no-build Mathlib.Init && lake exe cache get || echo "No cache for 'Mathlib.Init' available"
 
+      - name: update {Mathlib, Tactic, Counterexamples, Archive}.lean
+        id: mk_all
+        run: |
+
+          if ! lake exe mk_all --check
+          then
+            echo "Not all lean files are in the import all files"
+            echo "mk_all=false" >> "${GITHUB_OUTPUT}"
+          else
+            echo "mk_all=true" >> "${GITHUB_OUTPUT}"
+          fi
+
       - name: build mathlib
         id: build
         uses: liskin/gh-problem-matcher-wrap@v3
         with:
           linters: gcc
           run: |
-            bash -o pipefail -c "lake exe mk_all || echo \"There are unaccounted for files, but I am not failing yet\!\"; env LEAN_ABORT_ON_PANIC=1 lake build --wfail -KCI"
+            bash -o pipefail -c "env LEAN_ABORT_ON_PANIC=1 lake build --wfail -KCI"
 
       - name: upload cache
         # We only upload the cache if the build started (whether succeeding, failing, or cancelled)
@@ -214,8 +227,13 @@ jobs:
           MATHLIB_CACHE_SAS: ${{ secrets.MATHLIB_CACHE_SAS }}
           MATHLIB_CACHE_S3_TOKEN: ${{ secrets.MATHLIB_CACHE_S3_TOKEN }}
 
-      - name: update {Mathlib, Tactic, Counterexamples, Archive}.lean
-        run: lake exe mk_all --check
+      - name: Check {Mathlib, Tactic, Counterexamples, Archive}.lean
+        run: |
+          if [ ${{ steps.mk_all.outputs.mk_all }} == "false" ]
+          then
+            echo "Please run 'lake exe mk_all' to regenerate the import all files"
+            exit 1
+          fi
 
       - name: check for noisy stdout lines
         id: noisy

.github/workflows/build_fork.yml

@@ -1,7 +1,8 @@
 # DO NOT EDIT THIS FILE!!!
 
 # This file is automatically generated by mk_build_yml.sh
-# Edit .github/build.in.yml instead and run mk_build_yml.sh to update.
+# Edit .github/build.in.yml instead and run
+# .github/workflows/mk_build_yml.sh to update.
 
 # Forks of mathlib and other projects should be able to use build_fork.yml directly
 # The jobs in this file run on GitHub-hosted workers and will only be run from external forks
@@ -149,13 +150,25 @@ jobs:
           lake exe cache get Mathlib.Init
           lake build --no-build Mathlib.Init && lake exe cache get || echo "No cache for 'Mathlib.Init' available"
 
+      - name: update {Mathlib, Tactic, Counterexamples, Archive}.lean
+        id: mk_all
+        run: |
+
+          if ! lake exe mk_all --check
+          then
+            echo "Not all lean files are in the import all files"
+            echo "mk_all=false" >> "${GITHUB_OUTPUT}"
+          else
+            echo "mk_all=true" >> "${GITHUB_OUTPUT}"
+          fi
+
       - name: build mathlib
         id: build
         uses: liskin/gh-problem-matcher-wrap@v3
         with:
           linters: gcc
           run: |
-            bash -o pipefail -c "lake exe mk_all || echo \"There are unaccounted for files, but I am not failing yet\!\"; env LEAN_ABORT_ON_PANIC=1 lake build --wfail -KCI"
+            bash -o pipefail -c "env LEAN_ABORT_ON_PANIC=1 lake build --wfail -KCI"
 
       - name: upload cache
         # We only upload the cache if the build started (whether succeeding, failing, or cancelled)
@@ -211,8 +224,13 @@ jobs:
           MATHLIB_CACHE_SAS: ${{ secrets.MATHLIB_CACHE_SAS }}
           MATHLIB_CACHE_S3_TOKEN: ${{ secrets.MATHLIB_CACHE_S3_TOKEN }}
 
-      - name: update {Mathlib, Tactic, Counterexamples, Archive}.lean
-        run: lake exe mk_all --check
+      - name: Check {Mathlib, Tactic, Counterexamples, Archive}.lean
+        run: |
+          if [ ${{ steps.mk_all.outputs.mk_all }} == "false" ]
+          then
+            echo "Please run 'lake exe mk_all' to regenerate the import all files"
+            exit 1
+          fi
 
       - name: check for noisy stdout lines
         id: noisy

.github/workflows/dependent-issues.yml

@@ -3,6 +3,7 @@ name: Dependent Issues
 on:
   schedule:
     - cron: '*/15 * * * *' # run every 15 minutes
+  workflow_dispatch:
 
 jobs:
   cancel:

.github/workflows/lean4checker.yml

@@ -4,6 +4,7 @@ name: lean4checker Workflow
 on:
   schedule:
     - cron: '0 0 * * *'   # Runs at 00:00 UTC every day
+  workflow_dispatch:
 
 jobs:
   check-lean4checker:

.github/workflows/merge_conflicts.yml

@@ -3,6 +3,7 @@ name: Merge conflicts
 on:
   schedule:
     - cron: '*/15 * * * *' # run every 15 minutes
+  workflow_dispatch:
 
 jobs:
   main:

.github/workflows/mk_build_yml.sh

@@ -13,7 +13,8 @@ header() {
 # DO NOT EDIT THIS FILE!!!
 
 # This file is automatically generated by mk_build_yml.sh
-# Edit .github/build.in.yml instead and run mk_build_yml.sh to update.
+# Edit .github/build.in.yml instead and run
+# .github/workflows/mk_build_yml.sh to update.
 
 # Forks of mathlib and other projects should be able to use build_fork.yml directly
 EOF
@@ -82,7 +83,7 @@ include() {
     s/MAIN_OR_FORK/$3/g;
     s/JOB_NAME/$4/g;
     s/STYLE_LINT_RUNNER/$5/g;
-    /^#.*autogenerating/d
+    /^### NB/d
   " ../build.in.yml
 }
 

.github/workflows/nightly_bump_toolchain.yml

@@ -1,9 +1,9 @@
 name: Bump lean-toolchain on nightly-testing
 
 on:
-  workflow_dispatch:
   schedule:
     - cron: '0 10/3 * * *'  # Run every three hours, starting at 11AM CET/2AM PT.
+  workflow_dispatch:
 
 jobs:
   update-toolchain:

.github/workflows/nightly_detect_failure.yml

@@ -210,7 +210,7 @@ jobs:
             bump_branch_suffix = bump_branch.replace('bump/', '')
             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 {bump_branch_suffix} {current_version}\n```\n"
+            payload += f"```bash\n./scripts/create-adaptation-pr.sh --bumpversion={bump_branch_suffix} --nightlydate={current_version} --nightlysha={sha}\n```\n"
             # 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]:

.github/workflows/nightly_merge_master.yml

@@ -4,7 +4,8 @@ name: Merge master to nightly
 
 on:
   schedule:
-    - cron: '30 */3 * * *'  # 8AM CET/11PM PT
+    - cron: '30 */3 * * *'  # At minute 30 past every 3rd hour.
+  workflow_dispatch:
 
 jobs:
   merge-to-nightly:

.github/workflows/nolints.yml

@@ -2,7 +2,8 @@ name: update nolints
 
 on:
   schedule:
-    - cron: "0 0 * * 0"
+    - cron: "0 0 * * 0" # At 00:00 UTC on Sunday.
+  workflow_dispatch:
 
 jobs:
   build:

.github/workflows/technical_debt_metrics.yml

@@ -2,7 +2,8 @@ name: Weekly Technical Debt Counters
 
 on:
   schedule:
-    - cron: '0 4 * * 1'  # Run at 04:00 every Monday
+    - cron: '0 4 * * 1'  # Run at 04:00 UTC every Monday
+  workflow_dispatch:
 
 jobs:
   run-script:

.github/workflows/update_dependencies.yml

@@ -3,6 +3,7 @@ name: Update Mathlib Dependencies
 on:
   schedule:
     - cron: '0 * * * *'  # This will run every hour
+  workflow_dispatch:
 
 jobs:
   update-dependencies:

Archive/Examples/IfNormalization/Statement.lean

@@ -1,7 +1,7 @@
 /-
 Copyright (c) 2023 Lean FRO LLC. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Scott Morrison
+Authors: Kim Morrison
 -/
 
 /-!

Archive/Examples/IfNormalization/WithoutAesop.lean

@@ -1,7 +1,7 @@
 /-
 Copyright (c) 2023 Chris Hughes. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Chris Hughes, Scott Morrison
+Authors: Chris Hughes, Kim Morrison
 -/
 import Archive.Examples.IfNormalization.Statement
 import Mathlib.Algebra.Order.Monoid.Canonical.Defs

Archive/Examples/MersennePrimes.lean

@@ -1,7 +1,7 @@
 /-
-Copyright (c) 2020 Scott Morrison. All rights reserved.
+Copyright (c) 2020 Kim Morrison. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Scott Morrison
+Authors: Kim Morrison
 -/
 import Mathlib.NumberTheory.LucasLehmer
 

Archive/Hairer.lean

@@ -100,7 +100,7 @@ lemma inj_L : Injective (L ι) :=
         fun g hg _h2g g_supp ↦ by
           simpa [mul_comm (g _), L] using congr($hp ⟨g, g_supp.trans ball_subset_closedBall, hg⟩)
     simp_rw [MvPolynomial.funext_iff, map_zero]
-    refine fun x ↦ AnalyticOn.eval_linearMap (EuclideanSpace.equiv ι ℝ).toLinearMap p
+    refine fun x ↦ AnalyticOnNhd.eval_linearMap (EuclideanSpace.equiv ι ℝ).toLinearMap p
       |>.eqOn_zero_of_preconnected_of_eventuallyEq_zero
       (preconnectedSpace_iff_univ.mp inferInstance) (z₀ := 0) trivial
       (Filter.mem_of_superset (Metric.ball_mem_nhds 0 zero_lt_one) ?_) trivial