Merge pull request #14585 from leanprover-community/master

sync master

.github/PULL_REQUEST_TEMPLATE.md

@@ -4,6 +4,13 @@
 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, and is labeled with `awaiting-review`.
+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:
 

.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 `no_lost_declarations` 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/no_lost_declarations.sh short)
+        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/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,40 +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 Mathlib.lean
-        run: |
-          git ls-files 'Mathlib/*.lean' | LC_ALL=C sort | sed 's/\.lean//;s,/,.,g;s/^/import /' > Mathlib.lean
-
-      - name: update MathlibExtras.lean
-        run: |
-          git ls-files 'MathlibExtras/*.lean' | LC_ALL=C sort | sed 's/\.lean//;s,/,.,g;s/^/import /' > MathlibExtras.lean
-
-      - name: update Mathlib/Tactic.lean
-        run: |
-          git ls-files 'Mathlib/Tactic/*.lean' | LC_ALL=C sort | sed 's/\.lean//;s,/,.,g;s/^/import /' > Mathlib/Tactic.lean
-
-      - name: update Counterexamples.lean
-        run: |
-          git ls-files 'Counterexamples/*.lean' | LC_ALL=C sort | sed 's/\.lean//;s,/,.,g;s/^/import /' > Counterexamples.lean
-
-      - name: update Archive.lean
-        run: |
-          git ls-files 'Archive/*.lean' | LC_ALL=C sort | sed 's/\.lean//;s,/,.,g;s/^/import /' > Archive.lean
-
-      - name: check that all files are imported
-        run: git diff --exit-code
-
   check_workflows:
     if: github.repository == 'leanprover-community/mathlib4'
     name: check workflows
@@ -141,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: |
-          find Mathlib -name "*.lean" | LC_ALL=C sort | sed 's/\.lean//;s,/,.,g;s/^/import /' > Mathlib.lean
-
       - name: If using a lean-pr-release toolchain, uninstall
         run: |
           if [[ $(cat lean-toolchain) =~ ^leanprover/lean4-pr-releases:pr-release-[0-9]+$ ]]; then
@@ -165,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
@@ -179,6 +149,7 @@ jobs:
           rm -rf .lake/packages/proofwidgets/.lake/build/ir
 
       - name: get cache
+        id: get
         run: |
           lake exe cache clean
           lake exe cache get
@@ -189,15 +160,13 @@ jobs:
         with:
           linters: gcc
           run: |
-            bash -o pipefail -c "env LEAN_ABORT_ON_PANIC=1 lake build -KCI | tee stdout.log"
-
-      - name: build library_search cache
-        run: lake build -KCI MathlibExtras
+            bash -o pipefail -c "env LEAN_ABORT_ON_PANIC=1 lake build --wfail -KCI"
 
       - name: upload cache
-        # We only upload the cache if the build ran (either succeeding or failing),
-        # but not if it was skipped.
-        if: ${{ always() && steps.build.outcome == 'success' || steps.build.outcome == 'failure' }}
+        # We only upload the cache if the build started (whether succeeding, failing, or cancelled)
+        # but not if any earlier step failed or was cancelled.
+        # See discussion at https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/Some.20files.20not.20found.20in.20the.20cache/near/407183836
+        if: ${{ always() && steps.get.outcome == 'success' }}
         run: |
           # TODO: this is not doing anything currently, and needs to be integrated with put-unpacked
           # lake exe cache commit || true
@@ -217,17 +186,9 @@ jobs:
             lake exe cache clean!
             rm -rf .lake/build/lib/Mathlib
             lake exe cache get || (sleep 1; lake exe cache get)
-            # We pipe the output of `lake build` to a file,
-            # and if we find " Building Mathlib" in that file we kill `lake build`, and error.
-            lake build > tmp & tail --pid=$! -n +1 -F tmp | (! (grep -m 1 " Building Mathlib" && kill $! ))
+            lake build --no-build
           fi
 
-      - name: find `#`-commands
-        id: hash_commands
-        run: |
-          chmod u+x scripts/lint_hash_commands.sh
-          ./scripts/lint_hash_commands.sh
-
       - name: build archive
         id: archive
         run: |
