Merge remote-tracking branch 'origin/master' into adomani/capture_exc…

…eptions
leanprover-community · Sep 2, 2024 · 6dbf078 · 6dbf078
2 parents 112a759 + bd5475a
commit 6dbf078
Show file tree

Hide file tree

Showing 683 changed files with 4,259 additions and 2,011 deletions.
diff --git a/.github/workflows/bot_fix_style_comment.yaml b/.github/workflows/bot_fix_style_comment.yaml
@@ -9,7 +9,6 @@ jobs:
     name: Fix style issues from lint
     if: (github.event.issue.pull_request) && (startsWith(github.event.comment.body, 'bot fix style') || contains(toJSON(github.event.comment.body), '\nbot fix style'))
     runs-on: ubuntu-latest
-    continue-on-error: true  # do not annoy the user when linting fails, as expected
     steps:
       - id: user_permission
         uses: actions-cool/check-user-permission@v2
@@ -58,7 +57,6 @@ jobs:
 
       - name: lint
         if: steps.user_permission.outputs.require-result == 'true'
-        continue-on-error: true  # allows the following `reviewdog` step to add GitHub suggestions
         run: |
           lake exe lint-style --fix
 
@@ -70,14 +68,15 @@ jobs:
 
       - name: lint references.bib
         if: steps.user_permission.outputs.require-result == 'true'
-        continue-on-error: true  # allows the following `reviewdog` step to add GitHub suggestions
         run: |
-          ./scripts/lint-bib.sh
+          # ignoring the return code allows the following `reviewdog` step to add GitHub suggestions
+          ./scripts/lint-bib.sh || true
 
       - name: update {Mathlib, Tactic, Counterexamples, Archive}.lean
         if: steps.user_permission.outputs.require-result == 'true'
-        continue-on-error: true  # allows the following `reviewdog` step to add GitHub suggestions
-        run: lake exe mk_all
+        run: |
+          # ignoring the return code allows the following `reviewdog` step to add GitHub suggestions
+          lake exe mk_all || true
 
       - name: Commit and push changes
         if: steps.user_permission.outputs.require-result == 'true'

diff --git a/.github/workflows/bot_fix_style_review.yaml b/.github/workflows/bot_fix_style_review.yaml
@@ -10,7 +10,6 @@ jobs:
     name: Fix style issues from lint
     if: (startsWith(github.event.review.body, 'bot fix style') || contains(toJSON(github.event.review.body), '\nbot fix style'))
     runs-on: ubuntu-latest
-    continue-on-error: true  # do not annoy the user when linting fails, as expected
     steps:
       - id: user_permission
         uses: actions-cool/check-user-permission@v2
@@ -64,7 +63,6 @@ jobs:
 
       - name: lint
         if: steps.user_permission.outputs.require-result == 'true'
-        continue-on-error: true  # allows the following `reviewdog` step to add GitHub suggestions
         run: |
           lake exe lint-style --fix
 
@@ -76,14 +74,15 @@ jobs:
 
       - name: lint references.bib
         if: steps.user_permission.outputs.require-result == 'true'
-        continue-on-error: true  # allows the following `reviewdog` step to add GitHub suggestions
         run: |
-          ./scripts/lint-bib.sh
+          # ignoring the return code allows the following `reviewdog` step to add GitHub suggestions
+          ./scripts/lint-bib.sh || true
 
       - name: update {Mathlib, Tactic, Counterexamples, Archive}.lean
         if: steps.user_permission.outputs.require-result == 'true'
-        continue-on-error: true  # allows the following `reviewdog` step to add GitHub suggestions
-        run: lake exe mk_all
+        run: |
+          # ignoring the return code allows the following `reviewdog` step to add GitHub suggestions
+          lake exe mk_all || true
 
       - name: Commit and push changes
         if: steps.user_permission.outputs.require-result == 'true'

diff --git a/.github/workflows/bot_fix_style_review_comment.yaml b/.github/workflows/bot_fix_style_review_comment.yaml
@@ -9,7 +9,6 @@ jobs:
     name: Fix style issues from lint
     if: (startsWith(github.event.comment.body, 'bot fix style') || contains(toJSON(github.event.comment.body), '\nbot fix style'))
     runs-on: ubuntu-latest
-    continue-on-error: true  # do not annoy the user when linting fails, as expected
     steps:
       - id: user_permission
         uses: actions-cool/check-user-permission@v2
