Merge remote-tracking branch 'upstream/master' into prod-lp-measure

Author: wwylele

.github/workflows/PR_summary.yml

@@ -23,13 +23,16 @@ jobs:
         fetch-depth: 0
         path: pr-branch
 
-    # Checkout the master branch into a subdirectory
-    - name: Checkout master branch
+    - name: Checkout mathlib-ci
       uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2
       with:
-        # When testing the scripts, comment out the "ref: master"
-        ref: master
-        path: master-branch
+        repository: leanprover-community/mathlib-ci
+        ref: 4af75ac0b0d1aaf38d4546a779bc5c68b4d75069
+        fetch-depth: 1
+        path: ci-tools
+
+    - name: Set up CI scripts paths
+      uses: ./ci-tools/.github/actions/setup-ci-scripts
 
     - name: Update the merge-conflict label
       run: |
@@ -79,6 +82,10 @@ jobs:
         echo "Saving the changed files to 'changed_files.txt'..."
         git diff --name-only origin/${{ github.base_ref }}... | tee changed_files.txt
 
+        # Get all newly added files.
+        echo "Checking for added files..."
+        git diff --name-only --diff-filter A origin/${{ github.base_ref }}... | tee added_files.txt
+
         # Get all files which were removed or renamed.
         echo "Checking for removed files..."
 
@@ -152,13 +159,13 @@ jobs:
         printf 'currentHash=%s\n' "${currentHash}"
 
         echo "Compute the counts for the HEAD of the PR"
-        python ../master-branch/scripts/count-trans-deps.py "Mathlib/" > head.json
+        python "${CI_SCRIPTS_DIR}/pr_summary/count-trans-deps.py" "Mathlib/" > head.json
 
         # Checkout the merge base
         git checkout "$(git merge-base master ${{ github.event.pull_request.head.sha }})"
 
         echo "Compute the counts for the merge base"
-        python ../master-branch/scripts/count-trans-deps.py "Mathlib/" > base.json
+        python "${CI_SCRIPTS_DIR}/pr_summary/count-trans-deps.py" "Mathlib/" > base.json
 
         # switch back to the current branch: the `declarations_diff` script should be here
         git checkout "${currentHash}" --
@@ -173,12 +180,12 @@ jobs:
         PR="${{ github.event.pull_request.number }}"
         title="### PR summary"
 
-        graphAndHighPercentReports=$(python ../master-branch/scripts/import-graph-report.py base.json head.json changed_files.txt)
+        graphAndHighPercentReports=$(python "${CI_SCRIPTS_DIR}/pr_summary/import-graph-report.py" base.json head.json changed_files.txt)
 
         echo "Produce import count comment"
         importCount=$(
           printf '%s\n' "${graphAndHighPercentReports}" | sed '/^Import changes exceeding/Q'
-          ../master-branch/scripts/import_trans_difference.sh
+          "${CI_SCRIPTS_DIR}/pr_summary/import_trans_difference.sh"
         )
 
         echo "Produce high percentage imports"
@@ -202,7 +209,7 @@ jobs:
         fi
 
         echo "Compute Declarations' diff comment"
-        declDiff=$(../master-branch/scripts/declarations_diff.sh)
+        declDiff=$("${CI_SCRIPTS_DIR}/pr_summary/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}")"
@@ -214,10 +221,40 @@ jobs:
         printf 'hashURL: %s' "${hashURL}"
 
         echo "Compute technical debt changes"