@@ -239,7 +200,7 @@ jobs:
           # storing and transferring oleans over the network.
           # Hopefully a future re-implementation of `cache` will obviate the present need for this hack.
           lake exe cache get Archive.lean
-          bash -o pipefail -c "env LEAN_ABORT_ON_PANIC=1 lake build Archive | tee --append stdout.log"
+          bash -o pipefail -c "env LEAN_ABORT_ON_PANIC=1 lake build Archive"
           lake exe cache put Archive.lean
         env:
           MATHLIB_CACHE_SAS: ${{ secrets.MATHLIB_CACHE_SAS }}
@@ -249,7 +210,7 @@ jobs:
         id: counterexamples
         run: |
           lake exe cache get Counterexamples.lean
-          bash -o pipefail -c "env LEAN_ABORT_ON_PANIC=1 lake build Counterexamples | tee --append stdout.log"
+          bash -o pipefail -c "env LEAN_ABORT_ON_PANIC=1 lake build Counterexamples"
           lake exe cache put Counterexamples.lean
         env:
           MATHLIB_CACHE_SAS: ${{ secrets.MATHLIB_CACHE_SAS }}
@@ -258,9 +219,19 @@ jobs:
       - name: check for noisy stdout lines
         id: noisy
         run: |
-          grep --after-context=1 "stdout" stdout.log && ret=0
-          grep --after-context=1 "stderr" stdout.log && new=0
-          if [ "${ret}" == "0" ] || [ "${new}"  == "0" ]; then exit 1; fi
+          buildMsgs="$(
+            ##  we exploit `lake`s replay feature: since the cache is present, running
+            ##  `lake build` will reproduce all the outputs without having to recompute
+            lake build Mathlib Archive Counterexamples |
+            ##  we filter out the output lines that begin with `✔ [xx/yy]`, where xx, yy
+            ##  are either numbers or ?, and the "Build completed successfully." message.
+            ##  We keep the rest, which are actual outputs of the files
+            awk '!($0 ~ "^\\s*✔ \\[[?0-9]*/[?0-9]*\\]" || $0 == "Build completed successfully."){ print $0 }')"
+          if [ -n "${buildMsgs}" ]
+          then
+            printf $'%s\n' "${buildMsgs}"
+            exit 1
+          fi
 
       - name: check declarations in db files
         run: |
@@ -277,9 +248,7 @@ jobs:
         uses: liskin/gh-problem-matcher-wrap@v3
         with:
           linters: gcc
-          run: |
-            bash -o pipefail -c "
-            make -k -j 8 test"
+          run: lake test
 
       - name: check for unused imports
         id: shake
@@ -296,19 +265,10 @@ jobs:
           linters: gcc
           run: env LEAN_ABORT_ON_PANIC=1 lake exe runLinter Mathlib
 
-      - name: check environments using lean4checker
-        id: lean4checker
-        run: |
-          git clone https://github.com/leanprover/lean4checker
-          cd lean4checker
-          git checkout toolchain/v4.7.0
-          # Now that the git hash is embedded in each olean,
-          # we need to compile lean4checker on the same toolchain
-          cp ../lean-toolchain .
-          lake build
-          ./test.sh
-          cd ..
-          lake env lean4checker/.lake/build/bin/lean4checker
+      # We no longer run `lean4checker` in regular CI, as it is quite expensive for little benefit.
+      # Instead we run it in a cron job on master: see `lean4checker.yml`.
+      # Output is posted to the zulip topic
+      # https://leanprover.zulipchat.com/#narrow/stream/345428-mathlib-reviewers/topic/lean4checker
 
       - name: Post comments for lean-pr-testing branch
         if: always()
@@ -322,14 +282,13 @@ jobs:
           COUNTEREXAMPLE_OUTCOME: ${{ steps.counterexamples.outcome }}
           LINT_OUTCOME: ${{ steps.lint.outcome }}
           TEST_OUTCOME: ${{ steps.test.outcome }}
-          CHECK_OUTCOME: ${{ steps.lean4checker.outcome }}
         run: |
           scripts/lean-pr-testing-comments.sh
 
   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