Merge branch 'master' into nerve2

leanprover-community · Sep 15, 2024 · 18f0836 · 18f0836
2 parents 6092636 + 13018a2
commit 18f0836
Show file tree

Hide file tree

Showing 1,047 changed files with 20,489 additions and 9,680 deletions.
diff --git a/.github/build.in.yml b/.github/build.in.yml
@@ -130,9 +130,6 @@ jobs:
           lean --version
           lake --version
 
-      - name: check {Mathlib, Tactic, Counterexamples, Archive}.lean are up to date
-        run: lake exe mk_all --check
-
       - name: build cache
         run: |
           lake build cache
@@ -160,7 +157,7 @@ jobs:
         with:
           linters: gcc
           run: |
-            bash -o pipefail -c "env LEAN_ABORT_ON_PANIC=1 lake build --wfail -KCI"
+            bash -o pipefail -c "lake exe mk_all || echo "There are unaccounted for files, but I am not failing yet!"; env LEAN_ABORT_ON_PANIC=1 lake build --wfail -KCI"
 
       - name: upload cache
         # We only upload the cache if the build started (whether succeeding, failing, or cancelled)
@@ -216,6 +213,9 @@ jobs:
           MATHLIB_CACHE_SAS: ${{ secrets.MATHLIB_CACHE_SAS }}
           MATHLIB_CACHE_S3_TOKEN: ${{ secrets.MATHLIB_CACHE_S3_TOKEN }}
 
+      - name: update {Mathlib, Tactic, Counterexamples, Archive}.lean
+        run: lake exe mk_all --check
+
       - name: check for noisy stdout lines
         id: noisy
         run: |

diff --git a/.github/workflows/add_label_from_comment.yml b/.github/workflows/add_label_from_comment.yml
@@ -7,50 +7,15 @@ on:
 jobs:
   add_ready_to_merge_label:
     name: Add ready-to-merge label
-    if: (toJSON(github.event.issue.pull_request) != 'null') && (startsWith(github.event.comment.body, 'bors r+') || contains(toJSON(github.event.comment.body), '\r\nbors r+') || startsWith(github.event.comment.body, 'bors merge') || contains(toJSON(github.event.comment.body), '\r\nbors merge'))
+    if: github.event.issue.pull_request && (startsWith(github.event.comment.body, 'bors r+') || contains(toJSON(github.event.comment.body), '\nbors r+') || startsWith(github.event.comment.body, 'bors merge') || contains(toJSON(github.event.comment.body), '\nbors merge'))
     runs-on: ubuntu-latest
     steps:
-      - uses: octokit/[email protected]
-        name: Get PR head
-        id: get_pr_head
+      - id: user_permission
+        uses: actions-cool/check-user-permission@v2
         with:
-          route: GET /repos/:repository/pulls/:pull_number
-          repository: ${{ github.repository }}
-          pull_number: ${{ github.event.issue.number }}
-        env:
-          GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }}
-
-      # Parse steps.get_pr_head.outputs.data, since it is a string
-      - id: parse_pr_head
-        name: Parse PR head
-        uses: gr2m/[email protected]
-        with:
-          json: ${{ steps.get_pr_head.outputs.data }}
-          head_user: 'head.user.login'
-
-      # we skip the rest if this PR is from a fork,
-      # since the GITHUB_TOKEN doesn't have write perms
-      - if: steps.parse_pr_head.outputs.head_user == 'leanprover-community'
-        uses: octokit/[email protected]
-        name: Get comment author
-        id: get_user
-        with:
-          route: GET /repos/:repository/collaborators/:username/permission
-          repository: ${{ github.repository }}
-          username: ${{ github.event.comment.user.login }}
-        env:
-          GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }}
-
-      # Parse steps.get_user.outputs.data, since it is a string
-      - if: steps.parse_pr_head.outputs.head_user == 'leanprover-community'
-        id: parse_user
-        name: Parse comment author permission
-        uses: gr2m/[email protected]
-        with:
-          json: ${{ steps.get_user.outputs.data }}
-          permission: 'permission'
+          require: 'admin'
 
