Merge branch 'master' into nontriviality

Author: urkud

.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/bors.yml

@@ -26,6 +26,9 @@ jobs:
     with:
       concurrency_group: ${{ github.workflow }}-${{ github.ref }}-${{ github.run_id }}
       pr_branch_ref: ${{ github.sha }}
+      # 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/build.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:

.github/workflows/build_template.yml

@@ -1,14 +1,22 @@
-# Reusable workflow invoked by build.yml, bors.yml, and build_fork.yml.
+# Reusable workflow invoked by build.yml, bors.yml, build_fork.yml, and ci_dev.yml.
 
 on:
   workflow_call:
     inputs:
       concurrency_group:
         type: string
         required: true
+      tools_branch_ref:
+        type: string
+        required: false
+        default: ''
       pr_branch_ref:
         type: string
         required: true
+      run_post_ci:
+        type: boolean
+        required: false
+        default: true
       runs_on:
         type: string
         required: true
@@ -71,16 +79,16 @@ jobs:
       - name: 'Setup jq'
         uses: dcarbone/install-jq-action@b7ef57d46ece78760b4019dbc4080a1ba2a40b45 # v3.2.0
 
-      # Checkout the master branch into a subdirectory
-      - name: Checkout master branch
+      # Checkout a trusted branch to build the tooling from
+      - name: Checkout tools branch
         uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2
         with:
           # Recall that on the `leanprover-community/mathlib4-nightly-testing` repository,
           # we don't maintain a `master` branch at all.
           # For PRs and pushes to this repository, we will use `nightly-testing-green` instead,
           # so that even when `nightly-testing` is broken, we can still build tools from a known good state.
-          ref: ${{ github.repository == 'leanprover-community/mathlib4-nightly-testing' && 'nightly-testing-green' || 'master' }}
-          path: master-branch
+          ref: ${{ inputs.tools_branch_ref != '' && inputs.tools_branch_ref || (github.repository == 'leanprover-community/mathlib4-nightly-testing' && 'nightly-testing-green' || 'master') }}
+          path: tools-branch
 
       # Checkout the PR branch into a subdirectory
       - name: Checkout PR branch
@@ -160,18 +168,18 @@ jobs:
           # Set it as an environment variable for subsequent steps
           echo "LEAN_SRC_PATH=$LEAN_SRC_PATH" >> "$GITHUB_ENV"
 
-      - name: build master-branch tools
-        shell: bash # We're only building the `master` branch version of the tools, so don't need to run inside landrun.
+      - name: build tools-branch tools
+        shell: bash # We're only building a trusted branch with the tools, so no need to run inside landrun.
         run: |
-          cd master-branch
+          cd tools-branch
           lake build cache check-yaml graph
           ls .lake/build/bin/cache
           ls .lake/build/bin/check-yaml
           ls .lake/packages/importGraph/.lake/build/bin/graph
 
       - name: cleanup .cache/mathlib
         # This needs write access to .cache/mathlib, so can't be run inside landrun.
-        # However it is only using the `master` version of `cache`, so is safe to run outside landrun.
+        # However it is only using the `tools` version of `cache`, so is safe to run outside landrun.
         shell: bash
         run: |
           # Define the cache directory path
@@ -190,8 +198,8 @@ jobs:
           # Check if size exceeds 10GB
           if [ "$DIR_SIZE" -gt "10737418240" ]; then
             echo "Cache size exceeds threshold, running lake exe cache clean"
-            # We use the master-branch version of `cache`.
-            cd master-branch
+            # We use the tools-branch version of `cache`.
+            cd tools-branch
             lake exe cache clean
           fi
 
@@ -281,15 +289,15 @@ jobs:
 
       - name: get cache (1/3 - setup and initial fetch)
         id: get_cache_part1_setup
