Merge branch 'master' into Frullani_integral

Author: Deep0Thinking

.github/workflows/bors.yml

@@ -4,6 +4,7 @@ on:
   push:
     branches:
       - staging
+      - trying
 
 concurrency:
   # label each workflow run; only the latest with each label will run
@@ -25,5 +26,6 @@ jobs:
       concurrency_group: ${{ github.workflow }}-${{ github.ref }}-${{ github.run_id }}
       pr_branch_ref: ${{ github.sha }}
       job_name_suffix: ""
-      runs_on: bors
+      # 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

@@ -7,8 +7,9 @@ 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'
   merge_group:
 
 concurrency:

.github/workflows/build_fork.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

.github/workflows/build_template.yml

@@ -692,6 +692,13 @@ jobs:
     needs: [style_lint, build, post_steps]
     runs-on: ubuntu-latest
     steps:
+      - name: Generate auto merge app token
+        id: auto-merge-app-token
+        uses: actions/create-github-app-token@29824e69f54612133e76f7eaac726eef6c875baf # v2.2.1
+        with:
+          app-id: ${{ secrets.MATHLIB_AUTO_MERGE_APP_ID }}
+          private-key: ${{ secrets.MATHLIB_AUTO_MERGE_PRIVATE_KEY }}
+
       - id: PR_from_push
         uses: 8BitJonny/gh-get-current-pr@4056877062a1f3b624d5d4c2bedefa9cf51435c9 # 4.0.0
         # TODO: this may not work properly if the same commit is pushed to multiple branches:
@@ -788,11 +795,12 @@ 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')) }}
         name: If `auto-merge-after-CI` is present, add a `bors merge` comment.
         uses: GrantBirki/comment@608e41b19bc973020ec0e189ebfdae935d7fe0cc # v2.1.1
         with:
-          token: ${{ secrets.AUTO_MERGE_TOKEN }}
+          token: ${{ steps.auto-merge-app-token.outputs.token }}
           issue-number: ${{ steps.PR.outputs.number }}
           body: |
             As this PR is labelled `auto-merge-after-CI`, we are now sending it to bors:

.github/workflows/maintainer_bors.yml

@@ -23,10 +23,19 @@ jobs:
       COMMENT_REVIEW: ${{ github.event.review.body }}
       PR_NUMBER: ${{ github.event.issue.number }}${{ github.event.pull_request.number }}
       HAS_DELEGATED_LABEL: ${{ contains(github.event.issue.labels.*.name, 'delegated') }}
+      HAS_TRIAGE_SECRET: ${{ secrets.MATHLIB_TRIAGE_APP_ID != '' }}
     name: Add ready-to-merge or delegated label
     runs-on: ubuntu-latest
     if: github.repository == 'leanprover-community/mathlib4'
     steps:
+      - name: Generate app token
+        if: ${{ env.HAS_TRIAGE_SECRET == 'true' }}
+        id: app-token
+        uses: actions/create-github-app-token@29824e69f54612133e76f7eaac726eef6c875baf # v2.2.1
+        with:
+          app-id: ${{ secrets.MATHLIB_TRIAGE_APP_ID }}
+          private-key: ${{ secrets.MATHLIB_TRIAGE_PRIVATE_KEY }}
+
       - name: Find bors merge/delegate
         id: merge_or_delegate
         run: |
@@ -58,7 +67,8 @@ jobs:
           printf $'removeLabels=%s\n' "${remove_labels}" >> "${GITHUB_OUTPUT}"
           if [ "${AUTHOR}" == 'leanprover-community-mathlib4-bot' ] ||
              [ "${AUTHOR}" == 'leanprover-community-bot-assistant' ] ||
-             [ "${AUTHOR}" == 'mathlib-bors[bot]' ]
+             [ "${AUTHOR}" == 'mathlib-bors[bot]' ] ||
+             [ "${AUTHOR}" == 'mathlib-triage[bot]' ]
           then
             printf $'bot=true\n'
             printf $'bot=true\n' >> "${GITHUB_OUTPUT}"
@@ -70,7 +80,7 @@ jobs:
           fi
 
           # write an artifact with all data needed below if we don't have access to necessary secrets
-          if [[ -z '${{ secrets.TRIAGE_TOKEN }}' ]]
+          if [[ -z '${{ secrets.MATHLIB_TRIAGE_APP_ID }}' ]]
           then
             printf 'No access to secrets, writing to file.\n'
             jq -n \
@@ -131,7 +141,8 @@ jobs:
           issue_number: ${{ github.event.issue.number }}${{ github.event.pull_request.number }}
           labels: '["${{ steps.merge_or_delegate.outputs.mOrD }}"]'
         env:
-          GITHUB_TOKEN: ${{ secrets.TRIAGE_TOKEN }}
+          # The create-github-app-token README states that this token is masked and will not be logged accidentally.
+          GITHUB_TOKEN: ${{ steps.app-token.outputs.token }}
 
       - if: ${{ ! steps.merge_or_delegate.outputs.secrets == '' &&
           (! steps.merge_or_delegate.outputs.mOrD == '' &&
@@ -145,7 +156,7 @@ jobs:
           for label in awaiting-author maintainer-merge; do
             curl --request DELETE \
               --url "https://api.github.com/repos/${{ github.repository }}/issues/${{ github.event.issue.number }}${{ github.event.pull_request.number }}/labels/${label}" \
-              --header 'authorization: Bearer ${{ secrets.TRIAGE_TOKEN }}'
+              --header 'authorization: Bearer ${{ steps.app-token.outputs.token }}'
           done
 
       - name: On bors r/d-, remove ready-to-merge or delegated label
@@ -158,7 +169,7 @@ jobs:
           for label in ready-to-merge delegated; do
             curl --request DELETE \
               --url "https://api.github.com/repos/${{ github.repository }}/issues/${{ github.event.issue.number }}${{ github.event.pull_request.number }}/labels/${label}" \
-              --header 'authorization: Bearer ${{ secrets.TRIAGE_TOKEN }}'
+              --header 'authorization: Bearer ${{ steps.app-token.outputs.token }}'
           done
 
       - name: Set up Python

.github/workflows/maintainer_bors_wf_run.yml

@@ -13,6 +13,13 @@ jobs:
     runs-on: ubuntu-latest
     if: ${{ github.repository == 'leanprover-community/mathlib4' && github.event.workflow_run.conclusion == 'success' }}
     steps:
+      - name: Generate app token
+        id: app-token
+        uses: actions/create-github-app-token@29824e69f54612133e76f7eaac726eef6c875baf # v2.2.1
+        with:
+          app-id: ${{ secrets.MATHLIB_TRIAGE_APP_ID }}
+          private-key: ${{ secrets.MATHLIB_TRIAGE_PRIVATE_KEY }}
+
       - name: Download artifact
         id: download-artifact
         uses: dawidd6/action-download-artifact@5c98f0b039f36ef966fdb7dfa9779262785ecb05 # v14
@@ -80,7 +87,8 @@ jobs:
           issue_number: ${{ steps.extract-data.outputs.pr_number }}
           labels: '["${{ steps.extract-data.outputs.mOrD }}"]'
         env:
-          GITHUB_TOKEN: ${{ secrets.TRIAGE_TOKEN }}
+          # The create-github-app-token README states that this token is masked and will not be logged accidentally.
+          GITHUB_TOKEN: ${{ steps.app-token.outputs.token }}
 
       - if: ${{ ! steps.extract-data.outputs.mOrD == '' &&
           ( steps.user_permission.outputs.require-result == 'true' ||
@@ -93,7 +101,7 @@ jobs:
           for label in awaiting-author maintainer-merge; do
             curl --request DELETE \
               --url "https://api.github.com/repos/${{ github.repository }}/issues/${{ steps.extract-data.outputs.pr_number }}/labels/${label}" \
-              --header 'authorization: Bearer ${{ secrets.TRIAGE_TOKEN }}'
+              --header 'authorization: Bearer ${{ steps.app-token.outputs.token }}'
           done
 
       - name: On bors r/d-, remove ready-to-merge or delegated label
@@ -104,7 +112,7 @@ jobs:
           for label in ready-to-merge delegated; do
             curl --request DELETE \
               --url "https://api.github.com/repos/${{ github.repository }}/issues/${{ steps.extract-data.outputs.pr_number }}/labels/${label}" \
-              --header 'authorization: Bearer ${{ secrets.TRIAGE_TOKEN }}'
+              --header 'authorization: Bearer ${{ steps.app-token.outputs.token }}'
           done
 
       - name: Set up Python

.github/workflows/maintainer_merge.yml

@@ -27,6 +27,7 @@ jobs:
       PR_TITLE_PR: ${{ github.event.pull_request.title }}
       PR_URL: ${{ github.event.issue.html_url }}${{ github.event.pull_request.html_url }}
       EVENT_NAME: ${{ github.event_name }}
+      HAS_TRIAGE_SECRET: ${{ secrets.MATHLIB_TRIAGE_APP_ID != '' }}
     name: Ping maintainers on Zulip
     runs-on: ubuntu-latest
     if: >- # crude check to skip running this on most reviews / comments
@@ -36,6 +37,14 @@ jobs:
         contains(format('{0}{1}', github.event.comment.body, github.event.review.body), 'maintainer delegate')
       )
     steps:
+      - name: Generate app token
+        if: ${{ env.HAS_TRIAGE_SECRET == 'true' }}
+        id: app-token
+        uses: actions/create-github-app-token@29824e69f54612133e76f7eaac726eef6c875baf # v2.2.1
+        with:
+          app-id: ${{ secrets.MATHLIB_TRIAGE_APP_ID }}
+          private-key: ${{ secrets.MATHLIB_TRIAGE_PRIVATE_KEY }}
+
       - name: Find maintainer merge/delegate
         id: merge_or_delegate
         run: |
@@ -58,7 +67,7 @@ jobs:
           printf $'mOrD=%s\n' "${m_or_d}" > "${GITHUB_OUTPUT}"
 
           # write an artifact with all data needed below if we don't have access to necessary secrets
-          if [[ -z '${{ secrets.MATHLIB_REVIEWERS_TEAM_KEY }}' ]]
+          if [[ -z '${{ secrets.MATHLIB_TRIAGE_APP_ID }}' ]]
           then
             printf 'No access to secrets, writing to file.\n'
             jq -n \
@@ -167,7 +176,8 @@ jobs:
         uses: actions/github-script@ed597411d8f924073f98dfc5c65a23a2325f34cd # v8.0.0
         with:
           # labels added by GITHUB_TOKEN won't trigger the Zulip emoji workflow
-          github-token: ${{secrets.TRIAGE_TOKEN}}
+          # The create-github-app-token README states that this token is masked and will not be logged accidentally.
+          github-token: ${{ steps.app-token.outputs.token }}
           script: |
             const { owner, repo, number: issue_number } = context.issue;
             await github.rest.issues.addLabels({ owner, repo, issue_number, labels: ['maintainer-merge'] });

.github/workflows/maintainer_merge_wf_run.yml

@@ -13,6 +13,13 @@ jobs:
     runs-on: ubuntu-latest
     if: ${{ github.repository == 'leanprover-community/mathlib4' && github.event.workflow_run.conclusion == 'success' }}
     steps:
+      - name: Generate app token
+        id: app-token
+        uses: actions/create-github-app-token@29824e69f54612133e76f7eaac726eef6c875baf # v2.2.1
+        with:
+          app-id: ${{ secrets.MATHLIB_TRIAGE_APP_ID }}
+          private-key: ${{ secrets.MATHLIB_TRIAGE_PRIVATE_KEY }}
+
       - name: Download artifact
         id: download-artifact
         uses: dawidd6/action-download-artifact@5c98f0b039f36ef966fdb7dfa9779262785ecb05 # v14
@@ -140,7 +147,8 @@ jobs:
         uses: actions/github-script@ed597411d8f924073f98dfc5c65a23a2325f34cd # v8.0.0
         with:
           # labels added by GITHUB_TOKEN won't trigger the Zulip emoji workflow
-          github-token: ${{secrets.TRIAGE_TOKEN}}
+          # The create-github-app-token README states that this token is masked and will not be logged accidentally.
+          github-token: ${{ steps.app-token.outputs.token }}
           script: |
             const { owner, repo } = context.repo;
             const issue_number = ${{ steps.extract-data.outputs.pr_number }};

.github/workflows/pre-commit.yml

@@ -8,8 +8,9 @@ on:
       - 'trying.tmp*'
       - 'staging*.tmp'
       - 'nolints'
-      # 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'
       - 'master'
   pull_request:
 

.github/workflows/update_dependencies.yml

@@ -12,11 +12,19 @@ jobs:
     env:
       BRANCH_NAME: "update-dependencies-bot-use-only"
     steps:
+      - name: Generate app token
+        id: app-token
+        uses: actions/create-github-app-token@29824e69f54612133e76f7eaac726eef6c875baf # v2.2.1
+        with:
+          app-id: ${{ secrets.MATHLIB_UPDATE_DEPENDENCIES_APP_ID }}
+          private-key: ${{ secrets.MATHLIB_UPDATE_DEPENDENCIES_PRIVATE_KEY }}
+
+      # The create-github-app-token README states that this token is masked and will not be logged accidentally.
       - name: Checkout repository
         uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2
         with:
           fetch-depth: 0
-          token: "${{ secrets.UPDATE_DEPENDENCIES_TOKEN }}"
+          token: ${{ steps.app-token.outputs.token }}
 
       - name: Configure Lean
         uses: leanprover/lean-action@c544e89643240c6b398f14a431bcdc6309e36b3e # v1.4.0
@@ -116,8 +124,7 @@ jobs:
         if: ${{ steps.pr-title.outcome == 'success' }}
         uses: peter-evans/create-pull-request@c0f553fe549906ede9cf27b5156039d195d2ece0 # v8.1.0
         with:
-          token: "${{ secrets.UPDATE_DEPENDENCIES_TOKEN }}"
-          author: "leanprover-community-mathlib4-bot <leanprover-community-mathlib4-bot@users.noreply.github.com>"
+          token: ${{ steps.app-token.outputs.token }}
           commit-message: "chore: update Mathlib dependencies ${{ env.timestamp }}"
           # this branch is referenced in update_dependencies_zulip.yml
           branch: ${{ env.BRANCH_NAME }}