Trigger CI for leanprover/lean4#3106

.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 <author@email.com>
 
+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

@@ -0,0 +1,85 @@
+name: Post PR summary comment
+
+on:
+  pull_request:
+
+jobs:
+  build:
+    runs-on: ubuntu-latest
+
+    steps:
+    - name: Checkout code
+      uses: actions/checkout@v4
+      with:
+        fetch-depth: 0
+
+    - name: Set up Python
+      uses: actions/setup-python@v5
+      with:
+        python-version: 3.12
+
+    - name: Install dependencies
+      run: |
+        python -m pip install --upgrade pip
+        sudo apt-get install -y jq
+        # If you have additional dependencies, install them here
+
+    - name: Get changed files
+      run: |
+        git fetch origin ${{ github.base_ref }}  # fetch the base branch
+        git diff --name-only origin/${{ github.base_ref }}... > changed_files.txt  # get the list of changed files
+
+    - name: Compute transitive imports
+      run: |
+        # the checkout dance, to avoid a detached head
+        git checkout master
+        git checkout -
+        currentHash="$(git rev-parse HEAD)"
+
+        # Compute the counts for the HEAD of the PR
+        python ./scripts/count-trans-deps.py "Mathlib/" > head.json
+
+        # Checkout the merge base
+        git checkout "$(git merge-base master ${{ github.sha }})"
+
+        # Compute the counts for the merge base
+        python ./scripts/count-trans-deps.py "Mathlib/" > base.json
+
+        # 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
+          ./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 for modified files" "${importCount}")"
+        else
+          importCount="$(printf '#### Import changes for modified files\n\n%s\n' "${importCount}")"
+        fi
+
+        ## Declarations' diff comment
+        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 [%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
 
@@ -64,24 +71,6 @@ jobs:
         run: |
           ./scripts/lint-bib.sh
 
-  check_imported:
-    if: github.repository == 'leanprover-community/mathlib4'
-    name: Check all files imported
-    runs-on: ubuntu-latest
-    steps:
-      - name: cleanup
-        run: |
-          find . -name . -o -prune -exec rm -rf -- {} +
-
-      - uses: actions/checkout@v4
-
-      - name: update import-only files in {Mathlib Mathlib/Tactic Counterexamples Archive}.lean
-        run: |
-          ./scripts/mk_all.sh
-
-      - name: check that all files are imported
-        run: git diff --exit-code
-
   check_workflows:
     if: github.repository == 'leanprover-community/mathlib4'
     name: check workflows
@@ -101,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
@@ -142,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: |
-          ./scripts/mk_all.sh Mathlib
-
       - name: If using a lean-pr-release toolchain, uninstall
         run: |
           if [[ $(cat lean-toolchain) =~ ^leanprover/lean4-pr-releases:pr-release-[0-9]+$ ]]; then
@@ -166,6 +132,9 @@ 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
@@ -267,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
@@ -319,7 +294,7 @@ jobs:
   final:
     name: Post-CI job
     if: github.repository == 'leanprover-community/mathlib4'
-    needs: [style_lint, build, check_imported]
+    needs: [style_lint, build]
     runs-on: ubuntu-latest
     steps:
       - uses: actions/checkout@v4