diff --git a/.github/workflows/bors.yml b/.github/workflows/bors.yml index 4c49350abc2bf..0947ced12a31f 100644 --- 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 index a94777b4ec1ba..0f36dcaf7ebb4 100644 --- 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 index 46ee546b5e70c..db75043e32d6a 100644 --- 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 index 2cc6ebff60ad1..e71806bd28534 100644 --- 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