feat: mkAll in CI

leanprover-community · Apr 3, 2024 · 50738b5 · 50738b5
1 parent 49729f9
commit 50738b5
Show file tree

Hide file tree

Showing 4 changed files with 36 additions and 100 deletions.
diff --git a/.github/workflows/bors.yml b/.github/workflows/bors.yml
@@ -73,31 +73,6 @@ jobs:
         run: |
           find . -name . -o -prune -exec rm -rf -- {} +
 
-      - uses: actions/checkout@v4
-
-      - name: update Mathlib.lean
-        run: |
-          git ls-files 'Mathlib/*.lean' | LC_ALL=C sort | sed 's/\.lean//;s,/,.,g;s/^/import /' > Mathlib.lean
-
-      - name: update MathlibExtras.lean
-        run: |
-          git ls-files 'MathlibExtras/*.lean' | LC_ALL=C sort | sed 's/\.lean//;s,/,.,g;s/^/import /' > MathlibExtras.lean
-
-      - name: update Mathlib/Tactic.lean
-        run: |
-          git ls-files 'Mathlib/Tactic/*.lean' | LC_ALL=C sort | sed 's/\.lean//;s,/,.,g;s/^/import /' > Mathlib/Tactic.lean
-
-      - name: update Counterexamples.lean
-        run: |
-          git ls-files 'Counterexamples/*.lean' | LC_ALL=C sort | sed 's/\.lean//;s,/,.,g;s/^/import /' > Counterexamples.lean
-
-      - name: update Archive.lean
-        run: |
-          git ls-files 'Archive/*.lean' | LC_ALL=C sort | sed 's/\.lean//;s,/,.,g;s/^/import /' > Archive.lean
-
-      - name: check that all files are imported
-        run: git diff --exit-code
-
   check_workflows:
     if: github.repository == 'leanprover-community/mathlib4'
     name: check workflows
@@ -165,6 +140,15 @@ jobs:
           lean --version
           lake --version
 
+      - uses: actions/checkout@v4
+
+      - name: update {Mathlib, MathlibExtras, Tactic, Counterexamples, Archive}.lean
+        run: lake exe mkAll
+
+      - name: check that all files are imported
+        run: git diff --exit-code
+
+
       - name: build cache
         run: |
           lake build cache

diff --git a/.github/workflows/build.yml b/.github/workflows/build.yml
@@ -80,31 +80,6 @@ jobs:
         run: |
           find . -name . -o -prune -exec rm -rf -- {} +
 
-      - uses: actions/checkout@v4
-
-      - name: update Mathlib.lean
-        run: |
-          git ls-files 'Mathlib/*.lean' | LC_ALL=C sort | sed 's/\.lean//;s,/,.,g;s/^/import /' > Mathlib.lean
-
-      - name: update MathlibExtras.lean
-        run: |
-          git ls-files 'MathlibExtras/*.lean' | LC_ALL=C sort | sed 's/\.lean//;s,/,.,g;s/^/import /' > MathlibExtras.lean
-
-      - name: update Mathlib/Tactic.lean
-        run: |
-          git ls-files 'Mathlib/Tactic/*.lean' | LC_ALL=C sort | sed 's/\.lean//;s,/,.,g;s/^/import /' > Mathlib/Tactic.lean
-
-      - name: update Counterexamples.lean
-        run: |
-          git ls-files 'Counterexamples/*.lean' | LC_ALL=C sort | sed 's/\.lean//;s,/,.,g;s/^/import /' > Counterexamples.lean
-
-      - name: update Archive.lean
-        run: |
-          git ls-files 'Archive/*.lean' | LC_ALL=C sort | sed 's/\.lean//;s,/,.,g;s/^/import /' > Archive.lean
-
-      - name: check that all files are imported
-        run: git diff --exit-code
-
   check_workflows:
     if: github.repository == 'leanprover-community/mathlib4'
     name: check workflows
@@ -172,6 +147,15 @@ jobs:
           lean --version
           lake --version
 
+      - uses: actions/checkout@v4
+
+      - name: update {Mathlib, MathlibExtras, Tactic, Counterexamples, Archive}.lean
+        run: lake exe mkAll
+
+      - name: check that all files are imported
+        run: git diff --exit-code
+
+
       - name: build cache
         run: |
           lake build cache

