Trigger CI for leanprover/lean4#4717

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

@@ -69,7 +69,7 @@ jobs:
         run: |
           git clone https://github.com/leanprover/lean4checker
           cd lean4checker
-          git checkout v4.9.0
+          git checkout v4.10.0
           # Now that the git hash is embedded in each olean,
           # we need to compile lean4checker on the same toolchain
           cp ../lean-toolchain .

.github/workflows/lint_and_suggest_pr.yml

@@ -21,8 +21,15 @@ jobs:
         with:
           python-version: 3.8
 
+      - name: install elan
+        run: |
+          set -o pipefail
+          curl -sSfL https://github.com/leanprover/elan/releases/download/v3.1.1/elan-x86_64-unknown-linux-gnu.tar.gz | tar xz
+          ./elan-init -y --default-toolchain none
+          echo "$HOME/.elan/bin" >> "${GITHUB_PATH}"
+
       - name: lint
-        continue-on-error: true
+        continue-on-error: true  # allows the following `reviewdog` step to add GitHub suggestions
         run: |
           ./scripts/lint-style.sh --fix
 
@@ -37,7 +44,7 @@ jobs:
           sudo apt-get install -y bibtool
 
       - name: lint references.bib
-        continue-on-error: true
+        continue-on-error: true  # allows the following `reviewdog` step to add GitHub suggestions
         run: |
           ./scripts/lint-bib.sh
 
@@ -65,6 +72,7 @@ jobs:
           echo "$HOME/.elan/bin" >> "${GITHUB_PATH}"
 
       - name: update {Mathlib, Tactic, Counterexamples, Archive}.lean
+        continue-on-error: true  # allows the following `reviewdog` step to add GitHub suggestions
         run: lake exe mk_all
 
       - name: suggester / import list

.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_bump_toolchain.yml

@@ -1,8 +1,9 @@
 name: Bump lean-toolchain on nightly-testing
 
 on:
+  workflow_dispatch:
   schedule:
-    - cron: '0 10 * * *'  # 11AM CET/2AM PT, 3 hours after lean4 starts building the nightly.
+    - cron: '0 10/3 * * *'  # Run every three hours, starting at 11AM CET/2AM PT.
 
 jobs:
   update-toolchain:
@@ -30,5 +31,6 @@ jobs:
         git config user.name "leanprover-community-mathlib4-bot"
         git config user.email "[email protected]"
         git add lean-toolchain
-        git commit -m "chore: bump to ${RELEASE_TAG}"
+        # Don't fail if there's nothing to commit
+        git commit -m "chore: bump to ${RELEASE_TAG}" || true
         git push origin nightly-testing