Merge branch 'master' into mo271/fract_div_intCast_eq_div_intCast_mod

.devcontainer/devcontainer.json

@@ -7,6 +7,10 @@
 
   "onCreateCommand": "lake exe cache get!",
 
+  "hostRequirements": {
+     "cpus": 4
+  },
+
   "customizations": {
     "vscode" : {
       "extensions" : [ "leanprover.lean4" ]

.github/workflows/build.yml.in → .github/build.in.yml

@@ -1,3 +1,4 @@
+# This is the master file for autogenerating `.github/workflows/{bors, build_fork, build }.yml`.
 
 jobs:
   # Cancels previous runs of jobs in this file
@@ -30,6 +31,17 @@ jobs:
       - name: Look for ignored files
         uses: credfeto/action-no-ignored-files@v1.1.0
 
+      - 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
@@ -43,9 +55,9 @@ jobs:
           ./elan-init -y --default-toolchain none
           echo "$HOME/.elan/bin" >> "${GITHUB_PATH}"
 
-      - name: "run style linters: Python ones and their Lean rewrite"
+      - name: "run style linters"
         run: |
-          ./scripts/lint-style.sh
+          lake exe lint-style
 
       - name: Install bibtool
         if: ${{ 'STYLE_LINT_RUNNER' == 'ubuntu-latest' }}
@@ -57,25 +69,6 @@ jobs:
         run: |
           ./scripts/lint-bib.sh
 
-  check_workflows:
-    if: github.repository MAIN_OR_FORK 'leanprover-community/mathlib4'
-    name: check workflowsJOB_NAME
-    runs-on: ubuntu-latest
-    steps:
-      - name: cleanup
-        run: |
-          find . -name . -o -prune -exec rm -rf -- {} +
-
-      - uses: actions/checkout@v4
-
-      - name: update workflows
-        run: |
-          cd .github/workflows/
-          ./mk_build_yml.sh
-
-      - name: check that workflows were consistent
-        run: git diff --exit-code
-
   build:
     if: github.repository MAIN_OR_FORK 'leanprover-community/mathlib4'
     name: BuildJOB_NAME
@@ -118,9 +111,6 @@ 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
@@ -137,16 +127,18 @@ jobs:
       - name: get cache
         id: get
         run: |
-          lake exe cache clean
-          lake exe cache get
+          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: 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"
+            bash -o pipefail -c "lake exe mk_all || echo \"There are unaccounted for files, but I am not failing yet\!\"; 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)
@@ -202,6 +194,9 @@ jobs:
           MATHLIB_CACHE_SAS: ${{ secrets.MATHLIB_CACHE_SAS }}
           MATHLIB_CACHE_S3_TOKEN: ${{ secrets.MATHLIB_CACHE_S3_TOKEN }}
 
+      - name: update {Mathlib, Tactic, Counterexamples, Archive}.lean
+        run: lake exe mk_all --check
+
       - name: check for noisy stdout lines
         id: noisy
         run: |
@@ -222,19 +217,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
@@ -299,7 +300,7 @@ jobs:
 
       - 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.0.1
+        uses: GrantBirki/comment@v2
         with:
           token: ${{ secrets.AUTO_MERGE_TOKEN }}
           issue-number: ${{ steps.PR.outputs.number }}

.github/workflows/actionlint.yml

@@ -1,10 +1,5 @@
-name: Actionlint
+name: Check workflows
 on:
-  push:
-    branches:
-      - 'master'
-    paths:
-      - '.github/**'
   pull_request:
     paths:
       - '.github/**'
@@ -14,7 +9,28 @@ jobs:
   actionlint:
     runs-on: ubuntu-latest
     steps:
-    - name: Checkout
-      uses: actions/checkout@v4
-    - name: actionlint
-      uses: raven-actions/actionlint@v1
+      - name: Checkout
+        uses: actions/checkout@v4
+
+      - name: suggester / actionlint
+        uses: reviewdog/action-actionlint@v1
+        with:
+          tool_name: actionlint
+          fail_on_error: true
+
+  check_build_yml:
+    name: check workflows generated by build.in.yml
+    runs-on: ubuntu-latest
+    steps:
+      - uses: actions/checkout@v4
+
+      - name: update workflows
+        run: |
+          cd .github/workflows/
+          ./mk_build_yml.sh
+
+      - name: suggester / build.in.yml
+        uses: reviewdog/action-suggester@v1
+        with:
+          tool_name: mk_build_yml.sh
+          fail_on_error: true

.github/workflows/add_label_from_comment.yml

@@ -7,50 +7,15 @@ on:
 jobs:
   add_ready_to_merge_label:
     name: Add ready-to-merge label
-    if: (toJSON(github.event.issue.pull_request) != 'null') && (startsWith(github.event.comment.body, 'bors r+') || contains(toJSON(github.event.comment.body), '\r\nbors r+') || startsWith(github.event.comment.body, 'bors merge') || contains(toJSON(github.event.comment.body), '\r\nbors merge'))
+    if: github.event.issue.pull_request && (startsWith(github.event.comment.body, 'bors r+') || contains(toJSON(github.event.comment.body), '\nbors r+') || startsWith(github.event.comment.body, 'bors merge') || contains(toJSON(github.event.comment.body), '\nbors merge'))
     runs-on: ubuntu-latest
     steps:
-      - uses: octokit/request-action@v2.x
-        name: Get PR head
-        id: get_pr_head
+      - id: user_permission
+        uses: actions-cool/check-user-permission@v2
         with:
-          route: GET /repos/:repository/pulls/:pull_number
-          repository: ${{ github.repository }}
-          pull_number: ${{ github.event.issue.number }}
-        env:
-          GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }}
-
-      # Parse steps.get_pr_head.outputs.data, since it is a string
-      - id: parse_pr_head
-        name: Parse PR head
-        uses: gr2m/get-json-paths-action@v1.x
-        with:
-          json: ${{ steps.get_pr_head.outputs.data }}
-          head_user: 'head.user.login'
-
-      # we skip the rest if this PR is from a fork,
-      # since the GITHUB_TOKEN doesn't have write perms
-      - if: steps.parse_pr_head.outputs.head_user == 'leanprover-community'
-        uses: octokit/request-action@v2.x
-        name: Get comment author
-        id: get_user
-        with:
-          route: GET /repos/:repository/collaborators/:username/permission
-          repository: ${{ github.repository }}
-          username: ${{ github.event.comment.user.login }}
-        env:
-          GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }}
+          require: 'admin'
 
