Merge branch 'master' into pfaffelh_compactSystem

Author: pfaffelh

.github/build.in.yml

@@ -136,9 +136,8 @@ jobs:
         shell: bash # We're only building the `master` branch version of the tools, so don't need to run inside landrun.
         run: |
           cd master-branch
-          lake build cache mk_all check-yaml graph
+          lake build cache check-yaml graph
           ls .lake/build/bin/cache
-          ls .lake/build/bin/mk_all
           ls .lake/build/bin/check-yaml
           ls .lake/packages/importGraph/.lake/build/bin/graph
 
@@ -219,13 +218,11 @@ jobs:
       - name: update {Mathlib, Tactic, Counterexamples, Archive}.lean
         id: mk_all
         continue-on-error: true # Allow workflow to continue, outcome checked later
-        # This only runs `mk_all --check` from the `master-branch`, so doesn't need to be inside landrun
-        shell: bash
+        # This runs `mk_all --check` from the `pr-branch` inside landrun
         run: |
           cd pr-branch
-
-          echo "Running mk_all --check (from master-branch)..."
-          LAKE_HOME="$TOOLCHAIN_DIR" ../master-branch/.lake/build/bin/mk_all --check
+          echo "Running mk_all --check (from pr-branch)..."
+          lake exe mk_all --check
 
       - name: begin gh-problem-match-wrap for build step
         uses: leanprover-community/gh-problem-matcher-wrap@20007cb926a46aa324653a387363b52f07709845 # 2025-04-23
@@ -422,6 +419,7 @@ jobs:
 
   post_steps:
     name: Post-Build StepJOB_NAME
+    if: FORK_CONDITION
     needs: [build]
     runs-on: ubuntu-latest # Note these steps run on disposable GitHub runners, so no landrun sandboxing is needed.
     steps:
@@ -503,20 +501,34 @@ jobs:
 
   style_lint:
     name: Lint styleJOB_NAME
+    if: FORK_CONDITION
     runs-on: ubuntu-latest
     steps:
       - uses: leanprover-community/lint-style-action@f2e7272aad56233a642b08fe974cf09dd664b0c8 # 2025-05-22
         with:
           mode: check
           lint-bib-file: true
 
+  build_and_lint:
+    name: CI Success
+    if: FORK_CONDITION
+    needs: [style_lint, post_steps]
+    runs-on: ubuntu-latest
+    steps:
+      - name: succeed
+        run: |
+          echo "Success: Required build and lint checks completed!"
+
   final:
     name: Post-CI jobJOB_NAME
     if: FORK_CONDITION
     needs: [style_lint, build, post_steps]
     runs-on: ubuntu-latest
     steps:
-      - id: PR
+      # This action is used to determine the PR metadata in the event of a push.
+      # If it is called from a PR from a fork, it will find nothing/irrelevant data.
+      - if: github.event_name != 'pull_request_target'
+        id: PR_from_push
         uses: 8BitJonny/gh-get-current-pr@08e737c57a3a4eb24cec6487664b243b77eb5e36 # 3.0.0
         # TODO: this may not work properly if the same commit is pushed to multiple branches:
         # https://github.com/8BitJonny/gh-get-current-pr/issues/8
@@ -525,6 +537,13 @@ jobs:
           # Only return if PR is still open
           filterOutClosed: true
 
+      # Combine the output from the previous action with the metadata supplied by GitHub itself.
+      - id: PR
+        shell: bash
+        run: |
+          echo "number=${{ steps.PR_from_push.outputs.number || github.event.pull_request.number }}" >> $GITHUB_OUTPUT
+          echo "pr_labels=${{ steps.PR_from_push.outputs.pr_labels || join(github.event.pull_request.labels.*.name, ',') }}" >> $GITHUB_OUTPUT
+
       - if: contains(steps.PR.outputs.pr_labels, 'bench-after-CI')
         name: If `bench-after-CI` is present, add a `!bench` comment.
         uses: GrantBirki/comment@608e41b19bc973020ec0e189ebfdae935d7fe0cc # v2.1.1

.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

@@ -38,7 +38,7 @@ permissions:
 
 jobs:
   build:
-    if: true
+    if: github.repository == 'leanprover-community/mathlib4'
     name: Build
     runs-on: bors
     outputs:
@@ -146,9 +146,8 @@ jobs:
         shell: bash # We're only building the `master` branch version of the tools, so don't need to run inside landrun.
         run: |
           cd master-branch
-          lake build cache mk_all check-yaml graph
+          lake build cache check-yaml graph
           ls .lake/build/bin/cache
-          ls .lake/build/bin/mk_all
           ls .lake/build/bin/check-yaml
           ls .lake/packages/importGraph/.lake/build/bin/graph
 
@@ -229,13 +228,11 @@ jobs:
       - name: update {Mathlib, Tactic, Counterexamples, Archive}.lean
         id: mk_all
         continue-on-error: true # Allow workflow to continue, outcome checked later
-        # This only runs `mk_all --check` from the `master-branch`, so doesn't need to be inside landrun
-        shell: bash
+        # This runs `mk_all --check` from the `pr-branch` inside landrun
         run: |
           cd pr-branch
-
-          echo "Running mk_all --check (from master-branch)..."
-          LAKE_HOME="$TOOLCHAIN_DIR" ../master-branch/.lake/build/bin/mk_all --check
+          echo "Running mk_all --check (from pr-branch)..."
+          lake exe mk_all --check
 
       - name: begin gh-problem-match-wrap for build step
         uses: leanprover-community/gh-problem-matcher-wrap@20007cb926a46aa324653a387363b52f07709845 # 2025-04-23
@@ -432,6 +429,7 @@ jobs:
 
   post_steps:
     name: Post-Build Step
+    if: github.repository == 'leanprover-community/mathlib4'
     needs: [build]
     runs-on: ubuntu-latest # Note these steps run on disposable GitHub runners, so no landrun sandboxing is needed.
     steps:
@@ -513,20 +511,34 @@ jobs:
 
   style_lint:
     name: Lint style
+    if: github.repository == 'leanprover-community/mathlib4'
     runs-on: ubuntu-latest
     steps:
       - uses: leanprover-community/lint-style-action@f2e7272aad56233a642b08fe974cf09dd664b0c8 # 2025-05-22
         with:
           mode: check
           lint-bib-file: true
 
+  build_and_lint:
+    name: CI Success
+    if: github.repository == 'leanprover-community/mathlib4'
+    needs: [style_lint, post_steps]
+    runs-on: ubuntu-latest
+    steps:
+      - name: succeed
+        run: |
+          echo "Success: Required build and lint checks completed!"
+
   final:
     name: Post-CI job
-    if: true
+    if: github.repository == 'leanprover-community/mathlib4'
     needs: [style_lint, build, post_steps]
     runs-on: ubuntu-latest
     steps:
-      - id: PR
+      # This action is used to determine the PR metadata in the event of a push.
+      # If it is called from a PR from a fork, it will find nothing/irrelevant data.
+      - if: github.event_name != 'pull_request_target'
+        id: PR_from_push
         uses: 8BitJonny/gh-get-current-pr@08e737c57a3a4eb24cec6487664b243b77eb5e36 # 3.0.0
         # TODO: this may not work properly if the same commit is pushed to multiple branches:
         # https://github.com/8BitJonny/gh-get-current-pr/issues/8
@@ -535,6 +547,13 @@ jobs:
           # Only return if PR is still open
           filterOutClosed: true
 
+      # Combine the output from the previous action with the metadata supplied by GitHub itself.
+      - id: PR
+        shell: bash
+        run: |
+          echo "number=${{ steps.PR_from_push.outputs.number || github.event.pull_request.number }}" >> $GITHUB_OUTPUT
+          echo "pr_labels=${{ steps.PR_from_push.outputs.pr_labels || join(github.event.pull_request.labels.*.name, ',') }}" >> $GITHUB_OUTPUT
+
       - if: contains(steps.PR.outputs.pr_labels, 'bench-after-CI')
         name: If `bench-after-CI` is present, add a `!bench` comment.
         uses: GrantBirki/comment@608e41b19bc973020ec0e189ebfdae935d7fe0cc # v2.1.1

.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

@@ -45,7 +45,7 @@ permissions:
 
 jobs:
   build:
-    if: true
+    if: github.repository == 'leanprover-community/mathlib4'
     name: Build
     runs-on: pr
     outputs:
@@ -153,9 +153,8 @@ jobs:
         shell: bash # We're only building the `master` branch version of the tools, so don't need to run inside landrun.
         run: |
           cd master-branch
-          lake build cache mk_all check-yaml graph
+          lake build cache check-yaml graph
           ls .lake/build/bin/cache
-          ls .lake/build/bin/mk_all
           ls .lake/build/bin/check-yaml
           ls .lake/packages/importGraph/.lake/build/bin/graph
 
@@ -236,13 +235,11 @@ jobs:
       - name: update {Mathlib, Tactic, Counterexamples, Archive}.lean
         id: mk_all
         continue-on-error: true # Allow workflow to continue, outcome checked later
-        # This only runs `mk_all --check` from the `master-branch`, so doesn't need to be inside landrun
-        shell: bash
+        # This runs `mk_all --check` from the `pr-branch` inside landrun
         run: |
           cd pr-branch
-
-          echo "Running mk_all --check (from master-branch)..."
-          LAKE_HOME="$TOOLCHAIN_DIR" ../master-branch/.lake/build/bin/mk_all --check
+          echo "Running mk_all --check (from pr-branch)..."
+          lake exe mk_all --check
 
       - name: begin gh-problem-match-wrap for build step
         uses: leanprover-community/gh-problem-matcher-wrap@20007cb926a46aa324653a387363b52f07709845 # 2025-04-23
@@ -439,6 +436,7 @@ jobs:
 
   post_steps:
     name: Post-Build Step
+    if: github.repository == 'leanprover-community/mathlib4'
     needs: [build]
     runs-on: ubuntu-latest # Note these steps run on disposable GitHub runners, so no landrun sandboxing is needed.
     steps:
@@ -520,20 +518,34 @@ jobs:
 
   style_lint:
     name: Lint style
+    if: github.repository == 'leanprover-community/mathlib4'
     runs-on: ubuntu-latest
     steps:
       - uses: leanprover-community/lint-style-action@f2e7272aad56233a642b08fe974cf09dd664b0c8 # 2025-05-22
         with:
           mode: check
           lint-bib-file: true
 
+  build_and_lint:
+    name: CI Success
+    if: github.repository == 'leanprover-community/mathlib4'
+    needs: [style_lint, post_steps]
+    runs-on: ubuntu-latest
+    steps:
+      - name: succeed
+        run: |
+          echo "Success: Required build and lint checks completed!"
+
   final:
     name: Post-CI job
-    if: true
+    if: github.repository == 'leanprover-community/mathlib4'
     needs: [style_lint, build, post_steps]
     runs-on: ubuntu-latest
     steps:
-      - id: PR
+      # This action is used to determine the PR metadata in the event of a push.
+      # If it is called from a PR from a fork, it will find nothing/irrelevant data.
+      - if: github.event_name != 'pull_request_target'
+        id: PR_from_push
         uses: 8BitJonny/gh-get-current-pr@08e737c57a3a4eb24cec6487664b243b77eb5e36 # 3.0.0
         # TODO: this may not work properly if the same commit is pushed to multiple branches:
         # https://github.com/8BitJonny/gh-get-current-pr/issues/8
@@ -542,6 +554,13 @@ jobs:
           # Only return if PR is still open
           filterOutClosed: true
 
+      # Combine the output from the previous action with the metadata supplied by GitHub itself.
+      - id: PR
+        shell: bash
+        run: |
+          echo "number=${{ steps.PR_from_push.outputs.number || github.event.pull_request.number }}" >> $GITHUB_OUTPUT
+          echo "pr_labels=${{ steps.PR_from_push.outputs.pr_labels || join(github.event.pull_request.labels.*.name, ',') }}" >> $GITHUB_OUTPUT
+
       - if: contains(steps.PR.outputs.pr_labels, 'bench-after-CI')
         name: If `bench-after-CI` is present, add a `!bench` comment.
         uses: GrantBirki/comment@608e41b19bc973020ec0e189ebfdae935d7fe0cc # v2.1.1