fix: remove MathlibExtras from github actions

leanprover-community · Mar 19, 2024 · ba20f8f · ba20f8f
1 parent dca4e2e
commit ba20f8f
Show file tree

Hide file tree

Showing 5 changed files with 0 additions and 32 deletions.
diff --git a/.github/workflows/bors.yml b/.github/workflows/bors.yml
@@ -79,10 +79,6 @@ jobs:
         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
@@ -191,9 +187,6 @@ jobs:
           run: |
             bash -o pipefail -c "env LEAN_ABORT_ON_PANIC=1 lake build -KCI | tee stdout.log"
 
-      - name: build library_search cache
-        run: lake build -KCI MathlibExtras
-
       - name: upload cache
         # We only upload the cache if the build ran (either succeeding or failing),
         # but not if it was skipped.

diff --git a/.github/workflows/build.yml b/.github/workflows/build.yml
@@ -86,10 +86,6 @@ jobs:
         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
@@ -198,9 +194,6 @@ jobs:
           run: |
             bash -o pipefail -c "env LEAN_ABORT_ON_PANIC=1 lake build -KCI | tee stdout.log"
 
-      - name: build library_search cache
-        run: lake build -KCI MathlibExtras
-
       - name: upload cache
         # We only upload the cache if the build ran (either succeeding or failing),
         # but not if it was skipped.

diff --git a/.github/workflows/build.yml.in b/.github/workflows/build.yml.in
@@ -65,10 +65,6 @@ jobs:
         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
@@ -177,9 +173,6 @@ jobs:
           run: |
             bash -o pipefail -c "env LEAN_ABORT_ON_PANIC=1 lake build -KCI | tee stdout.log"
 
-      - name: build library_search cache
-        run: lake build -KCI MathlibExtras
-
       - name: upload cache
         # We only upload the cache if the build ran (either succeeding or failing),
         # but not if it was skipped.

diff --git a/.github/workflows/build_fork.yml b/.github/workflows/build_fork.yml
@@ -83,10 +83,6 @@ jobs:
         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
@@ -195,9 +191,6 @@ jobs:
           run: |
             bash -o pipefail -c "env LEAN_ABORT_ON_PANIC=1 lake build -KCI | tee stdout.log"
 
-      - name: build library_search cache
-        run: lake build -KCI MathlibExtras
-
       - name: upload cache
         # We only upload the cache if the build ran (either succeeding or failing),
         # but not if it was skipped.

diff --git a/.github/workflows/lint_and_suggest_pr.yml b/.github/workflows/lint_and_suggest_pr.yml
@@ -61,10 +61,6 @@ jobs:
         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