-      - if: (steps.parse_pr_head.outputs.head_user == 'leanprover-community') && (steps.parse_user.outputs.permission == 'admin')
+      - if: (steps.user_permission.outputs.require-result == 'true') || (github.event.comment.user.login == 'leanprover-community-mathlib4-bot') || (github.event.comment.user.login == 'leanprover-community-bot-assistant')
         uses: octokit/[email protected]
         id: add_label
         name: Add label
@@ -62,7 +27,7 @@ jobs:
         env:
           GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }}
 
-      - if: (steps.parse_pr_head.outputs.head_user == 'leanprover-community') && (steps.parse_user.outputs.permission == 'admin')
+      - if: (steps.user_permission.outputs.require-result == 'true') || (github.event.comment.user.login == 'leanprover-community-mathlib4-bot') || (github.event.comment.user.login == 'leanprover-community-bot-assistant')
         id: remove_labels
         name: Remove "awaiting-author"
         # we use curl rather than octokit/request-action so that the job won't fail
@@ -74,50 +39,15 @@ jobs:
 
   add_delegated_label:
     name: Add delegated label
-    if: (toJSON(github.event.issue.pull_request) != 'null') && (startsWith(github.event.comment.body, 'bors d') || contains(toJSON(github.event.comment.body), '\r\nbors d'))
+    if: github.event.issue.pull_request && (startsWith(github.event.comment.body, 'bors d') || contains(toJSON(github.event.comment.body), '\nbors d'))
     runs-on: ubuntu-latest
     steps:
-      - uses: octokit/[email protected]
-        name: Get PR head
-        id: get_pr_head
-        with:
-          route: GET /repos/:repository/pulls/:pull_number
-          repository: ${{ github.repository }}
-          pull_number: ${{ github.event.issue.number }}
-        env:
-          GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }}
-
-      # Parse steps.get_pr_head.outputs.data, since it is a string
-      - id: parse_pr_head
-        name: Parse PR head
-        uses: gr2m/[email protected]
-        with:
-          json: ${{ steps.get_pr_head.outputs.data }}
-          head_user: 'head.user.login'
-
-      # we skip the rest if this PR is from a fork,
-      # since the GITHUB_TOKEN doesn't have write perms
-      - if: steps.parse_pr_head.outputs.head_user == 'leanprover-community'
-        uses: octokit/[email protected]
-        name: Get comment author
-        id: get_user
-        with:
-          route: GET /repos/:repository/collaborators/:username/permission
-          repository: ${{ github.repository }}
-          username: ${{ github.event.comment.user.login }}
-        env:
-          GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }}
-
-      # Parse steps.get_user.outputs.data, since it is a string
-      - if: steps.parse_pr_head.outputs.head_user == 'leanprover-community'
-        id: parse_user
-        name: Parse comment author permission
-        uses: gr2m/[email protected]
+      - id: user_permission
+        uses: actions-cool/check-user-permission@v2
         with:
-          json: ${{ steps.get_user.outputs.data }}
-          permission: 'permission'
+          require: 'admin'
 
-      - if: (steps.parse_pr_head.outputs.head_user == 'leanprover-community') && (steps.parse_user.outputs.permission == 'admin')
+      - if: (steps.user_permission.outputs.require-result == 'true') || (github.event.comment.user.login == 'leanprover-community-mathlib4-bot') || (github.event.comment.user.login == 'leanprover-community-bot-assistant')
         uses: octokit/[email protected]
         id: add_label
         name: Add label

diff --git a/.github/workflows/add_label_from_review.yml b/.github/workflows/add_label_from_review.yml
@@ -7,50 +7,16 @@ on:
 jobs:
   add_ready_to_merge_label:
     name: Add ready-to-merge label
