Merge branch 'master' into bjoernkjoshanssen_1st_deriv_test

.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
@@ -69,25 +73,6 @@ jobs:
         run: |
           ./scripts/lint-bib.sh
 
-  check_workflows:
-    if: github.repository MAIN_OR_FORK 'leanprover-community/mathlib4'
-    name: check workflowsJOB_NAME
-    runs-on: ubuntu-latest
-    steps:
-      - name: cleanup
-        run: |
-          find . -name . -o -prune -exec rm -rf -- {} +
-
-      - uses: actions/checkout@v4
-
-      - name: update workflows
-        run: |
-          cd .github/workflows/
-          ./mk_build_yml.sh
-
-      - name: check that workflows were consistent
-        run: git diff --exit-code
-
   build:
     if: github.repository MAIN_OR_FORK 'leanprover-community/mathlib4'
     name: BuildJOB_NAME
@@ -130,9 +115,6 @@ jobs:
           lean --version
           lake --version
 
-      - name: check {Mathlib, Tactic, Counterexamples, Archive}.lean are up to date
-        run: lake exe mk_all --check
-
       - name: build cache
         run: |
           lake build cache
@@ -151,8 +133,20 @@ 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
+        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
@@ -216,6 +210,14 @@ jobs:
           MATHLIB_CACHE_SAS: ${{ secrets.MATHLIB_CACHE_SAS }}
           MATHLIB_CACHE_S3_TOKEN: ${{ secrets.MATHLIB_CACHE_S3_TOKEN }}
 
+      - 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
         run: |
@@ -276,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 }}
@@ -289,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/actionlint.yml

@@ -1,10 +1,5 @@
-name: Actionlint
+name: Check workflows
 on:
-  push:
-    branches:
-      - 'master'
-    paths:
-      - '.github/**'
   pull_request:
     paths:
       - '.github/**'
@@ -14,7 +9,28 @@ jobs:
   actionlint:
     runs-on: ubuntu-latest
     steps:
-    - name: Checkout
-      uses: actions/checkout@v4
-    - name: actionlint
-      uses: raven-actions/actionlint@v1
+      - name: Checkout
+        uses: actions/checkout@v4
+
+      - name: suggester / actionlint
+        uses: reviewdog/action-actionlint@v1
+        with:
+          tool_name: actionlint
+          fail_on_error: true
+
+  check_build_yml:
+    name: check workflows generated by build.in.yml
+    runs-on: ubuntu-latest
+    steps:
+      - uses: actions/checkout@v4
+
+      - name: update workflows
+        run: |
+          cd .github/workflows/
+          ./mk_build_yml.sh
+
+      - name: suggester / build.in.yml
+        uses: reviewdog/action-suggester@v1
+        with:
+          tool_name: mk_build_yml.sh
+          fail_on_error: true

.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
@@ -82,25 +83,6 @@ jobs:
         run: |
           ./scripts/lint-bib.sh
 
-  check_workflows:
-    if: github.repository == 'leanprover-community/mathlib4'
-    name: check workflows
-    runs-on: ubuntu-latest
-    steps:
-      - name: cleanup
-        run: |
-          find . -name . -o -prune -exec rm -rf -- {} +
-
-      - uses: actions/checkout@v4
-
-      - name: update workflows
-        run: |
-          cd .github/workflows/
-          ./mk_build_yml.sh
-
-      - name: check that workflows were consistent
-        run: git diff --exit-code
-
   build:
     if: github.repository == 'leanprover-community/mathlib4'
     name: Build
@@ -143,9 +125,6 @@ jobs:
           lean --version
           lake --version
 
-      - name: check {Mathlib, Tactic, Counterexamples, Archive}.lean are up to date
-        run: lake exe mk_all --check
-
       - name: build cache
         run: |
           lake build cache
@@ -164,8 +143,20 @@ 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
+        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
@@ -229,6 +220,14 @@ jobs:
           MATHLIB_CACHE_SAS: ${{ secrets.MATHLIB_CACHE_SAS }}
           MATHLIB_CACHE_S3_TOKEN: ${{ secrets.MATHLIB_CACHE_S3_TOKEN }}
 
+      - 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
         run: |
@@ -289,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 }}
@@ -302,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