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

Author: CBirkbeck

.devcontainer/devcontainer.json

@@ -1,9 +1,7 @@
 {
   "name": "Mathlib4 dev container",
 
-  "build": {
-    "dockerfile": "Dockerfile"
-  },
+  "image": "ghcr.io/leanprover-community/mathlib4/gitpod",
 
   "onCreateCommand": "lake exe cache get!",
 

.github/build.in.yml

@@ -1,7 +1,13 @@
 name: Post PR summary comment
 
 on:
-  pull_request:
+  pull_request_target:
+
+# Limit permissions for GITHUB_TOKEN for the entire workflow
+permissions:
+  contents: read
+  pull-requests: write  # Only allow PR comments/labels
+  # All other permissions are implicitly 'none'
 
 jobs:
   build:
@@ -12,11 +18,25 @@ jobs:
     - name: Checkout code
       uses: actions/checkout@11bd71901bbe5b1630ceea73d27597364c9af683 # v4.2.2
       with:
+        ref: ${{ github.event.pull_request.head.sha }}
         fetch-depth: 0
+        path: pr-branch
+
+    # Checkout the master branch into a subdirectory
+    - name: Checkout master branch
+      uses: actions/checkout@11bd71901bbe5b1630ceea73d27597364c9af683 # v4.2.2
+      with:
+        # When testing the scripts, comment out the "ref: master"
+        ref: master
+        path: master-branch
 
     - name: Update the merge-conflict label
       run: |
+        cd pr-branch
         printf 'PR number: "%s"\n' "${{ github.event.pull_request.number }}"
+        git config user.name "leanprover-community-mathlib4-bot"
+        git config user.email "leanprover-community-mathlib4-bot@users.noreply.github.com"
+
         if git merge origin/master --no-ff --no-commit
         then
           git merge --abort || true
@@ -27,7 +47,7 @@ jobs:
             --url https://api.github.com/repos/${{ github.repository }}/issues/${{ github.event.pull_request.number }}/labels/merge-conflict \
             --header 'authorization: Bearer ${{ secrets.GITHUB_TOKEN }}'
         else
-          echo "This PR has merge conflicts with main."
+          echo "This PR has merge conflicts with master."
           # we use curl rather than octokit/request-action so that the job won't fail
           # (and send an annoying email) if the labels don't exist
           curl --request POST \
@@ -36,7 +56,6 @@ jobs:
             --header 'X-GitHub-Api-Version: 2022-11-28' \
             --url https://api.github.com/repos/${{ github.repository }}/issues/${{ github.event.pull_request.number }}/labels \
             --data '{"labels":["merge-conflict"]}'
-
         fi
 
     - name: Set up Python
@@ -52,10 +71,12 @@ jobs:
 
     - name: Get changed and removed/renamed files
       run: |
+        cd pr-branch
         git fetch origin ${{ github.base_ref }}  # fetch the base branch
 
         # Get the list of all changed files.
-        git diff --name-only origin/${{ github.base_ref }}... > changed_files.txt
+        echo "Saving the changed files to 'changed_files.txt'..."
+        git diff --name-only origin/${{ github.base_ref }}... | tee changed_files.txt
 
         # Get all files which were removed or renamed.
         echo "Checking for removed files..."
@@ -87,61 +108,79 @@ jobs:
 
     - name: Compute (re)moved files without deprecation
       run: |
+        cd pr-branch
         touch moved_without_deprecation.txt
+        touch extraneous_deprecated_module.txt
         git checkout ${{ github.base_ref }}
-        for file in $(cat removed_files.txt) ; do
+        while IFS= read -r file
+        do
           if grep ^deprecated_module "${file}" ; then
-            printf 'info: removed file %s contains a deprecation\n' "${file}"
+            # shellcheck disable=SC2016
+            printf '\n⚠️ **warning**: removed file `%s` contains a module deprecation: please add this in a follow-up PR instead\n' "${file}" |
+              tee -a extraneous_deprecated_module.txt
           else
-            printf '\n⚠️ **warning**: file `%s` was removed without a module deprecation\n' "${file}" |
+            # shellcheck disable=SC2016
+            printf '\nnote: file `%s` was removed.\nPlease create a follow-up pull request adding a module deprecation. Thanks!\n' "${file}" |
               tee -a moved_without_deprecation.txt
           fi
-        done
+        done < removed_files.txt
         IFS=$'\n'
-        for file in $(cat renamed_files.txt) ; do
-          printf '\n⚠️ **warning**: file %s without a module deprecation\n' "${file}" |
-            tee -a moved_without_deprecation.txt
-        done
+        while IFS= read -r file
+        do
+          if grep ^deprecated_module "${file}" ; then
+            # shellcheck disable=SC2016
+            printf '\n⚠️ **warning**: renamed file `%s` contains a module deprecation: please add this in a follow-up PR instead\n' "${file}" |
+              tee -a extraneous_deprecated_module.txt
+          else
+            # shellcheck disable=SC2016
+            printf '\nnote: file `%s` without a module deprecation\nPlease create a follow-up pull request adding one. Thanks!\n' "${file}" |
+              tee -a moved_without_deprecation.txt
+          fi
+        done < renamed_files.txt
 
         # we return to the PR branch, since the next step wants it!
         git checkout -
 
     - name: Compute transitive imports
       run: |
+        cd pr-branch
         # the checkout dance, to avoid a detached head
         git checkout master
         git checkout -
         currentHash="$(git rev-parse HEAD)"
+        printf 'currentHash=%s\n' "${currentHash}"
 
-        # Compute the counts for the HEAD of the PR
-        python ./scripts/count-trans-deps.py "Mathlib/" > head.json
+        echo "Compute the counts for the HEAD of the PR"
+        python ../master-branch/scripts/count-trans-deps.py "Mathlib/" > head.json
 
         # Checkout the merge base
-        git checkout "$(git merge-base master ${{ github.sha }})"
+        git checkout "$(git merge-base master ${{ github.event.pull_request.head.sha }})"
 
-        # Compute the counts for the merge base
-        python ./scripts/count-trans-deps.py "Mathlib/" > base.json
+        echo "Compute the counts for the merge base"
+        python ../master-branch/scripts/count-trans-deps.py "Mathlib/" > base.json
 
         # switch back to the current branch: the `declarations_diff` script should be here
-        git checkout "${currentHash}"
+        git checkout "${currentHash}" --
 
     - name: Post or update the summary comment
       env:
-        GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }}
+        GH_TOKEN: ${{ secrets.GITHUB_TOKEN }}
         BRANCH_NAME: ${{ github.head_ref }}
       run: |
