Merge branch 'master' into rida/refactorDist

.devcontainer/devcontainer.json

@@ -7,6 +7,10 @@
 
   "onCreateCommand": "lake exe cache get!",
 
+  "hostRequirements": {
+     "cpus": 4
+  },
+
   "customizations": {
     "vscode" : {
       "extensions" : [ "leanprover.lean4" ]

.github/PULL_REQUEST_TEMPLATE.md

@@ -8,14 +8,25 @@ For details on the "pull request lifecycle" in mathlib, please see:
 https://leanprover-community.github.io/contribute/index.html
 
 In particular, note that most reviewers will only notice your PR
-if it passes the continuous integration checks, and is labeled with `awaiting-review`.
+if it passes the continuous integration checks.
 Please ask for help on https://leanprover.zulipchat.com if needed.
 
 To indicate co-authors, include lines at the bottom of the commit message
 (that is, before the `---`) using the following format:
 
 Co-authored-by: Author Name <[email protected]>
 
+If you are moving or deleting declarations, please include these lines at the bottom of the commit message
+(that is, before the `---`) using the following format:
+
+Moves:
+- Vector.* -> Mathlib.Vector.*
+- ...
+
+Deletions:
+- Nat.bit1_add_bit1
+- ...
+
 Any other comments you want to keep out of the PR commit should go
 below the `---`, and placed outside this HTML comment, or else they
 will be invisible to reviewers.
@@ -24,6 +35,7 @@ If this PR depends on other PRs, please list them below this comment,
 using the following format:
 - [ ] depends on: #abc [optional extra text]
 - [ ] depends on: #xyz [optional extra text]
+
 -->
 
 [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)

.github/workflows/PR_summary.yml

@@ -45,7 +45,7 @@ jobs:
         # Compute the counts for the merge base
         python ./scripts/count-trans-deps.py "Mathlib/" > base.json
 
-        # switch back to the current branch: the `no_lost_declarations` script should be here
+        # switch back to the current branch: the `declarations_diff` script should be here
         git checkout "${currentHash}"
     - name: Post or update the summary comment
       env:
@@ -69,7 +69,7 @@ jobs:
         fi
 
         ## Declarations' diff comment
-        declDiff=$(./scripts/no_lost_declarations.sh short)
+        declDiff=$(./scripts/declarations_diff.sh)
         if [ "$(printf '%s' "${declDiff}" | wc -l)" -gt 15 ]
         then
           declDiff="$(printf '<details><summary>\n\n%s\n\n</summary>\n\n%s\n\n</details>\n' "#### Declarations diff" "${declDiff}")"

.github/workflows/add_label_from_comment.yml

@@ -64,13 +64,10 @@ jobs:
 
       - if: (steps.parse_pr_head.outputs.head_user == 'leanprover-community') && (steps.parse_user.outputs.permission == 'admin')
         id: remove_labels
-        name: Remove "awaiting-review" and "awaiting-author"
+        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.issue.number }}/labels/awaiting-review \
-            --header 'authorization: Bearer ${{ secrets.GITHUB_TOKEN }}'
           curl --request DELETE \
             --url https://api.github.com/repos/${{ github.repository }}/issues/${{ github.event.issue.number }}/labels/awaiting-author \
             --header 'authorization: Bearer ${{ secrets.GITHUB_TOKEN }}'
@@ -131,13 +128,3 @@ jobs:
           labels: '["delegated"]'
         env:
           GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }}
-
-      - if: (steps.parse_pr_head.outputs.head_user == 'leanprover-community') && (steps.parse_user.outputs.permission == 'admin')
-        id: remove_labels
-        name: Remove "awaiting-review"
-        # 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.issue.number }}/labels/awaiting-review \
-            --header 'authorization: Bearer ${{ secrets.GITHUB_TOKEN }}'

.github/workflows/add_label_from_review.yml

@@ -64,13 +64,10 @@ jobs:
 
       - if: (steps.parse_pr_head.outputs.head_user == 'leanprover-community') && (steps.parse_user.outputs.permission == 'admin')
         id: remove_labels
