From c9c411cbec9b019a6d7303c2902f27787dd6ea70 Mon Sep 17 00:00:00 2001 From: damiano Date: Fri, 31 May 2024 15:21:20 +0000 Subject: [PATCH] feat: `lake exe mk_all` in CI (#11874) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit This PR replaces the shell commands for importing all the mathlib libraries by a lean executable defined in #11853. Co-authored-by: Yaël Dillies --- .github/workflows/bors.yml | 28 ++++++++-------------------- .github/workflows/build.yml | 28 ++++++++-------------------- .github/workflows/build.yml.in | 28 ++++++++-------------------- .github/workflows/build_fork.yml | 28 ++++++++-------------------- 4 files changed, 32 insertions(+), 80 deletions(-) diff --git a/.github/workflows/bors.yml b/.github/workflows/bors.yml index 7f6a93267d1349..1a761d0043f615 100644 --- a/.github/workflows/bors.yml +++ b/.github/workflows/bors.yml @@ -64,24 +64,6 @@ jobs: run: | ./scripts/lint-bib.sh - check_imported: - if: github.repository == 'leanprover-community/mathlib4' - name: Check all files imported - runs-on: ubuntu-latest - steps: - - name: cleanup - run: | - find . -name . -o -prune -exec rm -rf -- {} + - - - uses: actions/checkout@v4 - - - name: update import-only files in {Mathlib Mathlib/Tactic Counterexamples Archive}.lean - run: | - ./scripts/mk_all.sh - - - name: check that all files are imported - run: git diff --exit-code - check_workflows: if: github.repository == 'leanprover-community/mathlib4' name: check workflows @@ -152,7 +134,7 @@ jobs: # but verify that this didn't change anything in the `check_imported` job. - name: update Mathlib.lean run: | - ./scripts/mk_all.sh Mathlib + lake exe mk_all --lib Mathlib - name: If using a lean-pr-release toolchain, uninstall run: | @@ -166,6 +148,12 @@ jobs: lean --version lake --version + - name: update {Mathlib, Tactic, Counterexamples, Archive}.lean + run: lake exe mk_all + + - name: check_imported + run: git diff --exit-code + - name: build cache run: | lake build cache @@ -319,7 +307,7 @@ jobs: final: name: Post-CI job if: github.repository == 'leanprover-community/mathlib4' - needs: [style_lint, build, check_imported] + needs: [style_lint, build] runs-on: ubuntu-latest steps: - uses: actions/checkout@v4 diff --git a/.github/workflows/build.yml b/.github/workflows/build.yml index feab74152d313e..d0b024d98018b3 100644 --- a/.github/workflows/build.yml +++ b/.github/workflows/build.yml @@ -71,24 +71,6 @@ jobs: run: | ./scripts/lint-bib.sh - check_imported: - if: github.repository == 'leanprover-community/mathlib4' - name: Check all files imported - runs-on: ubuntu-latest - steps: - - name: cleanup - run: | - find . -name . -o -prune -exec rm -rf -- {} + - - - uses: actions/checkout@v4 - - - name: update import-only files in {Mathlib Mathlib/Tactic Counterexamples Archive}.lean - run: | - ./scripts/mk_all.sh - - - name: check that all files are imported - run: git diff --exit-code - check_workflows: if: github.repository == 'leanprover-community/mathlib4' name: check workflows @@ -159,7 +141,7 @@ jobs: # but verify that this didn't change anything in the `check_imported` job. - name: update Mathlib.lean run: | - ./scripts/mk_all.sh Mathlib + lake exe mk_all --lib Mathlib - name: If using a lean-pr-release toolchain, uninstall run: | @@ -173,6 +155,12 @@ jobs: lean --version lake --version + - name: update {Mathlib, Tactic, Counterexamples, Archive}.lean + run: lake exe mk_all + + - name: check_imported + run: git diff --exit-code + - name: build cache run: | lake build cache @@ -326,7 +314,7 @@ jobs: final: name: Post-CI job if: github.repository == 'leanprover-community/mathlib4' - needs: [style_lint, build, check_imported] + needs: [style_lint, build] runs-on: ubuntu-latest steps: - uses: actions/checkout@v4 diff --git a/.github/workflows/build.yml.in b/.github/workflows/build.yml.in index 5ec3436864f1eb..a278c2459bcb5b 100644 --- a/.github/workflows/build.yml.in +++ b/.github/workflows/build.yml.in @@ -50,24 +50,6 @@ jobs: run: | ./scripts/lint-bib.sh - check_imported: - if: github.repository MAIN_OR_FORK 'leanprover-community/mathlib4' - name: Check all files importedJOB_NAME - runs-on: ubuntu-latest - steps: - - name: cleanup - run: | - find . -name . -o -prune -exec rm -rf -- {} + - - - uses: actions/checkout@v4 - - - name: update import-only files in {Mathlib Mathlib/Tactic Counterexamples Archive}.lean - run: | - ./scripts/mk_all.sh - - - 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 @@ -138,7 +120,7 @@ jobs: # but verify that this didn't change anything in the `check_imported` job. - name: update Mathlib.lean run: | - ./scripts/mk_all.sh Mathlib + lake exe mk_all --lib Mathlib - name: If using a lean-pr-release toolchain, uninstall run: | @@ -152,6 +134,12 @@ jobs: lean --version lake --version + - name: update {Mathlib, Tactic, Counterexamples, Archive}.lean + run: lake exe mk_all + + - name: check_imported + run: git diff --exit-code + - name: build cache run: | lake build cache @@ -305,7 +293,7 @@ jobs: final: name: Post-CI jobJOB_NAME if: github.repository MAIN_OR_FORK 'leanprover-community/mathlib4' - needs: [style_lint, build, check_imported] + needs: [style_lint, build] runs-on: ubuntu-latest steps: - uses: actions/checkout@v4 diff --git a/.github/workflows/build_fork.yml b/.github/workflows/build_fork.yml index bc00a41ce4aa3b..c2c0cafd0f8940 100644 --- a/.github/workflows/build_fork.yml +++ b/.github/workflows/build_fork.yml @@ -68,24 +68,6 @@ jobs: run: | ./scripts/lint-bib.sh - check_imported: - if: github.repository != 'leanprover-community/mathlib4' - name: Check all files imported (fork) - runs-on: ubuntu-latest - steps: - - name: cleanup - run: | - find . -name . -o -prune -exec rm -rf -- {} + - - - uses: actions/checkout@v4 - - - name: update import-only files in {Mathlib Mathlib/Tactic Counterexamples Archive}.lean - run: | - ./scripts/mk_all.sh - - - name: check that all files are imported - run: git diff --exit-code - check_workflows: if: github.repository != 'leanprover-community/mathlib4' name: check workflows (fork) @@ -156,7 +138,7 @@ jobs: # but verify that this didn't change anything in the `check_imported` job. - name: update Mathlib.lean run: | - ./scripts/mk_all.sh Mathlib + lake exe mk_all --lib Mathlib - name: If using a lean-pr-release toolchain, uninstall run: | @@ -170,6 +152,12 @@ jobs: lean --version lake --version + - name: update {Mathlib, Tactic, Counterexamples, Archive}.lean + run: lake exe mk_all + + - name: check_imported + run: git diff --exit-code + - name: build cache run: | lake build cache @@ -323,7 +311,7 @@ jobs: final: name: Post-CI job (fork) if: github.repository != 'leanprover-community/mathlib4' - needs: [style_lint, build, check_imported] + needs: [style_lint, build] runs-on: ubuntu-latest steps: - uses: actions/checkout@v4