+        cd pr-branch
+        currentHash="$(git rev-parse HEAD)"
         PR="${{ github.event.pull_request.number }}"
         title="### PR summary"
 
-        graphAndHighPercentReports=$(python ./scripts/import-graph-report.py base.json head.json changed_files.txt)
+        graphAndHighPercentReports=$(python ../master-branch/scripts/import-graph-report.py base.json head.json changed_files.txt)
 
-        ## Import count comment
+        echo "Produce import count comment"
         importCount=$(
           printf '%s\n' "${graphAndHighPercentReports}" | sed '/^Import changes exceeding/Q'
-          ./scripts/import_trans_difference.sh
+          ../master-branch/scripts/import_trans_difference.sh
         )
 
-        ## High percentage imports
+        echo "Produce high percentage imports"
         high_percentages=$(
           printf '%s\n' "${graphAndHighPercentReports}" | sed -n '/^Import changes exceeding/,$p'
         )
@@ -161,36 +200,43 @@ jobs:
           importCount="$(printf '#### Import changes for modified files\n\n%s\n' "${importCount}")"
         fi
 
-        ## Declarations' diff comment
-        declDiff=$(./scripts/declarations_diff.sh)
+        echo "Compute Declarations' diff comment"
+        declDiff=$(../master-branch/scripts/declarations_diff.sh)
         if [ "$(printf '%s' "${declDiff}" | wc -l)" -gt 15 ]
         then
           declDiff="$(printf '<details><summary>\n\n%s\n\n</summary>\n\n%s\n\n</details>\n' "#### Declarations diff" "${declDiff}")"
         else
           declDiff="$(printf '#### Declarations diff\n\n%s\n' "${declDiff}")"
         fi
-        git checkout "${BRANCH_NAME}"
-        currentHash="$(git rev-parse HEAD)"
+        git checkout "${currentHash}" --
         hashURL="https://github.com/${{ github.repository }}/pull/${{ github.event.pull_request.number }}/commits/${currentHash}"
+        printf 'hashURL: %s' "${hashURL}"
 