-        shell: bash # only runs `cache get` from `master-branch`, so doesn't need to be inside landrun
+        shell: bash # only runs `cache get` from `tools-branch`, so doesn't need to be inside landrun
         run: |
           cd pr-branch
           echo "Removing old Mathlib build directories prior to cache fetch..."
           rm -rf .lake/build/lib/lean/Mathlib
 
           # Fail quickly if the cache is completely cold, by checking for Mathlib.Init
           echo "Attempting to fetch olean for Mathlib/Init.lean from cache..."
-          ../master-branch/.lake/build/bin/cache get Mathlib/Init.lean
+          ../tools-branch/.lake/build/bin/cache get Mathlib/Init.lean
 
       - name: get cache (2/3 - test Mathlib.Init cache)
         id: get_cache_part2_test
@@ -303,16 +311,16 @@ jobs:
 
       - name: get cache (3/3 - finalize cache operation)
         id: get
-        shell: bash # only runs `cache get` from `master-branch`, so doesn't need to be inside landrun
+        shell: bash # only runs `cache get` from `tools-branch`, so doesn't need to be inside landrun
         run: |
           cd pr-branch
           if [[ "${{ steps.get_cache_part2_test.outcome }}" == "success" ]]; then
             echo "Fetching all remaining cache..."
 
-            ../master-branch/.lake/build/bin/cache get
+            ../tools-branch/.lake/build/bin/cache get
 
             # Run again with --repo, to ensure we actually get the oleans.
-            ../master-branch/.lake/build/bin/cache --repo=${{ github.event.pull_request.head.repo.full_name || github.repository }} get
+            ../tools-branch/.lake/build/bin/cache --repo=${{ github.event.pull_request.head.repo.full_name || github.repository }} get
           else
             echo "WARNING: 'lake build --no-build -v Mathlib.Init' failed."
             echo "No cache for 'Mathlib.Init' available or it could not be prepared."
@@ -346,7 +354,7 @@ jobs:
           fi
           echo "::endgroup::"
 
-          ../master-branch/scripts/lake-build-with-retry.sh Mathlib
+          ../tools-branch/scripts/lake-build-with-retry.sh Mathlib
           # results of build at pr-branch/.lake/build_summary_Mathlib.json
       - name: end gh-problem-match-wrap for build step
         uses: leanprover-community/gh-problem-matcher-wrap@20007cb926a46aa324653a387363b52f07709845 # 2025-04-23
