Merge branch 'ACL/ConjClassCount-25' into ACL/ConjClassCount-3

.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
@@ -129,8 +133,8 @@ jobs:
         run: |
           rm -rf .lake/build/lib/Mathlib/
           # Fail quickly if the cache is completely cold, by checking for Mathlib.Init
-          lake exe cache get Mathlib.Init
-          lake build --no-build Mathlib.Init && lake exe cache get || echo "No cache for 'Mathlib.Init' available"
+          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
@@ -274,7 +278,7 @@ jobs:
       # Output is posted to the zulip topic
       # https://leanprover.zulipchat.com/#narrow/stream/345428-mathlib-reviewers/topic/lean4checker
 
-      - name: Post comments for lean-pr-testing branch
+      - name: Post comments for lean-pr-testing-NNNN and batteries-pr-testing-NNNN branches
         if: always()
         env:
           TOKEN: ${{ secrets.LEAN_PR_TESTING }}
@@ -287,7 +291,8 @@ jobs:
           LINT_OUTCOME: ${{ steps.lint.outcome }}
           TEST_OUTCOME: ${{ steps.test.outcome }}
         run: |
-          scripts/lean-pr-testing-comments.sh
+          scripts/lean-pr-testing-comments.sh lean
+          scripts/lean-pr-testing-comments.sh batteries
 
   final:
     name: Post-CI jobJOB_NAME

.github/workflows/PR_summary.yml

@@ -55,12 +55,27 @@ jobs:
         PR="${{ github.event.pull_request.number }}"
         title="### PR summary"
 
+        graphAndHighPercentReports=$(python ./scripts/import-graph-report.py base.json head.json changed_files.txt)
+
         ## Import count comment
         importCount=$(
-          python ./scripts/import-graph-report.py base.json head.json changed_files.txt
+          printf '%s\n' "${graphAndHighPercentReports}" | sed '/^Import changes exceeding/Q'
           ./scripts/import_trans_difference.sh
         )
 
+        ## High percentage imports
+        high_percentages=$(
+          printf '%s\n' "${graphAndHighPercentReports}" | sed -n '/^Import changes exceeding/,$p'
+        )
+        # if there are files with large increase in transitive imports, then we add the `large-import` label
+        if [ -n "${high_percentages}" ]
+        then
+          high_percentages=$'\n\n'"${high_percentages}"
+          gh pr edit "${PR}" --add-label large-import
+        else # otherwise, we remove the label
+          gh pr edit "${PR}" --remove-label large-import
+        fi
+
         if [ "$(printf '%s' "${importCount}" | wc -l)" -gt 12 ]
         then
           importCount="$(printf '<details><summary>\n\n%s\n\n</summary>\n\n%s\n\n</details>\n' "#### Import changes for modified files" "${importCount}")"
@@ -80,6 +95,6 @@ jobs:
         currentHash="$(git rev-parse HEAD)"
         hashURL="https://github.com/${{ github.repository }}/pull/${{ github.event.pull_request.number }}/commits/${currentHash}"
 
-        message="$(printf '%s [%s](%s)\n\n%s\n\n---\n\n%s\n' "${title}" "$(git rev-parse --short HEAD)" "${hashURL}" "${importCount}" "${declDiff}")"
+        message="$(printf '%s [%s](%s)%s\n\n%s\n\n---\n\n%s\n' "${title}" "$(git rev-parse --short HEAD)" "${hashURL}" "${high_percentages}" "${importCount}" "${declDiff}")"
 
         ./scripts/update_PR_comment.sh "${message}" "${title}" "${PR}"

.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
@@ -142,8 +143,8 @@ jobs:
         run: |
           rm -rf .lake/build/lib/Mathlib/
           # Fail quickly if the cache is completely cold, by checking for Mathlib.Init
-          lake exe cache get Mathlib.Init
-          lake build --no-build Mathlib.Init && lake exe cache get || echo "No cache for 'Mathlib.Init' available"
+          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
@@ -287,7 +288,7 @@ jobs:
       # Output is posted to the zulip topic
       # https://leanprover.zulipchat.com/#narrow/stream/345428-mathlib-reviewers/topic/lean4checker
 
-      - name: Post comments for lean-pr-testing branch
+      - name: Post comments for lean-pr-testing-NNNN and batteries-pr-testing-NNNN branches
         if: always()
         env:
           TOKEN: ${{ secrets.LEAN_PR_TESTING }}
@@ -300,7 +301,8 @@ jobs:
           LINT_OUTCOME: ${{ steps.lint.outcome }}
           TEST_OUTCOME: ${{ steps.test.outcome }}
         run: |
