Skip to content

Commit

Permalink
feat: mkAll in CI
Browse files Browse the repository at this point in the history
  • Loading branch information
@adomani
adomani committed Apr 3, 2024
1 parent 49729f9 commit 28f58fc
Show file tree
Hide file tree
Showing 4 changed files with 8 additions and 76 deletions.
21 changes: 2 additions & 19 deletions .github/workflows/bors.yml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -75,25 +75,8 @@ jobs:
- 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: update {Mathlib, MathlibExtras, Tactic, Counterexamples, Archive}.lean
run: lake exe mkAll

- name: check that all files are imported
run: git diff --exit-code
Expand Down
21 changes: 2 additions & 19 deletions .github/workflows/build.yml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -82,25 +82,8 @@ jobs:
- 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: update {Mathlib, MathlibExtras, Tactic, Counterexamples, Archive}.lean
run: lake exe mkAll

- name: check that all files are imported
run: git diff --exit-code
Expand Down
21 changes: 2 additions & 19 deletions .github/workflows/build.yml.in
View file
Original file line number Diff line number Diff line change
Expand Up @@ -61,25 +61,8 @@ jobs:

- 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: update {Mathlib, MathlibExtras, Tactic, Counterexamples, Archive}.lean
run: lake exe mkAll

- name: check that all files are imported
run: git diff --exit-code
Expand Down
21 changes: 2 additions & 19 deletions .github/workflows/build_fork.yml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -79,25 +79,8 @@ jobs:
- 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: update {Mathlib, MathlibExtras, Tactic, Counterexamples, Archive}.lean
run: lake exe mkAll

- name: check that all files are imported
run: git diff --exit-code
Expand Down

0 comments on commit 28f58fc

Please sign in to comment.