@@ -372,15 +380,15 @@ jobs:
           # Trim trailing whitespace from secrets to prevent issues with accidentally added spaces
           export MATHLIB_CACHE_SAS="${MATHLIB_CACHE_SAS_RAW%"${MATHLIB_CACHE_SAS_RAW##*[![:space:]]}"}"
 
-          # Use the trusted cache tool from master-branch
+          # Use the trusted cache tool from tools-branch
           # TODO: this is not doing anything currently, and needs to be integrated with put-unpacked
-          # ../master-branch/.lake/build/bin/cache commit || true
+          # ../tools-branch/.lake/build/bin/cache commit || true
           # run this in CI if it gets an incorrect lake hash for existing cache files somehow
-          # ../master-branch/.lake/build/bin/cache put!
+          # ../tools-branch/.lake/build/bin/cache put!
           # do not try to upload files just downloaded
 
           echo "Uploading cache to Azure..."
-          MATHLIB_CACHE_USE_CLOUDFLARE=0 ../master-branch/.lake/build/bin/cache --repo=${{ github.event.pull_request.head.repo.full_name || github.repository }} put-unpacked
+          MATHLIB_CACHE_USE_CLOUDFLARE=0 ../tools-branch/.lake/build/bin/cache --repo=${{ github.event.pull_request.head.repo.full_name || github.repository }} put-unpacked
         env:
           MATHLIB_CACHE_SAS_RAW: ${{ secrets.MATHLIB_CACHE_SAS }}
 
@@ -396,23 +404,23 @@ jobs:
         shell: bash
         run: |
           cd pr-branch
-          ../master-branch/.lake/build/bin/cache get Archive.lean
-          ../master-branch/.lake/build/bin/cache get Counterexamples.lean
+          ../tools-branch/.lake/build/bin/cache get Archive.lean
+          ../tools-branch/.lake/build/bin/cache get Counterexamples.lean
 
       - name: build archive
         id: archive
         continue-on-error: true
         run: |
           cd pr-branch
-          ../master-branch/scripts/lake-build-with-retry.sh Archive
+          ../tools-branch/scripts/lake-build-with-retry.sh Archive
           # results of build at pr-branch/.lake/build_summary_Archive.json
 
       - name: build counterexamples
         id: counterexamples
         continue-on-error: true
         run: |
           cd pr-branch
-          ../master-branch/scripts/lake-build-with-retry.sh Counterexamples
+          ../tools-branch/scripts/lake-build-with-retry.sh Counterexamples
           # results of build at pr-branch/.lake/build_summary_Counterexamples.json
 
       - name: Check if building Archive or Counterexamples failed
@@ -436,8 +444,8 @@ jobs:
           export MATHLIB_CACHE_SAS="${MATHLIB_CACHE_SAS_RAW%"${MATHLIB_CACHE_SAS_RAW##*[![:space:]]}"}"
 
           echo "Uploading Archive and Counterexamples cache to Azure..."
-          MATHLIB_CACHE_USE_CLOUDFLARE=0 ../master-branch/.lake/build/bin/cache --repo=${{ github.event.pull_request.head.repo.full_name || github.repository }} put-unpacked Archive.lean
-          MATHLIB_CACHE_USE_CLOUDFLARE=0 ../master-branch/.lake/build/bin/cache --repo=${{ github.event.pull_request.head.repo.full_name || github.repository }} put-unpacked Counterexamples.lean
+          MATHLIB_CACHE_USE_CLOUDFLARE=0 ../tools-branch/.lake/build/bin/cache --repo=${{ github.event.pull_request.head.repo.full_name || github.repository }} put-unpacked Archive.lean
+          MATHLIB_CACHE_USE_CLOUDFLARE=0 ../tools-branch/.lake/build/bin/cache --repo=${{ github.event.pull_request.head.repo.full_name || github.repository }} put-unpacked Counterexamples.lean
         env:
           MATHLIB_CACHE_SAS_RAW: ${{ secrets.MATHLIB_CACHE_SAS }}
 
@@ -460,7 +468,7 @@ jobs:
         id: test
         run: |
           cd pr-branch
-          ../master-branch/scripts/lake-build-wrapper.py .lake/build_summary_MathlibTest.json lake --iofail test
+          ../tools-branch/scripts/lake-build-wrapper.py .lake/build_summary_MathlibTest.json lake --iofail test
       - name: end gh-problem-match-wrap for test step
         uses: leanprover-community/gh-problem-matcher-wrap@20007cb926a46aa324653a387363b52f07709845 # 2025-04-23
         with:
@@ -584,8 +592,8 @@ jobs:
           TEST_OUTCOME: ${{ steps.test.outcome }}
           NIGHTLY_TESTING_REPO: leanprover-community/mathlib4-nightly-testing
         run: |
-          master-branch/scripts/lean-pr-testing-comments.sh lean
-          master-branch/scripts/lean-pr-testing-comments.sh batteries
+          tools-branch/scripts/lean-pr-testing-comments.sh lean
+          tools-branch/scripts/lean-pr-testing-comments.sh batteries
 
   post_steps:
     name: Post-Build Step
@@ -678,6 +686,7 @@ jobs:
 
   final:
     name: Post-CI job
+    if: ${{ inputs.run_post_ci }}
     needs: [style_lint, build, post_steps]
     runs-on: ubuntu-latest
     steps:
@@ -774,7 +783,10 @@ jobs:
           echo "username=$USERNAME" >> "$GITHUB_OUTPUT"
           echo "Found label actor: $USERNAME"
 
-      - if: contains(steps.PR.outputs.pr_labels, 'auto-merge-after-CI')
+      - if: >- # bot usernames will cause this step to error with "Could not resolve to a User..."
+          contains(steps.PR.outputs.pr_labels, 'auto-merge-after-CI') &&
+          steps.get-label-actor.outputs.username != 'mathlib-nolints' &&
+          steps.get-label-actor.outputs.username != 'mathlib-update-dependencies'
         name: check team membership
         uses: tspascoal/get-user-teams-membership@57e9f42acd78f4d0f496b3be4368fc5f62696662 # v3.0.0
         id: actorTeams
@@ -784,11 +796,18 @@ jobs:
           username: ${{ steps.get-label-actor.outputs.username }}
           GITHUB_TOKEN: ${{ secrets.MATHLIB_REVIEWERS_TEAM_KEY }} # (Requires scope: `read:org`)
 
-      # The create-github-app-token README states that this token is masked and will not be logged accidentally.
-      - if: ${{ contains(steps.PR.outputs.pr_labels, 'auto-merge-after-CI') && (contains(steps.actorTeams.outputs.teams, 'mathlib-maintainers') || contains(steps.actorTeams.outputs.teams, 'bot-users')) }}
+      - if: >-
+          contains(steps.PR.outputs.pr_labels, 'auto-merge-after-CI') &&
+          (
+            steps.get-label-actor.outputs.username == 'mathlib-nolints' ||
+            steps.get-label-actor.outputs.username == 'mathlib-update-dependencies' ||
+            contains(steps.actorTeams.outputs.teams, 'mathlib-maintainers') ||
+            contains(steps.actorTeams.outputs.teams, 'bot-users')
+          )
         name: If `auto-merge-after-CI` is present, add a `bors merge` comment.
         uses: GrantBirki/comment@608e41b19bc973020ec0e189ebfdae935d7fe0cc # v2.1.1
         with:
+          # The create-github-app-token README states that this token is masked and will not be logged accidentally.
           token: ${{ steps.auto-merge-app-token.outputs.token }}
           issue-number: ${{ steps.PR.outputs.number }}
           body: |

.github/workflows/ci_dev.yml

@@ -0,0 +1,42 @@
+name: ci dev
+
+on:
+  workflow_dispatch:
+    inputs:
+      tools_branch_ref:
+        description: ref for tools checkout (defaults to 'this commit')
+        required: false
+        type: string
+        default: ''
+      pr_branch_ref:
+        description: ref for building-branch checkout (defaults to 'this commit')
+        required: false
+        type: string
+        default: ''
+      run_post_ci:
+        description: Run the post-CI job?
+        required: false
+        type: boolean
+        default: false # We shouldn't need this job in typical experiments
+
+# Limit permissions for GITHUB_TOKEN for the entire workflow
+permissions:
+  contents: read
+  # By default let's remove this permission (which is present in the other build pipelines)
+  # from the CI experimentation runs to avoid unwitting side effects
+  # pull-requests: write
+
+jobs:
+  build:
+    name: ci (dev branch)
+    # For sanity and intentionality, let's only trigger this from branches ci-dev/*
+    if: ${{ github.repository == 'leanprover-community/mathlib4' && github.ref_type == 'branch' && startsWith(github.ref_name, 'ci-dev/') }}
+    uses: ./.github/workflows/build_template.yml
+    with:
+      concurrency_group: ${{ github.workflow }}-${{ github.ref }}
+      # Use the tools from 'this branch', as our changes in the tools might be relevant for experiments
+      tools_branch_ref: ${{ inputs.tools_branch_ref != '' && inputs.tools_branch_ref || github.sha }}
+      pr_branch_ref: ${{ inputs.pr_branch_ref != '' && inputs.pr_branch_ref || github.sha }}
+      run_post_ci: ${{ inputs.run_post_ci }}
+      runs_on: pr
+    secrets: inherit