Merge remote-tracking branch 'origin/instmulaction' into galfields_wip

Author: xroblot

.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

@@ -4,6 +4,7 @@ on:
   push:
     branches:
       - staging
+      - trying
 
 concurrency:
   # label each workflow run; only the latest with each label will run
@@ -19,11 +20,15 @@ permissions:
 
 jobs:
   build:
+    name: ci (staging)
     if: ${{ github.repository == 'leanprover-community/mathlib4' || github.repository == 'leanprover-community/mathlib4-nightly-testing' }}
     uses: ./.github/workflows/build_template.yml
     with:
       concurrency_group: ${{ github.workflow }}-${{ github.ref }}-${{ github.run_id }}
       pr_branch_ref: ${{ github.sha }}
-      job_name_suffix: ""
-      runs_on: bors
+      # 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 wan't '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

@@ -7,8 +7,11 @@ on:
       - 'staging.tmp*'
       - 'trying.tmp*'
       - 'staging*.tmp'
-      # ignore staging branch used by bors, this is handled by bors.yml
+      # 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:
@@ -26,11 +29,11 @@ permissions:
 
 jobs:
   build:
+    name: ci
     if: ${{ github.repository == 'leanprover-community/mathlib4' || github.repository == 'leanprover-community/mathlib4-nightly-testing' }}
     uses: ./.github/workflows/build_template.yml
     with:
       concurrency_group: ${{ github.workflow }}-${{ github.ref }}-${{ (github.event_name == 'push' && github.ref == 'refs/heads/master' && github.run_id) || '' }}
       pr_branch_ref: ${{ github.sha }}
-      job_name_suffix: ""
       runs_on: pr
     secrets: inherit

.github/workflows/build.yml

@@ -8,6 +8,11 @@ on:
       - 'trying.tmp*'
       - 'staging*.tmp'
       - 'nolints'
+    paths-ignore:
+      # pull_request_target uses the workflow from the target branch:
+      # PR changes under this directory won't affect this run, so
+      # running it is just wasteful
+      - '.github/workflows/**'
 
 concurrency:
   # label each workflow run; only the latest with each label will run
@@ -24,11 +29,11 @@ permissions:
 
 jobs:
   build:
+    name: ci (fork)
     if: ${{ github.event.pull_request.head.repo.fork && github.repository != 'leanprover-community/mathlib4-nightly-testing' }}
     uses: ./.github/workflows/build_template.yml
     with:
       concurrency_group: ${{ github.workflow }}-${{ github.event.pull_request.number }}
       pr_branch_ref: ${{ github.event.pull_request.head.sha }}
-      job_name_suffix: ' (fork)'
       runs_on: pr
     secrets: inherit