-        name: Remove "awaiting-review" and "awaiting-author"
+        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-review \
-            --header 'authorization: Bearer ${{ secrets.TRIAGE_TOKEN }}'
           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 }}'
@@ -131,13 +128,3 @@ jobs:
           labels: '["delegated"]'
         env:
           GITHUB_TOKEN: ${{ secrets.TRIAGE_TOKEN }}
-
-      - if: (steps.parse_pr_head.outputs.head_user == 'leanprover-community') && (steps.parse_user.outputs.permission == 'admin')
-        id: remove_labels
-        name: Remove "awaiting-review"
-        # 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-review \
-            --header 'authorization: Bearer ${{ secrets.TRIAGE_TOKEN }}'

.github/workflows/bors.yml

@@ -236,19 +236,25 @@ jobs:
       - name: check declarations in db files
         run: |
           python3 scripts/yaml_check.py docs/100.yaml docs/overview.yaml docs/undergrad.yaml
-          lake exe checkYaml
+          lake exe check-yaml
 
       - name: verify `lake exe graph` works
         run: |
           lake exe graph
           rm import_graph.dot
 
+      - name: build everything
+        # make sure everything is available for test/import_all.lean
+        run: |
+          lake build Batteries Qq Aesop ProofWidgets
+
       - name: test mathlib
         id: test
         uses: liskin/gh-problem-matcher-wrap@v3
         with:
           linters: gcc
-          run: lake test
+          run:
+            lake test
 
       - name: check for unused imports
         id: shake

.github/workflows/build.yml

@@ -243,19 +243,25 @@ jobs:
       - name: check declarations in db files
         run: |
           python3 scripts/yaml_check.py docs/100.yaml docs/overview.yaml docs/undergrad.yaml
-          lake exe checkYaml
+          lake exe check-yaml
 
       - name: verify `lake exe graph` works
         run: |
           lake exe graph
           rm import_graph.dot
 
+      - name: build everything
+        # make sure everything is available for test/import_all.lean
+        run: |
+          lake build Batteries Qq Aesop ProofWidgets
+
       - name: test mathlib
         id: test
         uses: liskin/gh-problem-matcher-wrap@v3
         with:
           linters: gcc
-          run: lake test
+          run:
+            lake test
 
       - name: check for unused imports
         id: shake

.github/workflows/build.yml.in

@@ -222,19 +222,25 @@ jobs:
       - name: check declarations in db files
         run: |
           python3 scripts/yaml_check.py docs/100.yaml docs/overview.yaml docs/undergrad.yaml
-          lake exe checkYaml
+          lake exe check-yaml
 
       - name: verify `lake exe graph` works
         run: |
           lake exe graph
           rm import_graph.dot
 
+      - name: build everything
+        # make sure everything is available for test/import_all.lean
+        run: |
+          lake build Batteries Qq Aesop ProofWidgets
+
       - name: test mathlib
         id: test
         uses: liskin/gh-problem-matcher-wrap@v3
         with:
           linters: gcc
-          run: lake test
+          run:
+            lake test
 
       - name: check for unused imports
         id: shake

.github/workflows/build_fork.yml

@@ -240,19 +240,25 @@ jobs:
       - name: check declarations in db files
         run: |
           python3 scripts/yaml_check.py docs/100.yaml docs/overview.yaml docs/undergrad.yaml
-          lake exe checkYaml
+          lake exe check-yaml
 
       - name: verify `lake exe graph` works
         run: |
           lake exe graph
           rm import_graph.dot
 
+      - name: build everything
+        # make sure everything is available for test/import_all.lean
+        run: |
+          lake build Batteries Qq Aesop ProofWidgets
+
       - name: test mathlib
         id: test
         uses: liskin/gh-problem-matcher-wrap@v3
         with:
           linters: gcc
-          run: lake test
+          run:
+            lake test
 
       - name: check for unused imports
         id: shake

.github/workflows/labels_from_comment.yml

