Merge remote-tracking branch 'origin/master' into eric-wieser/floor-normnum

Author: eric-wieser

.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

@@ -4,11 +4,29 @@
 PR is merged. Please leave a blank newline before the `---`, otherwise
 GitHub will format the text above it as a title.
 
+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.
+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.
@@ -17,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,33 +45,41 @@ 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:
         GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }}
+        BRANCH_NAME: ${{ github.head_ref }}
       run: |
         PR="${{ github.event.pull_request.number }}"
         title="### PR summary"
 
         ## Import count comment
-        importCount=$(python ./scripts/import-graph-report.py base.json head.json changed_files.txt)
+        importCount=$(
+          python ./scripts/import-graph-report.py base.json head.json changed_files.txt
+          ./scripts/import_trans_difference.sh
+        )
+
         if [ "$(printf '%s' "${importCount}" | wc -l)" -gt 12 ]
         then
-          importCount="$(printf '<details><summary>\n\n%s\n\n</summary>\n\n%s\n\n</details>\n' "#### Import changes" "${importCount}")"
+          importCount="$(printf '<details><summary>\n\n%s\n\n</summary>\n\n%s\n\n</details>\n' "#### Import changes for modified files" "${importCount}")"
         else
-          importCount="$(printf '#### Import changes\n\n%s\n' "${importCount}")"
+          importCount="$(printf '#### Import changes for modified files\n\n%s\n' "${importCount}")"
         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}")"
         else
           declDiff="$(printf '#### Declarations diff\n\n%s\n' "${declDiff}")"
         fi
+        git checkout "${BRANCH_NAME}"
+        currentHash="$(git rev-parse HEAD)"
+        hashURL="https://github.com/${{ github.repository }}/pull/${{ github.event.pull_request.number }}/commits/${currentHash}"
 
-        message="$(printf '%s\n\n%s\n\n---\n\n%s\n' "${title}" "${importCount}" "${declDiff}")"
+        message="$(printf '%s [%s](%s)\n\n%s\n\n---\n\n%s\n' "${title}" "$(git rev-parse --short HEAD)" "${hashURL}" "${importCount}" "${declDiff}")"
 
         ./scripts/update_PR_comment.sh "${message}" "${title}" "${PR}"

.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

@@ -50,7 +50,14 @@ jobs:
         with:
           python-version: 3.8
 
-      - name: lint
+      - 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: "run style linters: Python ones and their Lean rewrite"
         run: |
           ./scripts/lint-style.sh
 
@@ -83,23 +90,6 @@ jobs:
       - name: check that workflows were consistent
         run: git diff --exit-code
 
-  summarize_declarations:
-    if: github.repository == 'leanprover-community/mathlib4'
-    name: summarize_declarations
-    runs-on: ubuntu-latest
-    steps:
-      - uses: actions/checkout@v4
-        with:
-          ## fetch the whole repository, useful to find a common fork
-          fetch-depth: 0
-      - name: print_lost_declarations
-        run: |
-          ## back and forth to settle a "detached head" (maybe?)
-          git checkout -q master
-          git checkout -q -
-          printf '###  Summary\n\n' > "${GITHUB_STEP_SUMMARY}"
-          ./scripts/no_lost_declarations.sh >> "${GITHUB_STEP_SUMMARY}"
-
   build:
     if: github.repository == 'leanprover-community/mathlib4'
     name: Build
@@ -124,18 +114,12 @@ jobs:
       - name: install elan
         run: |
           set -o pipefail
-          curl -sSfL https://github.com/leanprover/elan/releases/download/v3.0.0/elan-x86_64-unknown-linux-gnu.tar.gz | tar xz
+          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}"
 
       - uses: actions/checkout@v4
 
-      # We update `Mathlib.lean` as a convenience here,
-      # but verify that this didn't change anything in the `check_imported` job.
-      - name: update Mathlib.lean
-        run: |
-          lake exe mk_all --lib Mathlib
-
       - name: If using a lean-pr-release toolchain, uninstall
         run: |
           if [[ $(cat lean-toolchain) =~ ^leanprover/lean4-pr-releases:pr-release-[0-9]+$ ]]; then
@@ -148,11 +132,8 @@ jobs:
           lean --version
           lake --version
 
-      - name: update {Mathlib, Tactic, Counterexamples, Archive}.lean
-        run: lake exe mk_all
-
-      - name: check_imported
-        run: git diff --exit-code
+      - name: check {Mathlib, Tactic, Counterexamples, Archive}.lean are up to date
+        run: lake exe mk_all --check
 
       - name: build cache
         run: |
@@ -255,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

@@ -57,7 +57,14 @@ jobs:
         with:
           python-version: 3.8
 
-      - name: lint
+      - 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: "run style linters: Python ones and their Lean rewrite"
         run: |
           ./scripts/lint-style.sh
 
@@ -90,23 +97,6 @@ jobs:
       - name: check that workflows were consistent
         run: git diff --exit-code
 
-  summarize_declarations:
-    if: github.repository == 'leanprover-community/mathlib4'
-    name: summarize_declarations
-    runs-on: ubuntu-latest
-    steps:
-      - uses: actions/checkout@v4
-        with:
-          ## fetch the whole repository, useful to find a common fork
-          fetch-depth: 0
-      - name: print_lost_declarations
-        run: |
-          ## back and forth to settle a "detached head" (maybe?)
-          git checkout -q master
-          git checkout -q -
-          printf '###  Summary\n\n' > "${GITHUB_STEP_SUMMARY}"
-          ./scripts/no_lost_declarations.sh >> "${GITHUB_STEP_SUMMARY}"
-
   build:
     if: github.repository == 'leanprover-community/mathlib4'
     name: Build
@@ -131,18 +121,12 @@ jobs:
       - name: install elan
         run: |
           set -o pipefail
-          curl -sSfL https://github.com/leanprover/elan/releases/download/v3.0.0/elan-x86_64-unknown-linux-gnu.tar.gz | tar xz
+          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}"
 
       - uses: actions/checkout@v4
 
-      # We update `Mathlib.lean` as a convenience here,
-      # but verify that this didn't change anything in the `check_imported` job.
-      - name: update Mathlib.lean
-        run: |
-          lake exe mk_all --lib Mathlib
-
       - name: If using a lean-pr-release toolchain, uninstall
         run: |
           if [[ $(cat lean-toolchain) =~ ^leanprover/lean4-pr-releases:pr-release-[0-9]+$ ]]; then
@@ -155,11 +139,8 @@ jobs:
           lean --version
           lake --version
 
-      - name: update {Mathlib, Tactic, Counterexamples, Archive}.lean
-        run: lake exe mk_all
-
-      - name: check_imported
-        run: git diff --exit-code
+      - name: check {Mathlib, Tactic, Counterexamples, Archive}.lean are up to date
+        run: lake exe mk_all --check
 
       - name: build cache
         run: |
@@ -262,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