Merge branch 'master' into LL/KernelFst'Snd'

.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
@@ -148,8 +149,10 @@ 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
@@ -316,7 +319,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/add_label_from_comment.yml

@@ -7,7 +7,7 @@ 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/[email protected]
@@ -74,7 +74,7 @@ jobs:
 
   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/[email protected]

.github/workflows/add_label_from_review.yml

@@ -7,7 +7,7 @@ on:
 jobs:
   add_ready_to_merge_label:
     name: Add ready-to-merge label
-    if: (startsWith(github.event.review.body, 'bors r+') || contains(toJSON(github.event.review.body), '\r\nbors r+') || startsWith(github.event.review.body, 'bors merge') || contains(toJSON(github.event.review.body), '\r\nbors merge'))
+    if: (startsWith(github.event.review.body, 'bors r+') || contains(toJSON(github.event.review.body), '\nbors r+') || startsWith(github.event.review.body, 'bors merge') || contains(toJSON(github.event.review.body), '\nbors merge'))
     runs-on: ubuntu-latest
     steps:
       - uses: octokit/[email protected]
@@ -74,7 +74,7 @@ jobs:
 
   add_delegated_label:
     name: Add delegated label
-    if: (startsWith(github.event.review.body, 'bors d') || contains(toJSON(github.event.review.body), '\r\nbors d'))
+    if: (startsWith(github.event.review.body, 'bors d') || contains(toJSON(github.event.review.body), '\nbors d'))
     runs-on: ubuntu-latest
     steps:
       - uses: octokit/[email protected]

.github/workflows/bors.yml

@@ -1,7 +1,7 @@
 # DO NOT EDIT THIS FILE!!!
 
 # This file is automatically generated by mk_build_yml.sh
-# Edit build.yml.in instead and run mk_build_yml.sh to update.
+# Edit .github/build.in.yml instead and run mk_build_yml.sh to update.
 
 # Forks of mathlib and other projects should be able to use build_fork.yml directly
 # The jobs in this file run on self-hosted workers and will not be run from external forks
@@ -162,8 +162,10 @@ 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
@@ -330,7 +332,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/bot_fix_style_comment.yaml

@@ -0,0 +1,93 @@
+name: bot fix style (comment)
+
+on:
+  issue_comment:
+    types: [created, edited]
+
+jobs:
+  fix_style:
+    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
+    steps:
+      - id: user_permission
+        uses: actions-cool/check-user-permission@v2
+        with:
+          require: 'write'
+
+      - name: Add reaction
+        if: steps.user_permission.outputs.require-result == 'true'
+        uses: peter-evans/create-or-update-comment@v4
+        with:
+          comment-id: ${{ github.event.comment.id }}
+          reactions: rocket
+
+      - name: cleanup
+        if: steps.user_permission.outputs.require-result == 'true'
+        run: |
+          find . -name . -o -prune -exec rm -rf -- {} +
+
+      - uses: actions/checkout@v4
+        if: steps.user_permission.outputs.require-result == 'true'
+        with:
+          token: ${{ secrets.BOT_FIX_STYLE_TOKEN }}
+
+      - name: Checkout PR branch
+        if: steps.user_permission.outputs.require-result == 'true'
+        run: |
+            gh pr checkout ${{ github.event.issue.number }}
+        env:
+            GH_TOKEN: ${{ secrets.BOT_FIX_STYLE_TOKEN }}
+
+      - name: install Python
+        if: steps.user_permission.outputs.require-result == 'true'
+        uses: actions/setup-python@v4
+        with:
+          python-version: 3.8
+
+      - name: install elan
+        if: steps.user_permission.outputs.require-result == 'true'
+        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}"
+
+      # run the same linting steps as in lint_and_suggest_pr.yaml
+
+      - name: lint
+        if: steps.user_permission.outputs.require-result == 'true'
+        run: |
+          lake exe lint-style --fix
+
+      - name: Install bibtool
+        if: steps.user_permission.outputs.require-result == 'true'
+        run: |
+          sudo apt-get update
+          sudo apt-get install -y bibtool
+
+      - name: lint references.bib
+        if: steps.user_permission.outputs.require-result == 'true'
+        run: |
+          # 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'
+        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'
+        run: |
+          # cleanup junk from build
+          rm elan-init
+          rm docs/references.bib.old
+          # setup commit and push
+          git config user.name "leanprover-community-mathlib4-bot"
+          git config user.email "[email protected]"
+          git add .
+          # Don't fail if there's nothing to commit
+          git commit -m "commit changes from style linters" || true
+          git push origin HEAD

.github/workflows/bot_fix_style_review.yaml