@@ -1,4 +1,4 @@
-# This workflow allows any user to add one of the `awaiting-review`, `awaiting-author`, or `WIP` labels,
+# This workflow allows any user to add one of the `awaiting-author`, or `WIP` labels,
 # by commenting on the PR or issue.
 # Other labels from this set are removed automatically at the same time.
 
@@ -10,7 +10,7 @@ on:
 
 jobs:
   update-label:
-    if: github.event.issue.pull_request != null && (contains(github.event.comment.body, 'awaiting-review') || contains(github.event.comment.body, 'awaiting-author') || contains(github.event.comment.body, 'WIP'))
+    if: github.event.issue.pull_request != null && (contains(github.event.comment.body, 'awaiting-author') || contains(github.event.comment.body, 'WIP'))
     runs-on: ubuntu-latest
 
     steps:
@@ -22,19 +22,14 @@ jobs:
           const { owner, repo, number: issue_number  } = context.issue;
           const commentLines = context.payload.comment.body.split('\r\n');
 
-          const awaitingReview = commentLines.includes('awaiting-review');
           const awaitingAuthor = commentLines.includes('awaiting-author');
           const wip = commentLines.includes('WIP');
 
-          if (awaitingReview || awaitingAuthor || wip) {
-            await github.rest.issues.removeLabel({ owner, repo, issue_number, name: 'awaiting-review' }).catch(() => {});
+          if (awaitingAuthor || wip) {
             await github.rest.issues.removeLabel({ owner, repo, issue_number, name: 'awaiting-author' }).catch(() => {});
             await github.rest.issues.removeLabel({ owner, repo, issue_number, name: 'WIP' }).catch(() => {});
           }
 
-          if (awaitingReview) {
-            await github.rest.issues.addLabels({ owner, repo, issue_number, labels: ['awaiting-review'] });
-          }
           if (awaitingAuthor) {
             await github.rest.issues.addLabels({ owner, repo, issue_number, labels: ['awaiting-author'] });
           }

.github/workflows/maintainer_merge_comment.yml

@@ -7,7 +7,7 @@ on:
 jobs:
   ping_zulip:
     name: Ping maintainers on Zulip
-    if: (github.event.issue.pull_request != 'null') && (startsWith(github.event.comment.body, 'maintainer merge') || contains(toJSON(github.event.comment.body), '\r\nmaintainer merge'))
+    if: (github.event.issue.pull_request != 'null') && (startsWith(github.event.comment.body, 'maintainer merge') || contains(toJSON(github.event.comment.body), '\nmaintainer merge'))
     runs-on: ubuntu-latest
     steps:
       - name: Check whether user is part of mathlib-reviewers team
@@ -30,7 +30,7 @@ jobs:
           type: 'stream'
           topic: 'maintainer merge'
           content: |
-            ${{ format('{0} requested a maintainer merge on PR [#{1}]({2}):', github.event.comment.user.login, github.event.issue.number, github.event.issue.html_url ) }}
+            ${{ format('{0} requested a maintainer merge from comment on PR [#{1}]({2}):', github.event.comment.user.login, github.event.issue.number, github.event.issue.html_url ) }}
 
             > ${{ github.event.issue.title }}
 

.github/workflows/maintainer_merge_review.yml

@@ -2,12 +2,13 @@ name: Maintainer merge (review)
 
 on:
   pull_request_review:
-    types: [submitted, edited]
+    # triggers on a review, whether or not it is accompanied by a comment
+    types: [submitted]
 
 jobs:
   ping_zulip:
     name: Ping maintainers on Zulip
-    if: (startsWith(github.event.review.body, 'maintainer merge') || contains(toJSON(github.event.review.body), '\r\nmaintainer merge'))
+    if: (startsWith(github.event.review.body, 'maintainer merge') || contains(toJSON(github.event.review.body), '\nmaintainer merge'))
     runs-on: ubuntu-latest
     steps:
       - name: Check whether user is part of mathlib-reviewers team
@@ -28,7 +29,7 @@ jobs:
           type: 'stream'
           topic: 'maintainer merge'
           content: |
-            ${{ format('{0} requested a maintainer merge on PR [#{1}]({2}):', github.event.review.user.login, github.event.pull_request.number, github.event.pull_request.html_url ) }}
+            ${{ format('{0} requested a maintainer merge from review on PR [#{1}]({2}):', github.event.review.user.login, github.event.pull_request.number, github.event.pull_request.html_url ) }}
 
             > ${{ github.event.pull_request.title }}
 

.github/workflows/maintainer_merge_review_comment.yml

@@ -7,7 +7,7 @@ on:
 jobs:
   ping_zulip:
     name: Ping maintainers on Zulip
-    if: (startsWith(github.event.comment.body, 'maintainer merge') || contains(toJSON(github.event.comment.body), '\r\nmaintainer merge'))
+    if: (startsWith(github.event.comment.body, 'maintainer merge') || contains(toJSON(github.event.comment.body), '\nmaintainer merge'))
     runs-on: ubuntu-latest
     steps:
       - name: Check whether user is part of mathlib-reviewers team
@@ -28,7 +28,7 @@ jobs:
           type: 'stream'
           topic: 'maintainer merge'
           content: |
-            ${{ format('{0} requested a maintainer merge on PR [#{1}]({2}):', github.event.comment.user.login, github.event.pull_request.number, github.event.pull_request.html_url ) }}
+            ${{ format('{0} requested a maintainer merge from review comment on PR [#{1}]({2}):', github.event.comment.user.login, github.event.pull_request.number, github.event.pull_request.html_url ) }}
 
             > ${{ github.event.pull_request.title }}
 

.github/workflows/nightly_detect_failure.yml

@@ -198,8 +198,21 @@ jobs:
             }
             response = client.get_messages(request)
             messages = response['messages']
