Merge branch 'master' into Field_Card_Emb

.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/build.in.yml

@@ -0,0 +1,332 @@
+### NB: This is the master file for autogenerating
+### NB: `.github/workflows/{bors, build_fork, build}.yml`.
+### NB: If you need to edit any of those files, you should edit this file instead,
+### NB: and regenerate those files by manually running
+### NB: .github/workflows/mk_build_yml.sh
+
+jobs:
+  # Cancels previous runs of jobs in this file
+  cancel:
+    if: github.repository == 'leanprover-community/mathlib4'
+    name: 'Cancel Previous Runs (CI)'
+    runs-on: ubuntu-latest
+    # timeout-minutes: 3
+    steps:
+      - uses: styfle/[email protected]
+        with:
+          all_but_latest: true
+          access_token: ${{ github.token }}
+
+  style_lint:
+    if: github.repository MAIN_OR_FORK 'leanprover-community/mathlib4'
+    name: Lint styleJOB_NAME
+    runs-on: STYLE_LINT_RUNNER
+    steps:
+      - name: cleanup
+        run: |
+          find . -name . -o -prune -exec rm -rf -- {} +
+
+      - uses: actions/checkout@v4
+
+      # Run the case checker action
+      - name: Check Case Sensitivity
+        uses: credfeto/[email protected]
+
+      - name: Look for ignored files
+        uses: credfeto/[email protected]
+
+      - name: "Check for Lean files with the executable bit set"
+        shell: bash
+        run: |
+          executable_files="$(find . -name '*.lean' -type f \( -perm -u=x -o -perm -g=x -o -perm -o=x \))"
+          if [[ -n "$executable_files" ]]
+          then
+            echo "ERROR: The following Lean files have the executable bit set."
+            echo "$executable_files"
+            exit 1
+          fi
+
+      - name: install Python
+        if: ${{ 'STYLE_LINT_RUNNER' == 'ubuntu-latest' }}
+        uses: actions/setup-python@v5
+        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: "run style linters"
+        run: |
+          lake exe lint-style
+
+      - name: Install bibtool
+        if: ${{ 'STYLE_LINT_RUNNER' == 'ubuntu-latest' }}
+        run: |
+          sudo apt-get update
+          sudo apt-get install -y bibtool
+
+      - name: lint references.bib
+        run: |
+          ./scripts/lint-bib.sh
+
+  build:
+    if: github.repository MAIN_OR_FORK 'leanprover-community/mathlib4'
+    name: BuildJOB_NAME
+    runs-on: RUNS_ON
+    steps:
+      - name: cleanup
+        run: |
+          find . -name . -o -prune -exec rm -rf -- {} +
+          # Delete all but the 5 most recent toolchains.
+          # Make sure to delete both the `~/.elan/toolchains/X` directory and the `~/.elan/update-hashes/X` file.
+          # Skip symbolic links (`-type d`), the current directory (`! -name .`), and `nightly` and `stable`.
+          if cd ~/.elan/toolchains && find . -maxdepth 1 -type d ! -name . -print0 | xargs -0 ls -1td | grep -v 'nightly$' | grep -v 'stable$' | tail -n +6 | xargs -I {} sh -c 'echo {} && rm -rf "{}" && rm "../update-hashes/{}"'; then
+              : # Do nothing on success
+          else
+              : # Do nothing on failure, but suppress errors
+          fi
+
+      # The Hoskinson runners may not have jq installed, so do that now.
+      - name: 'Setup jq'
+        uses: dcarbone/[email protected]
+
+      - 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}"
+
+      - uses: actions/checkout@v4
+
+      - name: If using a lean-pr-release toolchain, uninstall
+        run: |
+          if [[ $(cat lean-toolchain) =~ ^leanprover/lean4-pr-releases:pr-release-[0-9]+$ ]]; then
+            printf 'Uninstalling transient toolchain %s\n' "$(cat lean-toolchain)"
+            elan toolchain uninstall "$(cat lean-toolchain)"
+          fi
+
+      - name: print lean and lake versions
+        run: |
+          lean --version
+          lake --version
+
+      - name: build cache
+        run: |
+          lake build cache
+
+      - name: prune ProofWidgets .lake
+        run: |
+          # The ProofWidgets release contains not just the `.js` (which we need in order to build)
+          # but also `.oleans`, which may have been built with the wrong toolchain.
+          # This removes them.
+          # See discussion at https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/nightly-testing/near/411225235
+          rm -rf .lake/packages/proofwidgets/.lake/build/lib
+          rm -rf .lake/packages/proofwidgets/.lake/build/ir
+
+      - name: get cache
+        id: get
+        run: |
+          rm -rf .lake/build/lib/Mathlib/
+          # Fail quickly if the cache is completely cold, by checking for Mathlib.Init
+          lake exe cache get #Mathlib.Init
+          #lake build --no-build Mathlib.Init && lake exe cache get || echo "No cache for 'Mathlib.Init' available"
+
+      - name: update {Mathlib, Tactic, Counterexamples, Archive}.lean
+        id: mk_all
+        run: |
+
+          if ! lake exe mk_all --check
+          then
+            echo "Not all lean files are in the import all files"
+            echo "mk_all=false" >> "${GITHUB_OUTPUT}"
+          else
+            echo "mk_all=true" >> "${GITHUB_OUTPUT}"
+          fi
+
+      - name: build mathlib
+        id: build
+        uses: liskin/gh-problem-matcher-wrap@v3
+        with:
+          linters: gcc
+          run: |
+            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 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
+          # run this in CI if it gets an incorrect lake hash for existing cache files somehow
+          # lake exe cache put!
+          # do not try to upload files just downloaded
+          lake exe cache put-unpacked
+        env:
+          MATHLIB_CACHE_SAS: ${{ secrets.MATHLIB_CACHE_SAS }}
+          MATHLIB_CACHE_S3_TOKEN: ${{ secrets.MATHLIB_CACHE_S3_TOKEN }}
+
+      - name: check the cache
+        run: |
+          # Because the `lean-pr-testing-NNNN` branches use toolchains that are "updated in place"
+          # the cache mechanism is unreliable, so we don't test it if we are on such a branch.
+          if [[ ! $(cat lean-toolchain) =~ ^leanprover/lean4-pr-releases:pr-release-[0-9]+$ ]]; then
+            lake exe cache clean!
+            rm -rf .lake/build/lib/Mathlib
+            lake exe cache get || (sleep 1; lake exe cache get)
+            lake build --no-build
+          fi
+
+      - name: build archive
+        id: archive
+        run: |
+          # Note: we should not be including `Archive` and `Counterexamples` in the cache.
+          # We do this for now for the sake of not rebuilding them in every CI run
+          # even when they are not touched.
+          # Since `Archive` and `Counterexamples` files have very simple dependencies,
+          # it should be possible to determine whether they need to be built without actually
+          # 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"
+          lake exe cache put Archive.lean
+        env:
+          MATHLIB_CACHE_SAS: ${{ secrets.MATHLIB_CACHE_SAS }}
+          MATHLIB_CACHE_S3_TOKEN: ${{ secrets.MATHLIB_CACHE_S3_TOKEN }}
+
+      - name: build counterexamples
+        id: counterexamples
+        run: |
+          lake exe cache get Counterexamples.lean
+          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 }}
+          MATHLIB_CACHE_S3_TOKEN: ${{ secrets.MATHLIB_CACHE_S3_TOKEN }}
+
+      - name: Check {Mathlib, Tactic, Counterexamples, Archive}.lean
+        run: |
+          if [ ${{ steps.mk_all.outputs.mk_all }} == "false" ]
+          then
+            echo "Please run 'lake exe mk_all' to regenerate the import all files"
+            exit 1
+          fi
+
+      - name: check for noisy stdout lines
+        id: noisy
+        run: |
+          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: |
+          python3 scripts/yaml_check.py docs/100.yaml docs/overview.yaml docs/undergrad.yaml
+          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
+
+      - name: check for unused imports
+        id: shake
+        uses: liskin/gh-problem-matcher-wrap@v3
+        with:
+          linters: gcc
+          run: env LEAN_ABORT_ON_PANIC=1 lake exe shake --gh-style
+
+      - name: lint mathlib
+        if: ${{ always() && steps.build.outcome == 'success' || steps.build.outcome == 'failure' }}
+        id: lint
+        uses: liskin/gh-problem-matcher-wrap@v3
+        with:
+          linters: gcc
+          run: env LEAN_ABORT_ON_PANIC=1 lake exe runLinter Mathlib
+
+      # 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-NNNN and batteries-pr-testing-NNNN branches
+        if: always()
+        env:
+          TOKEN: ${{ secrets.LEAN_PR_TESTING }}
+          GITHUB_CONTEXT: ${{ toJson(github) }}
+          WORKFLOW_URL: https://github.com/${{ github.repository }}/actions/runs/${{ github.run_id }}
+          BUILD_OUTCOME: ${{ steps.build.outcome }}
+          NOISY_OUTCOME: ${{ steps.noisy.outcome }}
+          ARCHIVE_OUTCOME: ${{ steps.archive.outcome }}
+          COUNTEREXAMPLE_OUTCOME: ${{ steps.counterexamples.outcome }}
+          LINT_OUTCOME: ${{ steps.lint.outcome }}
+          TEST_OUTCOME: ${{ steps.test.outcome }}
+        run: |
+          scripts/lean-pr-testing-comments.sh lean
+          scripts/lean-pr-testing-comments.sh batteries
+
+  final:
+    name: Post-CI jobJOB_NAME
+    if: github.repository MAIN_OR_FORK 'leanprover-community/mathlib4'
+    needs: [style_lint, build]
+    runs-on: ubuntu-latest
+    steps:
+      - uses: actions/checkout@v4
+
+      - id: PR
+        uses: 8BitJonny/[email protected]
+        # TODO: this may not work properly if the same commit is pushed to multiple branches:
+        # https://github.com/8BitJonny/gh-get-current-pr/issues/8
+        with:
+          github-token: ${{ secrets.GITHUB_TOKEN }}
+          # Only return if PR is still open
+          filterOutClosed: true
+
+      - id: remove_labels
+        name: Remove "awaiting-CI"
+        # 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/${{ steps.PR.outputs.number }}/labels/awaiting-CI \
+            --header 'authorization: Bearer ${{ secrets.GITHUB_TOKEN }}'
+
+      - if: contains(steps.PR.outputs.pr_labels, 'auto-merge-after-CI')
+        name: If `auto-merge-after-CI` is present, add a `bors merge` comment.
+        uses: GrantBirki/comment@v2
+        with:
+          token: ${{ secrets.AUTO_MERGE_TOKEN }}
+          issue-number: ${{ steps.PR.outputs.number }}
+          body: |
+            As this PR is labelled `auto-merge-after-CI`, we are now sending it to bors:
+
+            bors merge