-      # Parse steps.get_user.outputs.data, since it is a string
-      - if: steps.parse_pr_head.outputs.head_user == 'leanprover-community'
-        id: parse_user
-        name: Parse comment author permission
-        uses: gr2m/get-json-paths-action@v1.x
-        with:
-          json: ${{ steps.get_user.outputs.data }}
-          permission: 'permission'
-
-      - if: (steps.parse_pr_head.outputs.head_user == 'leanprover-community') && (steps.parse_user.outputs.permission == 'admin')
+      - if: (steps.user_permission.outputs.require-result == 'true') || (github.event.comment.user.login == 'leanprover-community-mathlib4-bot') || (github.event.comment.user.login == 'leanprover-community-bot-assistant')
         uses: octokit/request-action@v2.x
         id: add_label
         name: Add label
@@ -62,65 +27,27 @@ jobs:
         env:
           GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }}
 
-      - if: (steps.parse_pr_head.outputs.head_user == 'leanprover-community') && (steps.parse_user.outputs.permission == 'admin')
+      - if: (steps.user_permission.outputs.require-result == 'true') || (github.event.comment.user.login == 'leanprover-community-mathlib4-bot') || (github.event.comment.user.login == 'leanprover-community-bot-assistant')
         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 }}'
 
   add_delegated_label:
     name: Add delegated label
-    if: (toJSON(github.event.issue.pull_request) != 'null') && (startsWith(github.event.comment.body, 'bors d') || contains(toJSON(github.event.comment.body), '\r\nbors d'))
+    if: github.event.issue.pull_request && (startsWith(github.event.comment.body, 'bors d') || contains(toJSON(github.event.comment.body), '\nbors d'))
     runs-on: ubuntu-latest
     steps:
-      - uses: octokit/request-action@v2.x
-        name: Get PR head
-        id: get_pr_head
+      - id: user_permission
+        uses: actions-cool/check-user-permission@v2
         with:
-          route: GET /repos/:repository/pulls/:pull_number
-          repository: ${{ github.repository }}
-          pull_number: ${{ github.event.issue.number }}
-        env:
-          GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }}
+          require: 'admin'
 
-      # Parse steps.get_pr_head.outputs.data, since it is a string
-      - id: parse_pr_head
-        name: Parse PR head
-        uses: gr2m/get-json-paths-action@v1.x
-        with:
-          json: ${{ steps.get_pr_head.outputs.data }}
-          head_user: 'head.user.login'
-
-      # we skip the rest if this PR is from a fork,
-      # since the GITHUB_TOKEN doesn't have write perms
-      - if: steps.parse_pr_head.outputs.head_user == 'leanprover-community'
-        uses: octokit/request-action@v2.x
-        name: Get comment author
-        id: get_user
-        with:
-          route: GET /repos/:repository/collaborators/:username/permission
-          repository: ${{ github.repository }}
-          username: ${{ github.event.comment.user.login }}
-        env:
-          GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }}
-
-      # Parse steps.get_user.outputs.data, since it is a string
-      - if: steps.parse_pr_head.outputs.head_user == 'leanprover-community'
-        id: parse_user
-        name: Parse comment author permission
-        uses: gr2m/get-json-paths-action@v1.x
-        with:
-          json: ${{ steps.get_user.outputs.data }}
-          permission: 'permission'
-
-      - if: (steps.parse_pr_head.outputs.head_user == 'leanprover-community') && (steps.parse_user.outputs.permission == 'admin')
+      - if: (steps.user_permission.outputs.require-result == 'true') || (github.event.comment.user.login == 'leanprover-community-mathlib4-bot') || (github.event.comment.user.login == 'leanprover-community-bot-assistant')
         uses: octokit/request-action@v2.x
         id: add_label
         name: Add label
@@ -131,13 +58,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 }}'