-            payload = f"🛠️: it looks like it's time to create a new bump/nightly-{current_version} branch from nightly-testing, and then PR that to {bump_branch}."
-            if not messages or messages[0]['content'] != payload:
+            bump_branch_suffix = bump_branch.replace('bump/', '')
+            payload = f"🛠️: it looks like it's time to create a new bump/nightly-{current_version} branch from nightly-testing, and then PR that to {bump_branch}. "
+            payload += "To do so semi-automatically, run the following script from mathlib root:\n\n"
+            payload += f"```bash\n./scripts/create-adaptation-pr.sh {bump_branch_suffix} {current_version}\n```\n"
+            # Only post if the message is different
+            # We compare the first 160 characters, since that includes the date and bump version
+            if not messages or messages[0]['content'][:160] != payload[:160]:
+                # Log messages, because the bot seems to repeat itself...
+                if messages:
+                    print("###### Last message:")
+                    print(messages[0]['content'])
+                    print("###### Current message:")
+                    print(payload)
+                else:
+                    print('The strings match!')
                 # Post the reminder message
                 request = {
                     'type': 'stream',

.github/workflows/update_dependencies.yml

@@ -29,19 +29,18 @@ jobs:
       - name: Update dependencies
         run: lake update
 
-      - name: Generate branch name
-        id: generate_branch_name
+      - name: Generate PR title
         run: |
-          timestamp=$(date -u +"%Y-%m-%d-%H-%M")
-          echo "branch_name=update-dependencies-$timestamp" >> "$GITHUB_ENV"
+          echo "timestamp=$(date -u +"%Y-%m-%d-%H-%M")" >> "$GITHUB_ENV"
           echo "pr_title=chore: update Mathlib dependencies $(date -u +"%Y-%m-%d")" >> "$GITHUB_ENV"
 
       - name: Create Pull Request
         uses: peter-evans/create-pull-request@v6
         with:
           token: "${{ secrets.NIGHTLY_TESTING }}"
           commit-message: "chore: update Mathlib dependencies ${{ env.timestamp }}"
-          branch: "${{ env.branch_name }}"
+          # this branch is referenced in update_dependencies_zulip.yml
+          branch: "update-dependencies-bot-use-only"
           base: master
           title: "${{ env.pr_title }}"
           body: "This PR updates the Mathlib dependencies."