-        ## Technical debt changes
-        techDebtVar="$(./scripts/technical-debt-metrics.sh pr_summary)"
+        echo "Compute technical debt changes"
+        techDebtVar="$(../master-branch/scripts/technical-debt-metrics.sh pr_summary)"
 
         # store in a file, to avoid "long arguments" error.
         printf '%s [%s](%s)%s\n\n%s\n\n---\n\n%s\n\n---\n\n%s\n' "${title}" "$(git rev-parse --short HEAD)" "${hashURL}" "${high_percentages}" "${importCount}" "${declDiff}" "${techDebtVar}" > please_merge_master.md
 
-        # At the end, include any errors about removed or renamed files without deprecation.
+        echo "Include any errors about removed or renamed files without deprecation,"
+        echo "as well as errors about extraneous deprecated_module additions."
         if [ -s moved_without_deprecation.txt ]
         then
           printf '\n\n---\n\n' >> please_merge_master.md
           cat moved_without_deprecation.txt >> please_merge_master.md
         fi
+        if [ -s extraneous_deprecated_module.txt ]
+        then
+          printf '\n\n---\n\n' >> please_merge_master.md
+          cat extraneous_deprecated_module.txt >> please_merge_master.md
+        fi
 
         cat please_merge_master.md
-        ./scripts/update_PR_comment.sh please_merge_master.md "${title}" "${PR}"
+        ../master-branch/scripts/update_PR_comment.sh please_merge_master.md "${title}" "${PR}"
 
     - name: Update the file-removed label
       run: |
+        cd pr-branch
         undeprecatedMoves="$(cat moved_without_deprecation.txt)"
         if [ -n "$undeprecatedMoves" ]; then
           echo "This PR has undeprecated module (re)movals."

.github/workflows/PR_summary.yml

@@ -1,42 +1,64 @@
 name: Autolabel PRs
 
 on:
-  pull_request:
+  pull_request_target:
     types: [opened]
   push:
     paths:
       - scripts/autolabel.lean
       - .github/workflows/add_label_from_diff.yaml
 
+# Limit permissions for GITHUB_TOKEN for the entire workflow
+permissions:
+  contents: read
+  pull-requests: write  # Only allow PR comments/labels
+  # All other permissions are implicitly 'none'
+
 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@11bd71901bbe5b1630ceea73d27597364c9af683 # v4.2.2
-        with:
-          fetch-depth: 0
-      - name: Configure Lean
-        uses: leanprover/lean-action@f807b338d95de7813c5c50d018f1c23c9b93b4ec # 2025-04-24
-        with:
-          auto-config: false
-          use-github-cache: false
-          use-mathlib-cache: false
-      - 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 }}
+    - name: Checkout code
+      uses: actions/checkout@11bd71901bbe5b1630ceea73d27597364c9af683 # v4.2.2
+      with:
+        ref: ${{ github.event.pull_request.head.sha }}
+        fetch-depth: 0
+    - name: Configure Lean
+      uses: leanprover/lean-action@f807b338d95de7813c5c50d018f1c23c9b93b4ec # 2025-04-24
+      with:
+        auto-config: false
+        use-github-cache: false
+        use-mathlib-cache: false
+    - name: lake exe autolabel
+      run: |
+        # the checkout dance, to avoid a detached head
+        git checkout master
+        git checkout -
+        labels="$(lake exe autolabel)"
+        printf '%s\n' "${labels}"
+        # extract
+        label="$(printf '%s' "${labels}" | sed -n 's=.*#\[\([^,]*\)\].*=\1=p')"
+        printf 'label: "%s"\n' "${label}"
+        if [ -n "${label}" ]
+        then
+          printf 'Applying label %s\n' "${label}"
+          # we use curl rather than octokit/request-action so that the job won't fail
+          # (and send an annoying email) if the labels don't exist
+          url="https://api.github.com/repos/${{ github.repository }}/issues/${{ github.event.pull_request.number }}/labels"
+          printf 'url: %s\n' "${url}"
+          jsonLabel="$(printf '{"labels":["%s"]}' "${label}")"
+          printf 'jsonLabel: %s\n' "${jsonLabel}"
+          curl --request POST \
+            --header 'Accept: application/vnd.github+json' \
+            --header 'authorization: Bearer ${{ secrets.GITHUB_TOKEN }}' \
+            --header 'X-GitHub-Api-Version: 2022-11-28' \
+            --url "${url}" \
+            --data "${jsonLabel}"
+        else
+          echo "There is no single label that we could apply, so we are not applying any label."
+        fi
+      env:
+        GH_TOKEN: ${{ secrets.GITHUB_TOKEN }}