@@ -62,7 +61,6 @@ jobs:
 
       - name: lint
         if: steps.user_permission.outputs.require-result == 'true'
-        continue-on-error: true  # allows the following `reviewdog` step to add GitHub suggestions
         run: |
           lake exe lint-style --fix
 
@@ -74,14 +72,15 @@ jobs:
 
       - name: lint references.bib
         if: steps.user_permission.outputs.require-result == 'true'
-        continue-on-error: true  # allows the following `reviewdog` step to add GitHub suggestions
         run: |
-          ./scripts/lint-bib.sh
+          # ignoring the return code allows the following `reviewdog` step to add GitHub suggestions
+          ./scripts/lint-bib.sh || true
 
       - name: update {Mathlib, Tactic, Counterexamples, Archive}.lean
         if: steps.user_permission.outputs.require-result == 'true'
-        continue-on-error: true  # allows the following `reviewdog` step to add GitHub suggestions
-        run: lake exe mk_all
+        run: |
+          # ignoring the return code allows the following `reviewdog` step to add GitHub suggestions
+          lake exe mk_all || true
 
       - name: Commit and push changes
         if: steps.user_permission.outputs.require-result == 'true'

diff --git a/.github/workflows/dependent-issues.yml b/.github/workflows/dependent-issues.yml
@@ -18,7 +18,7 @@ jobs:
   check:
     runs-on: ubuntu-latest
     steps:
-      - uses: z0al/dependent-issues@v1
+      - uses: z0al/dependent-issues@75d554cd9494b6e1766bc9d08a81c26444ad5c5a
         env:
           # (Required) The token to use to make API calls to GitHub.
           GITHUB_TOKEN: ${{ secrets.DEPENDENT_ISSUES_TOKEN }}

diff --git a/.github/workflows/lean4checker.yml b/.github/workflows/lean4checker.yml
@@ -69,7 +69,7 @@ jobs:
         run: |
           git clone https://github.com/leanprover/lean4checker
           cd lean4checker
-          git checkout v4.11.0-rc1
+          git checkout v4.11.0
           # Now that the git hash is embedded in each olean,
           # we need to compile lean4checker on the same toolchain
           cp ../lean-toolchain .

diff --git a/.github/workflows/lint_and_suggest_pr.yml b/.github/workflows/lint_and_suggest_pr.yml
@@ -30,14 +30,13 @@ jobs:
 
       # if you update this step (or its dependencies), please also update them in bot_fix_style_comment.yaml
       - name: lint
-        continue-on-error: true  # allows the following `reviewdog` step to add GitHub suggestions
         run: |
           lake exe lint-style --fix
 
       - name: suggester / lint-style
         uses: reviewdog/action-suggester@v1
         with:
-          tool_name: lint-style
+          tool_name: lint-style (comment with "bot fix style" to have the bot commit all style suggestions)
 
       - name: Install bibtool
         run: |
@@ -46,14 +45,14 @@ jobs:
 
       # if you update this step (or its dependencies), please also update them in bot_fix_style_comment.yaml
       - name: lint references.bib
-        continue-on-error: true  # allows the following `reviewdog` step to add GitHub suggestions
         run: |
-          ./scripts/lint-bib.sh
+          # ignoring the return code allows the following `reviewdog` step to add GitHub suggestions
+          ./scripts/lint-bib.sh || true
 
       - name: suggester / lint-bib
         uses: reviewdog/action-suggester@v1
         with:
-          tool_name: lint-bib
+          tool_name: lint-bib (comment with "bot fix style" to have the bot commit all style suggestions)
 
   check_imported:
     if: github.repository == 'leanprover-community/mathlib4' && github.event.pull_request.draft == false
@@ -75,10 +74,11 @@ jobs:
 
       # if you update this step (or its dependencies), please also update them in bot_fix_style_comment.yaml
       - name: update {Mathlib, Tactic, Counterexamples, Archive}.lean
-        continue-on-error: true  # allows the following `reviewdog` step to add GitHub suggestions
-        run: lake exe mk_all
+        run: 
+          # ignoring the return code allows the following `reviewdog` step to add GitHub suggestions
+          lake exe mk_all || true
 
       - name: suggester / import list
         uses: reviewdog/action-suggester@v1
         with:
-          tool_name: imports
+          tool_name: imports (comment with "bot fix style" to have the bot commit all style suggestions)
diff --git a/.github/workflows/maintainer_merge_comment.yml b/.github/workflows/maintainer_merge_comment.yml
@@ -20,6 +20,17 @@ jobs:
                                                   # This feature is only applicable in an issue (or PR) context
           exit: true # optional. If the action should exit if the user is not part of the team. Defaults to true.
 
+      - uses: actions/checkout@v4
+        with:
+          ref: master
+      - name: Determine Zulip topic
+        id: determine_topic
+        run: |
+          ./scripts/get_tlabel.sh "${PR}" >> "$GITHUB_OUTPUT"
+        env:
+          PR:  /repos/{owner}/{repo}/issues/{pull_number}
+          GH_TOKEN: ${{secrets.GITHUB_TOKEN}}
+
       - name: Send message on Zulip
         uses: zulip/github-actions-zulip/send-message@v1
         with:
@@ -28,7 +39,7 @@ jobs:
           organization-url: 'https://leanprover.zulipchat.com'
           to: 'mathlib reviewers'
           type: 'stream'
-          topic: 'maintainer merge'
+          topic: ${{ steps.determine_topic.outputs.topic }}
           content: |
             ${{ format('{0} requested a maintainer merge from comment on PR [#{1}]({2}):', github.event.comment.user.login, github.event.issue.number, github.event.issue.html_url ) }}
 

diff --git a/.github/workflows/maintainer_merge_review.yml b/.github/workflows/maintainer_merge_review.yml
@@ -19,6 +19,17 @@ jobs:
           token: ${{ secrets.MATHLIB_REVIEWERS_TEAM_KEY }} # required. Personal Access Token with the `read:org` permission
           exit: true # optional. If the action should exit if the user is not part of the team. Defaults to true.
 
+      - uses: actions/checkout@v4
+        with:
+          ref: master
+      - name: Determine Zulip topic
+        id: determine_topic
+        run: |
+          ./scripts/get_tlabel.sh "${PR}" >> "$GITHUB_OUTPUT"
+        env:
+          PR:  /repos/{owner}/{repo}/issues/{pull_number}
+          GH_TOKEN: ${{secrets.GITHUB_TOKEN}}
+
       - name: Send message on Zulip
         uses: zulip/github-actions-zulip/send-message@v1
         with:
@@ -27,7 +38,7 @@ jobs:
           organization-url: 'https://leanprover.zulipchat.com'
           to: 'mathlib reviewers'
           type: 'stream'
-          topic: 'maintainer merge'
+          topic: ${{ steps.determine_topic.outputs.topic }}
           content: |
             ${{ format('{0} requested a maintainer merge from review on PR [#{1}]({2}):', github.event.review.user.login, github.event.pull_request.number, github.event.pull_request.html_url ) }}
 

diff --git a/.github/workflows/maintainer_merge_review_comment.yml b/.github/workflows/maintainer_merge_review_comment.yml
@@ -18,6 +18,17 @@ jobs:
           token: ${{ secrets.MATHLIB_REVIEWERS_TEAM_KEY }} # required. Personal Access Token with the `read:org` permission
           exit: true # optional. If the action should exit if the user is not part of the team. Defaults to true.
 
+      - uses: actions/checkout@v4
+        with:
+          ref: master
+      - name: Determine Zulip topic
+        id: determine_topic
+        run: |
+          ./scripts/get_tlabel.sh "${PR}" >> "$GITHUB_OUTPUT"
+        env:
+          PR:  /repos/{owner}/{repo}/issues/{pull_number}
+          GH_TOKEN: ${{secrets.GITHUB_TOKEN}}
+
       - name: Send message on Zulip
         uses: zulip/github-actions-zulip/send-message@v1
         with:
@@ -26,7 +37,7 @@ jobs:
           organization-url: 'https://leanprover.zulipchat.com'
           to: 'mathlib reviewers'
           type: 'stream'
-          topic: 'maintainer merge'
+          topic: ${{ steps.determine_topic.outputs.topic }}
           content: |
             ${{ format('{0} requested a maintainer merge from review comment on PR [#{1}]({2}):', github.event.comment.user.login, github.event.pull_request.number, github.event.pull_request.html_url ) }}
 

diff --git a/.github/workflows/nolints.yml b/.github/workflows/nolints.yml
@@ -25,6 +25,9 @@ jobs:
           echo "$HOME/.elan/bin" >> "${GITHUB_PATH}"
 
       - uses: actions/checkout@v4
+        with:
+          ## fetch the whole repository, as we want to push to it later
+          fetch-depth: 0
 
       - name: print lean and lake versions
         run: |
