Trigger CI for leanprover/lean4#3714

leanprover-community · Sep 19, 2024 · e3e8e9b · e3e8e9b
2 parents 321f629 + 02caa3e
commit e3e8e9b
Show file tree

Hide file tree

Showing 415 changed files with 16,309 additions and 5,640 deletions.
diff --git a/.github/build.in.yml b/.github/build.in.yml
@@ -69,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
@@ -130,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
@@ -154,6 +132,18 @@ jobs:
           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
@@ -216,6 +206,14 @@ jobs:
           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: |

diff --git a/.github/workflows/actionlint.yml b/.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
diff --git a/.github/workflows/bors.yml b/.github/workflows/bors.yml
@@ -82,25 +82,6 @@ jobs:
         run: |
           ./scripts/lint-bib.sh
 
-  check_workflows:
-    if: github.repository == 'leanprover-community/mathlib4'
-    name: check workflows
-    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 == 'leanprover-community/mathlib4'
     name: Build
@@ -143,9 +124,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
@@ -167,6 +145,18 @@ jobs:
           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
@@ -229,6 +219,14 @@ jobs:
           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: |

diff --git a/.github/workflows/build.yml b/.github/workflows/build.yml
@@ -89,25 +89,6 @@ jobs:
         run: |
           ./scripts/lint-bib.sh
 
-  check_workflows:
-    if: github.repository == 'leanprover-community/mathlib4'
-    name: check workflows
-    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 == 'leanprover-community/mathlib4'
     name: Build
@@ -150,9 +131,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
@@ -174,6 +152,18 @@ jobs:
           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
@@ -236,6 +226,14 @@ jobs:
           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: |

diff --git a/.github/workflows/build_fork.yml b/.github/workflows/build_fork.yml
@@ -86,25 +86,6 @@ jobs:
         run: |
           ./scripts/lint-bib.sh
 
-  check_workflows:
-    if: github.repository != 'leanprover-community/mathlib4'
-    name: check workflows (fork)
-    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 != 'leanprover-community/mathlib4'
     name: Build (fork)
@@ -147,9 +128,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
@@ -171,6 +149,18 @@ jobs:
           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
@@ -233,6 +223,14 @@ jobs:
           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: |