-    if: (startsWith(github.event.review.body, 'bors r+') || contains(toJSON(github.event.review.body), '\r\nbors r+') || startsWith(github.event.review.body, 'bors merge') || contains(toJSON(github.event.review.body), '\r\nbors merge'))
+    if: (startsWith(github.event.review.body, 'bors r+') || contains(toJSON(github.event.review.body), '\nbors r+') || startsWith(github.event.review.body, 'bors merge') || contains(toJSON(github.event.review.body), '\nbors merge'))
     runs-on: ubuntu-latest
     steps:
-      - uses: octokit/[email protected]
-        name: Get PR head
-        id: get_pr_head
+      - id: user_permission
+        uses: actions-cool/check-user-permission@v2
         with:
-          route: GET /repos/:repository/pulls/:pull_number
-          repository: ${{ github.repository }}
-          pull_number: ${{ github.event.pull_request.number }}
-        env:
-          GITHUB_TOKEN: ${{ secrets.TRIAGE_TOKEN }}
-
-      # Parse steps.get_pr_head.outputs.data, since it is a string
-      - id: parse_pr_head
-        name: Parse PR head
-        uses: gr2m/[email protected]
-        with:
-          json: ${{ steps.get_pr_head.outputs.data }}
-          head_user: 'head.user.login'
-
-      # we skip the rest if this PR is from a fork,
-      # since the GITHUB_TOKEN doesn't have write perms
-      - if: steps.parse_pr_head.outputs.head_user == 'leanprover-community'
-        uses: octokit/[email protected]
-        name: Get comment author
-        id: get_user
-        with:
-          route: GET /repos/:repository/collaborators/:username/permission
-          repository: ${{ github.repository }}
-          username: ${{ github.event.review.user.login }}
-        env:
-          GITHUB_TOKEN: ${{ secrets.TRIAGE_TOKEN }}
-
-      # Parse steps.get_user.outputs.data, since it is a string
-      - if: steps.parse_pr_head.outputs.head_user == 'leanprover-community'
-        id: parse_user
-        name: Parse comment author permission
-        uses: gr2m/[email protected]
-        with:
-          json: ${{ steps.get_user.outputs.data }}
-          permission: 'permission'
+          require: 'write'
+          token: ${{ secrets.TRIAGE_TOKEN }}
 
-      - if: (steps.parse_pr_head.outputs.head_user == 'leanprover-community') && (steps.parse_user.outputs.permission == 'admin')
+      - if: (steps.user_permission.outputs.require-result == 'true') || (github.event.review.user.login == 'leanprover-community-mathlib4-bot') || (github.event.review.user.login == 'leanprover-community-bot-assistant')
         uses: octokit/[email protected]
         id: add_label
         name: Add label
@@ -62,7 +28,7 @@ jobs:
         env:
           GITHUB_TOKEN: ${{ secrets.TRIAGE_TOKEN }}
 
-      - if: (steps.parse_pr_head.outputs.head_user == 'leanprover-community') && (steps.parse_user.outputs.permission == 'admin')
+      - if: (steps.user_permission.outputs.require-result == 'true') || (github.event.review.user.login == 'leanprover-community-mathlib4-bot') || (github.event.review.user.login == 'leanprover-community-bot-assistant')
         id: remove_labels
         name: Remove "awaiting-author"
         # we use curl rather than octokit/request-action so that the job won't fail
@@ -74,50 +40,16 @@ jobs:
 
   add_delegated_label:
     name: Add delegated label
-    if: (startsWith(github.event.review.body, 'bors d') || contains(toJSON(github.event.review.body), '\r\nbors d'))
+    if: (startsWith(github.event.review.body, 'bors d') || contains(toJSON(github.event.review.body), '\nbors d'))
     runs-on: ubuntu-latest
     steps:
-      - uses: octokit/[email protected]
-        name: Get PR head
-        id: get_pr_head
-        with:
-          route: GET /repos/:repository/pulls/:pull_number
-          repository: ${{ github.repository }}
-          pull_number: ${{ github.event.pull_request.number }}
-        env:
-          GITHUB_TOKEN: ${{ secrets.TRIAGE_TOKEN }}
-
-      # Parse steps.get_pr_head.outputs.data, since it is a string
-      - id: parse_pr_head
-        name: Parse PR head
-        uses: gr2m/[email protected]
-        with:
-          json: ${{ steps.get_pr_head.outputs.data }}
-          head_user: 'head.user.login'
-
-      # we skip the rest if this PR is from a fork,
-      # since the GITHUB_TOKEN doesn't have write perms
-      - if: steps.parse_pr_head.outputs.head_user == 'leanprover-community'
-        uses: octokit/[email protected]
-        name: Get comment author
-        id: get_user
-        with:
-          route: GET /repos/:repository/collaborators/:username/permission
-          repository: ${{ github.repository }}
-          username: ${{ github.event.review.user.login }}
-        env:
-          GITHUB_TOKEN: ${{ secrets.TRIAGE_TOKEN }}
-
-      # Parse steps.get_user.outputs.data, since it is a string
-      - if: steps.parse_pr_head.outputs.head_user == 'leanprover-community'
-        id: parse_user
-        name: Parse comment author permission
-        uses: gr2m/[email protected]
+      - id: user_permission
+        uses: actions-cool/check-user-permission@v2
         with:
-          json: ${{ steps.get_user.outputs.data }}
-          permission: 'permission'
+          require: 'write'
+          token: ${{ secrets.TRIAGE_TOKEN }}
 
-      - if: (steps.parse_pr_head.outputs.head_user == 'leanprover-community') && (steps.parse_user.outputs.permission == 'admin')
+      - if: (steps.user_permission.outputs.require-result == 'true') || (github.event.review.user.login == 'leanprover-community-mathlib4-bot') || (github.event.review.user.login == 'leanprover-community-bot-assistant')
         uses: octokit/[email protected]
         id: add_label
         name: Add label

diff --git a/.github/workflows/add_label_from_review_comment.yml b/.github/workflows/add_label_from_review_comment.yml
@@ -0,0 +1,62 @@
+name: Add "ready-to-merge" and "delegated" label from PR review comment
+
+on:
+  pull_request_review_comment:
+    types: [created]
+
+jobs:
+  add_ready_to_merge_label:
+    name: Add ready-to-merge label
+    if: (startsWith(github.event.comment.body, 'bors r+') || contains(toJSON(github.event.comment.body), '\nbors r+') || startsWith(github.event.comment.body, 'bors merge') || contains(toJSON(github.event.comment.body), '\nbors merge'))
+    runs-on: ubuntu-latest
+    steps:
+      - id: user_permission
+        uses: actions-cool/check-user-permission@v2
+        with:
+          require: 'write'
+          token: ${{ secrets.TRIAGE_TOKEN }}
+
+      - if: (steps.user_permission.outputs.require-result == 'true') || (github.event.comment.user.login == 'leanprover-community-mathlib4-bot') || (github.event.comment.user.login == 'leanprover-community-bot-assistant')
+        uses: octokit/[email protected]
+        id: add_label
+        name: Add label
+        with:
+          route: POST /repos/:repository/issues/:issue_number/labels
+          repository: ${{ github.repository }}
+          issue_number: ${{ github.event.pull_request.number }}
+          labels: '["ready-to-merge"]'
+        env:
+          GITHUB_TOKEN: ${{ secrets.TRIAGE_TOKEN }}
+
+      - if: (steps.user_permission.outputs.require-result == 'true') || (github.event.comment.user.login == 'leanprover-community-mathlib4-bot') || (github.event.comment.user.login == 'leanprover-community-bot-assistant')
+        id: remove_labels
+        name: Remove "awaiting-author"
+        # 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
+        run: |
+          curl --request DELETE \
+            --url https://api.github.com/repos/${{ github.repository }}/issues/${{ github.event.pull_request.number }}/labels/awaiting-author \
+            --header 'authorization: Bearer ${{ secrets.TRIAGE_TOKEN }}'
+
+  add_delegated_label:
+    name: Add delegated label
+    if: (startsWith(github.event.comment.body, 'bors d') || contains(toJSON(github.event.comment.body), '\nbors d'))
+    runs-on: ubuntu-latest
+    steps:
+      - id: user_permission
+        uses: actions-cool/check-user-permission@v2
+        with:
+          require: 'write'
+          token: ${{ secrets.TRIAGE_TOKEN }}
+
+      - if: (steps.user_permission.outputs.require-result == 'true') || (github.event.comment.user.login == 'leanprover-community-mathlib4-bot') || (github.event.comment.user.login == 'leanprover-community-bot-assistant')
+        uses: octokit/[email protected]
+        id: add_label
+        name: Add label
+        with:
+          route: POST /repos/:repository/issues/:issue_number/labels
+          repository: ${{ github.repository }}
+          issue_number: ${{ github.event.pull_request.number }}
+          labels: '["delegated"]'
+        env:
+          GITHUB_TOKEN: ${{ secrets.TRIAGE_TOKEN }}
diff --git a/.github/workflows/bors.yml b/.github/workflows/bors.yml
@@ -143,9 +143,6 @@ jobs:
           lean --version
           lake --version
 