@@ -61,7 +64,7 @@ jobs:
 
       - name: configure git setup
         run: |
-          git remote add origin-bot "https://leanprover-community-bot:${{ secrets.UPDATE_NOLINTS_TOKEN }}@github.com/leanprover-community/mathlib.git"
+          git remote add origin-bot "https://leanprover-community-bot:${{ secrets.UPDATE_NOLINTS_TOKEN }}@github.com/leanprover-community/mathlib4.git"
           git config user.email "[email protected]"
           git config user.name "leanprover-community-bot"
 

diff --git a/.github/workflows/update_dependencies.yml b/.github/workflows/update_dependencies.yml
@@ -19,25 +19,39 @@ jobs:
         uses: actions/checkout@v4
         with:
           fetch-depth: 0
-          token: "${{ secrets.NIGHTLY_TESTING }}"
+          token: "${{ secrets.UPDATE_DEPENDENCIES_TOKEN }}"
+
+      - name: Get PR and labels
+        id: PR # all the steps below are skipped if 'ready-to-merge' is in the list of labels found here
+        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
 
       - name: Configure Git User
+        if: ${{ !contains(steps.PR.outputs.pr_labels, 'ready-to-merge') }}
         run: |
           git config user.name "leanprover-community-mathlib4-bot"
           git config user.email "[email protected]"
 
       - name: Update dependencies
+        if: ${{ !contains(steps.PR.outputs.pr_labels, 'ready-to-merge') }}
         run: lake update
 
       - name: Generate PR title
+        if: ${{ !contains(steps.PR.outputs.pr_labels, 'ready-to-merge') }}
         run: |
           echo "timestamp=$(date -u +"%Y-%m-%d-%H-%M")" >> "$GITHUB_ENV"
           echo "pr_title=chore: update Mathlib dependencies $(date -u +"%Y-%m-%d")" >> "$GITHUB_ENV"
 
       - name: Create Pull Request
+        if: ${{ !contains(steps.PR.outputs.pr_labels, 'ready-to-merge') }}
         uses: peter-evans/create-pull-request@v6
         with:
-          token: "${{ secrets.NIGHTLY_TESTING }}"
+          token: "${{ secrets.UPDATE_DEPENDENCIES_TOKEN }}"
           commit-message: "chore: update Mathlib dependencies ${{ env.timestamp }}"
           # this branch is referenced in update_dependencies_zulip.yml
           branch: "update-dependencies-bot-use-only"

diff --git a/.github/workflows/update_dependencies_zulip.yml b/.github/workflows/update_dependencies_zulip.yml
@@ -1,7 +1,5 @@
 name: Monitor Dependency Update Failures
 
-# This action currently uses the NIGHTLY_TESTING secret, but could be moved to a separate secret.
-
 on:
   workflow_run:
     workflows: ["continuous integration"]
@@ -20,7 +18,7 @@ jobs:
         uses: actions/github-script@v7
         id: construct_message
         with:
-          github-token: ${{ secrets.NIGHTLY_TESTING }}
+          github-token: ${{ secrets.UPDATE_DEPENDENCIES_TOKEN }}
           result-encoding: string
           script: |
             const owner = context.repo.owner, repo = context.repo.repo;

diff --git a/Counterexamples/CliffordAlgebraNotInjective.lean b/Counterexamples/CliffordAlgebraNotInjective.lean
@@ -132,7 +132,7 @@ theorem sq_zero_of_αβγ_mul {x : K} : α * β * γ * x = 0 → x * x = 0 := by
   rw [Ideal.Quotient.eq_zero_iff_mem, Ideal.Quotient.eq_zero_iff_mem]
   exact mul_self_mem_kIdeal_of_X0_X1_X2_mul_mem
 
-/-- Though `αβγ` is not itself zero-/
+/-- Though `αβγ` is not itself zero -/
 theorem αβγ_ne_zero : α * β * γ ≠ 0 := fun h =>
   X0_X1_X2_not_mem_kIdeal <| Ideal.Quotient.eq_zero_iff_mem.1 h
 

diff --git a/LongestPole/SpeedCenterJson.lean b/LongestPole/SpeedCenterJson.lean
@@ -47,7 +47,7 @@ structure RunResponse where
   run : Run
 deriving ToJson, FromJson
 
-/-- The error response-/
+/-- The error response -/
 structure ErrorMessage where
   repo_id : String
   message : String