-          scripts/lean-pr-testing-comments.sh
+          scripts/lean-pr-testing-comments.sh lean
+          scripts/lean-pr-testing-comments.sh batteries
 
   final:
     name: Post-CI job

.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
@@ -149,8 +150,8 @@ jobs:
         run: |
           rm -rf .lake/build/lib/Mathlib/
           # Fail quickly if the cache is completely cold, by checking for Mathlib.Init
-          lake exe cache get Mathlib.Init
-          lake build --no-build Mathlib.Init && lake exe cache get || echo "No cache for 'Mathlib.Init' available"
+          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
@@ -294,7 +295,7 @@ jobs:
       # Output is posted to the zulip topic
       # https://leanprover.zulipchat.com/#narrow/stream/345428-mathlib-reviewers/topic/lean4checker
 
-      - name: Post comments for lean-pr-testing branch
+      - name: Post comments for lean-pr-testing-NNNN and batteries-pr-testing-NNNN branches
         if: always()
         env:
           TOKEN: ${{ secrets.LEAN_PR_TESTING }}
@@ -307,7 +308,8 @@ jobs:
           LINT_OUTCOME: ${{ steps.lint.outcome }}
           TEST_OUTCOME: ${{ steps.test.outcome }}
         run: |
-          scripts/lean-pr-testing-comments.sh
+          scripts/lean-pr-testing-comments.sh lean
+          scripts/lean-pr-testing-comments.sh batteries
 
   final:
     name: Post-CI job

.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
@@ -146,8 +147,8 @@ jobs:
         run: |
           rm -rf .lake/build/lib/Mathlib/
           # Fail quickly if the cache is completely cold, by checking for Mathlib.Init
-          lake exe cache get Mathlib.Init
-          lake build --no-build Mathlib.Init && lake exe cache get || echo "No cache for 'Mathlib.Init' available"
+          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
@@ -291,7 +292,7 @@ jobs:
       # Output is posted to the zulip topic
       # https://leanprover.zulipchat.com/#narrow/stream/345428-mathlib-reviewers/topic/lean4checker
 
-      - name: Post comments for lean-pr-testing branch
+      - name: Post comments for lean-pr-testing-NNNN and batteries-pr-testing-NNNN branches
         if: always()
         env:
           TOKEN: ${{ secrets.LEAN_PR_TESTING }}
@@ -304,7 +305,8 @@ jobs:
           LINT_OUTCOME: ${{ steps.lint.outcome }}
           TEST_OUTCOME: ${{ steps.test.outcome }}
         run: |
-          scripts/lean-pr-testing-comments.sh
+          scripts/lean-pr-testing-comments.sh lean
+          scripts/lean-pr-testing-comments.sh batteries
 
   final:
     name: Post-CI job (fork)

.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

@@ -23,6 +23,7 @@ jobs:
         topic: 'Mathlib status updates'
         content: |
           ❌ The latest CI for Mathlib's branch#nightly-testing has [failed](https://github.com/${{ github.repository }}/actions/runs/${{ github.event.workflow_run.id }}) ([${{ github.sha }}](https://github.com/${{ github.repository }}/commit/${{ github.sha }})).
+          You can `git fetch; git checkout nightly-testing` and push a fix.
 
   handle_success:
     if: ${{ github.event.workflow_run.conclusion == 'success' && github.event.workflow_run.head_branch == 'nightly-testing' }}
@@ -210,26 +211,15 @@ 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"
-            # 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)
+            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)
         else:
             print('No action needed.')

.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:

.github/workflows/update_dependencies_zulip.yml

@@ -40,7 +40,7 @@ jobs:
                 });
               }
             } else {
-              output += "No PR found for this run!";
+              output += "No PR found for this run! If you are feeling impatient and have write access, please go to the following page and click the "Run workflow" button!\nhttps://github.com/leanprover-community/mathlib4/actions/workflows/update_dependencies.yml";
             }
             return output;
 

.vscode/deprecated-alias.code-snippets → .vscode/deprecated.code-snippets

@@ -1,4 +1,11 @@
 {
+	"Deprecation for mathlib": {
+		"scope": "lean4",
+		"prefix": "deprecated",
+		"body": [
+			"@[deprecated $1 (since := \"${CURRENT_YEAR}-${CURRENT_MONTH}-${CURRENT_DATE}\")]"
+		]
+	},
 	"Deprecated alias for mathlib": {
 		"scope": "lean4",
 		"prefix": "deprecated alias",