From c6c28c0fd0c1e003f2faf61bf605cd69a00c0eb3 Mon Sep 17 00:00:00 2001 From: damiano Date: Sat, 1 Jun 2024 12:34:23 +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: Michael Rothgang 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 +++++++---------------- .github/workflows/lint_and_suggest_pr.yml | 13 +++++++++-- bors.toml | 2 +- 6 files changed, 44 insertions(+), 83 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 diff --git a/.github/workflows/lint_and_suggest_pr.yml b/.github/workflows/lint_and_suggest_pr.yml index 2dd1c52756af62..e543b3be5f345d 100644 --- a/.github/workflows/lint_and_suggest_pr.yml +++ b/.github/workflows/lint_and_suggest_pr.yml @@ -57,9 +57,18 @@ jobs: - uses: actions/checkout@v4 - - name: import files in {Mathlib Mathlib/Tactic Counterexamples Archive}.lean + - name: install elan run: | - ./scripts/mk_all.sh + set -o pipefail + curl -sSfL https://github.com/leanprover/elan/releases/download/v3.0.0/elan-x86_64-unknown-linux-gnu.tar.gz | tar xz + ./elan-init -y --default-toolchain none + echo "$HOME/.elan/bin" >> "${GITHUB_PATH}" + + - name: update {Mathlib, Tactic, Counterexamples, Archive}.lean + run: lake exe mk_all + + - name: check_imported + run: git diff --exit-code - name: suggester / import list uses: reviewdog/action-suggester@v1 diff --git a/bors.toml b/bors.toml index 69ee9273356c48..6f0bc95fdaa7ad 100644 --- a/bors.toml +++ b/bors.toml @@ -1,4 +1,4 @@ -status = ["Build", "Lint style", "Check all files imported"] +status = ["Build", "Lint style"] use_squash_merge = true timeout_sec = 28800 block_labels = ["not-ready-to-merge", "WIP", "blocked-by-other-PR", "merge-conflict", "awaiting-CI"]