Merge branch 'master' into j-loreaux/CompleteLattice.Group

Author: j-loreaux

.github/build.in.yml

@@ -512,7 +512,7 @@ jobs:
   build_and_lint:
     name: CI Success
     if: FORK_CONDITION
-    needs: [style_lint, build]
+    needs: [style_lint, post_steps]
     runs-on: ubuntu-latest
     steps:
       - name: succeed

.github/workflows/PR_summary.yml

@@ -3,6 +3,12 @@ name: Post PR summary comment
 on:
   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:
     name: "post-or-update-summary-comment"

.github/workflows/add_label_from_diff.yaml

@@ -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 }}

.github/workflows/bors.yml

@@ -522,7 +522,7 @@ jobs:
   build_and_lint:
     name: CI Success
     if: true
-    needs: [style_lint, build]
+    needs: [style_lint, post_steps]
     runs-on: ubuntu-latest
     steps:
       - name: succeed

.github/workflows/bot_fix_style.yaml

@@ -31,4 +31,4 @@ jobs:
         with:
           mode: fix
           lint-bib-file: true
-          bot-fix-style-token: ${{ secrets.GITHUB_TOKEN }}
+          BOT_FIX_STYLE_TOKEN: ${{ secrets.GITHUB_TOKEN }}

.github/workflows/build.yml

@@ -529,7 +529,7 @@ jobs:
   build_and_lint:
     name: CI Success
     if: true
-    needs: [style_lint, build]
+    needs: [style_lint, post_steps]
     runs-on: ubuntu-latest
     steps:
       - name: succeed

.github/workflows/build_fork.yml

@@ -526,7 +526,7 @@ jobs:
   build_and_lint:
     name: CI Success
     if: github.event.pull_request.head.repo.fork
-    needs: [style_lint, build]
+    needs: [style_lint, post_steps]
     runs-on: ubuntu-latest
     steps:
       - name: succeed

.github/workflows/daily.yml

@@ -15,6 +15,7 @@ env:
 jobs:
   check-lean4checker:
     runs-on: ubuntu-latest
+    if: github.repository == 'leanprover-community/mathlib4'
     strategy:
       matrix:
         branch_type: [master, nightly]

.github/workflows/label_new_contributor.yml

@@ -4,6 +4,12 @@ name: Label New Contributors
 
 on: 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:
   label-and-report-new-contributor:
     runs-on: ubuntu-latest

.github/workflows/latest_import.yml

@@ -12,6 +12,7 @@ jobs:
   late-importers:
     name: Build
     runs-on: pr
+    if: github.repository == 'leanprover-community/mathlib4'
     steps:
     - name: cleanup
       run: |