diff --git a/.github/workflows/build.yml.in b/.github/workflows/build.yml.in
@@ -59,31 +59,6 @@ jobs:
         run: |
           find . -name . -o -prune -exec rm -rf -- {} +
 
-      - uses: actions/checkout@v4
-
-      - name: update Mathlib.lean
-        run: |
-          git ls-files 'Mathlib/*.lean' | LC_ALL=C sort | sed 's/\.lean//;s,/,.,g;s/^/import /' > Mathlib.lean
-
-      - name: update MathlibExtras.lean
-        run: |
-          git ls-files 'MathlibExtras/*.lean' | LC_ALL=C sort | sed 's/\.lean//;s,/,.,g;s/^/import /' > MathlibExtras.lean
-
-      - name: update Mathlib/Tactic.lean
-        run: |
-          git ls-files 'Mathlib/Tactic/*.lean' | LC_ALL=C sort | sed 's/\.lean//;s,/,.,g;s/^/import /' > Mathlib/Tactic.lean
-
-      - name: update Counterexamples.lean
-        run: |
-          git ls-files 'Counterexamples/*.lean' | LC_ALL=C sort | sed 's/\.lean//;s,/,.,g;s/^/import /' > Counterexamples.lean
-
-      - name: update Archive.lean
-        run: |
-          git ls-files 'Archive/*.lean' | LC_ALL=C sort | sed 's/\.lean//;s,/,.,g;s/^/import /' > Archive.lean
-
-      - name: check that all files are imported
-        run: git diff --exit-code
-
   check_workflows:
     if: github.repository MAIN_OR_FORK 'leanprover-community/mathlib4'
     name: check workflowsJOB_NAME
@@ -151,6 +126,15 @@ jobs:
           lean --version
           lake --version
 
+      - uses: actions/checkout@v4
+
+      - name: update {Mathlib, MathlibExtras, Tactic, Counterexamples, Archive}.lean
+        run: lake exe mkAll
+
+      - name: check that all files are imported
+        run: git diff --exit-code
+
+
       - name: build cache
         run: |
           lake build cache

diff --git a/.github/workflows/build_fork.yml b/.github/workflows/build_fork.yml
@@ -77,31 +77,6 @@ jobs:
         run: |
           find . -name . -o -prune -exec rm -rf -- {} +
 
-      - uses: actions/checkout@v4
-
-      - name: update Mathlib.lean
-        run: |
-          git ls-files 'Mathlib/*.lean' | LC_ALL=C sort | sed 's/\.lean//;s,/,.,g;s/^/import /' > Mathlib.lean
-
-      - name: update MathlibExtras.lean
-        run: |
-          git ls-files 'MathlibExtras/*.lean' | LC_ALL=C sort | sed 's/\.lean//;s,/,.,g;s/^/import /' > MathlibExtras.lean
-
-      - name: update Mathlib/Tactic.lean
-        run: |
-          git ls-files 'Mathlib/Tactic/*.lean' | LC_ALL=C sort | sed 's/\.lean//;s,/,.,g;s/^/import /' > Mathlib/Tactic.lean
-
-      - name: update Counterexamples.lean
-        run: |
-          git ls-files 'Counterexamples/*.lean' | LC_ALL=C sort | sed 's/\.lean//;s,/,.,g;s/^/import /' > Counterexamples.lean
-
-      - name: update Archive.lean
-        run: |
-          git ls-files 'Archive/*.lean' | LC_ALL=C sort | sed 's/\.lean//;s,/,.,g;s/^/import /' > Archive.lean
-
-      - name: check that all files are imported
-        run: git diff --exit-code
-
   check_workflows:
     if: github.repository != 'leanprover-community/mathlib4'
     name: check workflows (fork)
@@ -169,6 +144,15 @@ jobs:
           lean --version
           lake --version
 
+      - uses: actions/checkout@v4
+
+      - name: update {Mathlib, MathlibExtras, Tactic, Counterexamples, Archive}.lean
+        run: lake exe mkAll
+
+      - name: check that all files are imported
+        run: git diff --exit-code
+
+
       - name: build cache
         run: |
           lake build cache