-      - name: check {Mathlib, Tactic, Counterexamples, Archive}.lean are up to date
-        run: lake exe mk_all --check
-
       - name: build cache
         run: |
           lake build cache
@@ -173,7 +170,7 @@ jobs:
         with:
           linters: gcc
           run: |
-            bash -o pipefail -c "env LEAN_ABORT_ON_PANIC=1 lake build --wfail -KCI"
+            bash -o pipefail -c "lake exe mk_all || echo "There are unaccounted for files, but I am not failing yet!"; env LEAN_ABORT_ON_PANIC=1 lake build --wfail -KCI"
 
       - name: upload cache
         # We only upload the cache if the build started (whether succeeding, failing, or cancelled)
@@ -229,6 +226,9 @@ jobs:
           MATHLIB_CACHE_SAS: ${{ secrets.MATHLIB_CACHE_SAS }}
           MATHLIB_CACHE_S3_TOKEN: ${{ secrets.MATHLIB_CACHE_S3_TOKEN }}
 
+      - name: update {Mathlib, Tactic, Counterexamples, Archive}.lean
+        run: lake exe mk_all --check
+
       - name: check for noisy stdout lines
         id: noisy
         run: |

diff --git a/.github/workflows/build.yml b/.github/workflows/build.yml
@@ -150,9 +150,6 @@ jobs:
           lean --version
           lake --version
 
-      - name: check {Mathlib, Tactic, Counterexamples, Archive}.lean are up to date
-        run: lake exe mk_all --check
-
       - name: build cache
         run: |
           lake build cache
@@ -180,7 +177,7 @@ jobs:
         with:
           linters: gcc
           run: |
-            bash -o pipefail -c "env LEAN_ABORT_ON_PANIC=1 lake build --wfail -KCI"
+            bash -o pipefail -c "lake exe mk_all || echo "There are unaccounted for files, but I am not failing yet!"; env LEAN_ABORT_ON_PANIC=1 lake build --wfail -KCI"
 
       - name: upload cache
         # We only upload the cache if the build started (whether succeeding, failing, or cancelled)
@@ -236,6 +233,9 @@ jobs:
           MATHLIB_CACHE_SAS: ${{ secrets.MATHLIB_CACHE_SAS }}
           MATHLIB_CACHE_S3_TOKEN: ${{ secrets.MATHLIB_CACHE_S3_TOKEN }}
 
+      - name: update {Mathlib, Tactic, Counterexamples, Archive}.lean
+        run: lake exe mk_all --check
+
       - name: check for noisy stdout lines
         id: noisy
         run: |