@@ -0,0 +1,99 @@
+name: bot fix style (review)
+
+on:
+  pull_request_review:
+    # triggers on a review, whether or not it is accompanied by a comment
+    types: [submitted]
+
+jobs:
+  fix_style:
+    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
+    steps:
+      - id: user_permission
+        uses: actions-cool/check-user-permission@v2
+        with:
+          require: 'write'
+
+      # Maybe no API exists for this yet?
+      # - name: Add reaction
+      #   if: steps.user_permission.outputs.require-result == 'true'
+      #   run: |
+      #       gh api --method POST \
+      #         -H "Accept: application/vnd.github+json" \
+      #         -H "X-GitHub-Api-Version: 2022-11-28" \
+      #         /repos/${{ github.repository_owner }}/${{ github.event.repository.name }}/pulls/${{ github.event.pull_request.number }}/reviews/${{ github.event.review.id }}/reactions \
+      #         -f "content=rocket"
+      #   env:
+      #       GH_TOKEN: ${{ secrets.BOT_FIX_STYLE_TOKEN }}
+
+      - name: cleanup
+        if: steps.user_permission.outputs.require-result == 'true'
+        run: |
+          find . -name . -o -prune -exec rm -rf -- {} +
+
+      - uses: actions/checkout@v4
+        if: steps.user_permission.outputs.require-result == 'true'
+        with:
+          token: ${{ secrets.BOT_FIX_STYLE_TOKEN }}
+
+      - name: Checkout PR branch
+        if: steps.user_permission.outputs.require-result == 'true'
+        run: |
+            gh pr checkout ${{ github.event.pull_request.number }}
+        env:
+            GH_TOKEN: ${{ secrets.BOT_FIX_STYLE_TOKEN }}
+
+      - name: install Python
+        if: steps.user_permission.outputs.require-result == 'true'
+        uses: actions/setup-python@v4
+        with:
+          python-version: 3.8
+
+      - name: install elan
+        if: steps.user_permission.outputs.require-result == 'true'
+        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}"
+
+      # run the same linting steps as in lint_and_suggest_pr.yaml
+
+      - name: lint
+        if: steps.user_permission.outputs.require-result == 'true'
+        run: |
+          lake exe lint-style --fix
+
+      - name: Install bibtool
+        if: steps.user_permission.outputs.require-result == 'true'
+        run: |
+          sudo apt-get update
+          sudo apt-get install -y bibtool
+
+      - name: lint references.bib
+        if: steps.user_permission.outputs.require-result == 'true'
+        run: |
+          # 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'
+        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'
+        run: |
+          # cleanup junk from build
+          rm elan-init
+          rm docs/references.bib.old
+          # setup commit and push
+          git config user.name "leanprover-community-mathlib4-bot"
+          git config user.email "[email protected]"
+          git add .
+          # Don't fail if there's nothing to commit
+          git commit -m "commit changes from style linters" || true
+          git push origin HEAD

.github/workflows/bot_fix_style_review_comment.yaml

@@ -0,0 +1,97 @@
+name: bot fix style (review comment)
+
+on:
+  pull_request_review_comment:
+    types: [created, edited]
+
+jobs:
+  fix_style:
+    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
+    steps:
+      - id: user_permission
+        uses: actions-cool/check-user-permission@v2
+        with:
+          require: 'write'
+
+      - name: Add reaction
+        if: steps.user_permission.outputs.require-result == 'true'
+        run: |
+            gh api --method POST \
+              -H "Accept: application/vnd.github+json" \
+              -H "X-GitHub-Api-Version: 2022-11-28" \
+              /repos/${{ github.repository_owner }}/${{ github.event.repository.name }}/pulls/comments/${{ github.event.comment.id }}/reactions \
+              -f "content=rocket"
+        env:
+            GH_TOKEN: ${{ secrets.BOT_FIX_STYLE_TOKEN }}
+
+      - name: cleanup
+        if: steps.user_permission.outputs.require-result == 'true'
+        run: |
+          find . -name . -o -prune -exec rm -rf -- {} +
+
+      - uses: actions/checkout@v4
+        if: steps.user_permission.outputs.require-result == 'true'
+        with:
+          token: ${{ secrets.BOT_FIX_STYLE_TOKEN }}
+
+      - name: Checkout PR branch
+        if: steps.user_permission.outputs.require-result == 'true'
+        run: |
+            gh pr checkout ${{ github.event.pull_request.number }}
+        env:
+            GH_TOKEN: ${{ secrets.BOT_FIX_STYLE_TOKEN }}
+
+      - name: install Python
+        if: steps.user_permission.outputs.require-result == 'true'
+        uses: actions/setup-python@v4
+        with:
+          python-version: 3.8
+
+      - name: install elan
+        if: steps.user_permission.outputs.require-result == 'true'
+        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}"
+
+      # run the same linting steps as in lint_and_suggest_pr.yaml
+
+      - name: lint
+        if: steps.user_permission.outputs.require-result == 'true'
+        run: |
+          lake exe lint-style --fix
+
+      - name: Install bibtool
+        if: steps.user_permission.outputs.require-result == 'true'
+        run: |
+          sudo apt-get update
+          sudo apt-get install -y bibtool
+
+      - name: lint references.bib
+        if: steps.user_permission.outputs.require-result == 'true'
+        run: |
+          # 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'
+        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'
+        run: |
+          # cleanup junk from build
+          rm elan-init
+          rm docs/references.bib.old
+          # setup commit and push
+          git config user.name "leanprover-community-mathlib4-bot"
+          git config user.email "[email protected]"
+          git add .
+          # Don't fail if there's nothing to commit
+          git commit -m "commit changes from style linters" || true
+          git push origin HEAD