-        techDebtVar="$(../master-branch/scripts/technical-debt-metrics.sh pr_summary)"
+        techDebtVar="$("${CI_SCRIPTS_DIR}/reporting/technical-debt-metrics.sh" pr_summary)"
+
+        echo "Compute documentation reminder"
+        workflowFilesChanged="$(grep '^\.github/workflows/' changed_files.txt || true)"
+        if [ -n "${workflowFilesChanged}" ]
+        then
+          # Format each changed workflow path as a Markdown bullet: "- `path`"
+          workflowFilesChangedMarkdown="$(sed "s|^|- \`|; s|\$|\`|" <<< "${workflowFilesChanged}")"
+          workflowDocsReminder="$(printf "### Workflow documentation reminder\nThis PR modifies files under \`.github/workflows/\`.\nPlease update \`docs/workflows.md\` if the workflow inventory, triggers, or behavior changed.\n\nModified workflow files:\n%s\n" "${workflowFilesChangedMarkdown}")"
+        else
+          workflowDocsReminder=""
+        fi
+
+        echo "Compute scripts-location reminder"
+        scriptsFilesAdded="$(grep '^scripts/' added_files.txt || true)"
+        if [ -n "${scriptsFilesAdded}" ]
+        then
+          # Format each added scripts path as a Markdown bullet: "- `path`"
+          scriptsFilesAddedMarkdown="$(sed "s|^|- \`|; s|\$|\`|" <<< "${scriptsFilesAdded}")"
+          scriptsLocationReminder="$(printf "### Scripts folder reminder\nThis PR adds files under \`scripts/\`.\nPlease consider whether each added script belongs in this repository or in \`leanprover-community/mathlib-ci\`.\n\nAdded scripts files:\n%s\n" "${scriptsFilesAddedMarkdown}")"
+        else
+          scriptsLocationReminder=""
+        fi
 
         # 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
+        if [ -n "${workflowDocsReminder}" ]
+        then
+          printf '\n\n---\n\n%s\n' "${workflowDocsReminder}" >> please_merge_master.md
+        fi
+        if [ -n "${scriptsLocationReminder}" ]
+        then
+          printf '\n\n---\n\n%s\n' "${scriptsLocationReminder}" >> please_merge_master.md
+        fi
 
         echo "Include any errors about removed or renamed files without deprecation,"
         echo "as well as errors about extraneous deprecated_module additions."
@@ -233,7 +270,7 @@ jobs:
         fi
 
         cat please_merge_master.md
-        ../master-branch/scripts/update_PR_comment.sh please_merge_master.md "${title}" "${PR}"
+        "${CI_SCRIPTS_DIR}/pr_summary/update_PR_comment.sh" please_merge_master.md "${title}" "${PR}"
 
     - name: Update the file-removed label
       run: |

.github/workflows/actionlint.yml

@@ -16,4 +16,16 @@ jobs:
         uses: reviewdog/action-actionlint@e58ee9d111489c31395fbe4857b0be6e7635dbda # v1.70.0
         with:
           tool_name: actionlint
-          fail_level: error
+          fail_level: any
+
+  ensure-sha-pinned-actions:
+    runs-on: ubuntu-latest
+    steps:
+      - name: Checkout
+        uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2
+
+      # Using our fork's PR branch until upstream merges the improved error reporting:
+      # https://github.com/zgosalvez/github-actions-ensure-sha-pinned-actions/pull/288
+      # TODO: Update to upstream release once merged.
+      - name: Ensure all actions are pinned to SHA
+        uses: kim-em/github-actions-ensure-sha-pinned-actions@00f51cdb5bbc21f5bc873ef3a2dceef45df213af # improve-error-reporting

.github/workflows/add_label_from_diff.yaml

@@ -21,33 +21,42 @@ jobs:
     # Don't run on forks, where we wouldn't have permissions to add the label anyway.
     if: github.repository == 'leanprover-community/mathlib4'
     steps:
-    - name: Checkout code
+    - name: Checkout master branch to build autolabel from
       uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2
       with:
-        ref: ${{ github.event.pull_request.head.sha }}
-        fetch-depth: 0
+        ref: master
+        path: tools
     - name: Configure Lean
       uses: leanprover/lean-action@c544e89643240c6b398f14a431bcdc6309e36b3e # v1.4.0
       with:
         auto-config: false
         use-github-cache: false
         use-mathlib-cache: false
-    - name: lake exe autolabel
+        lake-package-directory: tools # Building here
+    - name: Build autolabel from master
+      working-directory: tools
+      run: |
+        lake build autolabel
+    - name: Checkout branch to label
+      uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2
+      with:
+        ref: ${{ github.event.pull_request.head.sha || github.sha }}
+        fetch-depth: 0
+        path: pr-branch
+    - name: Run autolabel
+      working-directory: pr-branch
       run: |
-        # the checkout dance, to avoid a detached head
-        git checkout master
-        git checkout -
-        labels="$(lake exe autolabel)"
+        labels="$("${GITHUB_WORKSPACE}/tools/.lake/build/bin/autolabel")"
         printf '%s\n' "${labels}"
         # extract
         label="$(printf '%s' "${labels}" | sed -n 's=^::notice::.*#\[\([^,]*\)\].*=\1=p')"
         printf 'label: "%s"\n' "${label}"
-        if [ -n "${label}" ]
+        if [ -n "${label}" ] && [ -n "${PR_NUMBER}" ]
         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"
+          url="https://api.github.com/repos/${{ github.repository }}/issues/${PR_NUMBER}/labels"
           printf 'url: %s\n' "${url}"
           jsonLabel="$(printf '{"labels":["%s"]}' "${label}")"
           printf 'jsonLabel: %s\n' "${jsonLabel}"
@@ -62,3 +71,6 @@ jobs:
         fi
       env:
         GH_TOKEN: ${{ secrets.GITHUB_TOKEN }}
+        # the PR number could be undefined in workflows triggered by 'push',
+        # in which case we only log the applicable label and exit
+        PR_NUMBER: ${{ github.event.pull_request.number }}

.github/workflows/auto_assign_reviewers.yaml

@@ -26,6 +26,9 @@ jobs:
     with:
       concurrency_group: ${{ github.workflow }}-${{ github.ref }}-${{ github.run_id }}
       pr_branch_ref: ${{ github.sha }}
-      # We don't wan't 'bors try' runs to compete with merge-candidates, so we pool trying with PR runs
+      # bors runs should build the tools from their commit-under-test: after all, we are trying to
+      # test 'what would happen if this was merged', so we need to use the 'would-be-post-merge' tools
+      tools_branch_ref: ${{ github.sha }}
+      # We don't want 'bors try' runs to compete with merge-candidates, so we pool trying with PR runs
       runs_on: ${{ github.ref_name == 'trying' && 'pr' || 'bors' }}
     secrets: inherit

.github/workflows/bors.yml

@@ -10,6 +10,8 @@ on:
       # ignore staging and trying branches used by bors, these are handled by bors.yml
       - 'staging'
       - 'trying'
+      # ignore branches meant for experiments
+      - 'ci-dev/**'
   merge_group:
 
 concurrency: