From 504f14fe94bb12ce92372223d9897b0a9e276b5b Mon Sep 17 00:00:00 2001 From: damiano Date: Wed, 18 Sep 2024 00:26:15 +0000 Subject: [PATCH] CI: fix mk_all (#16896) This should fix the `mk_all` step in CI that leaves through PRs that do not import all files. --- .github/build.in.yml | 23 ++++++++++++++++++++--- .github/workflows/bors.yml | 23 ++++++++++++++++++++--- .github/workflows/build.yml | 23 ++++++++++++++++++++--- .github/workflows/build_fork.yml | 23 ++++++++++++++++++++--- Mathlib/Nothing.lean | 1 + 5 files changed, 81 insertions(+), 12 deletions(-) create mode 100644 Mathlib/Nothing.lean diff --git a/.github/build.in.yml b/.github/build.in.yml index 023ae1426b9ef4..0681d86ddadf34 100644 --- a/.github/build.in.yml +++ b/.github/build.in.yml @@ -132,13 +132,25 @@ jobs: lake exe cache get Mathlib.Init lake build --no-build Mathlib.Init && lake exe cache get || echo "No cache for 'Mathlib.Init' available" + - name: update {Mathlib, Tactic, Counterexamples, Archive}.lean + id: mk_all + run: | + + if ! lake exe mk_all --check + then + echo "Not all lean files are in the import all files" + echo "mk_all=false" >> "${GITHUB_OUTPUT}" + else + echo "mk_all=true" >> "${GITHUB_OUTPUT}" + fi + - name: build mathlib id: build uses: liskin/gh-problem-matcher-wrap@v3 with: linters: gcc run: | - bash -o pipefail -c "lake exe mk_all || echo \"There are unaccounted for files, but I am not failing yet\!\"; env LEAN_ABORT_ON_PANIC=1 lake build --wfail -KCI" + bash -o pipefail -c "env LEAN_ABORT_ON_PANIC=1 lake build --wfail -KCI" - name: upload cache # We only upload the cache if the build started (whether succeeding, failing, or cancelled) @@ -194,8 +206,13 @@ jobs: MATHLIB_CACHE_SAS: ${{ secrets.MATHLIB_CACHE_SAS }} MATHLIB_CACHE_S3_TOKEN: ${{ secrets.MATHLIB_CACHE_S3_TOKEN }} - - name: update {Mathlib, Tactic, Counterexamples, Archive}.lean - run: lake exe mk_all --check + - name: Check {Mathlib, Tactic, Counterexamples, Archive}.lean + run: | + if [ ${{ steps.mk_all.outputs.mk_all }} == "false" ] + then + echo "Please run 'lake exe mk_all' to regenerate the import all files" + exit 1 + fi - name: check for noisy stdout lines id: noisy diff --git a/.github/workflows/bors.yml b/.github/workflows/bors.yml index ecd90d0749bb20..02e70351023a5e 100644 --- a/.github/workflows/bors.yml +++ b/.github/workflows/bors.yml @@ -145,13 +145,25 @@ jobs: lake exe cache get Mathlib.Init lake build --no-build Mathlib.Init && lake exe cache get || echo "No cache for 'Mathlib.Init' available" + - name: update {Mathlib, Tactic, Counterexamples, Archive}.lean + id: mk_all + run: | + + if ! lake exe mk_all --check + then + echo "Not all lean files are in the import all files" + echo "mk_all=false" >> "${GITHUB_OUTPUT}" + else + echo "mk_all=true" >> "${GITHUB_OUTPUT}" + fi + - name: build mathlib id: build uses: liskin/gh-problem-matcher-wrap@v3 with: linters: gcc run: | - bash -o pipefail -c "lake exe mk_all || echo \"There are unaccounted for files, but I am not failing yet\!\"; env LEAN_ABORT_ON_PANIC=1 lake build --wfail -KCI" + bash -o pipefail -c "env LEAN_ABORT_ON_PANIC=1 lake build --wfail -KCI" - name: upload cache # We only upload the cache if the build started (whether succeeding, failing, or cancelled) @@ -207,8 +219,13 @@ jobs: MATHLIB_CACHE_SAS: ${{ secrets.MATHLIB_CACHE_SAS }} MATHLIB_CACHE_S3_TOKEN: ${{ secrets.MATHLIB_CACHE_S3_TOKEN }} - - name: update {Mathlib, Tactic, Counterexamples, Archive}.lean - run: lake exe mk_all --check + - name: Check {Mathlib, Tactic, Counterexamples, Archive}.lean + run: | + if [ ${{ steps.mk_all.outputs.mk_all }} == "false" ] + then + echo "Please run 'lake exe mk_all' to regenerate the import all files" + exit 1 + fi - name: check for noisy stdout lines id: noisy diff --git a/.github/workflows/build.yml b/.github/workflows/build.yml index fc7ca496b13912..cd482c1de45090 100644 --- a/.github/workflows/build.yml +++ b/.github/workflows/build.yml @@ -152,13 +152,25 @@ jobs: lake exe cache get Mathlib.Init lake build --no-build Mathlib.Init && lake exe cache get || echo "No cache for 'Mathlib.Init' available" + - name: update {Mathlib, Tactic, Counterexamples, Archive}.lean + id: mk_all + run: | + + if ! lake exe mk_all --check + then + echo "Not all lean files are in the import all files" + echo "mk_all=false" >> "${GITHUB_OUTPUT}" + else + echo "mk_all=true" >> "${GITHUB_OUTPUT}" + fi + - name: build mathlib id: build uses: liskin/gh-problem-matcher-wrap@v3 with: linters: gcc run: | - bash -o pipefail -c "lake exe mk_all || echo \"There are unaccounted for files, but I am not failing yet\!\"; env LEAN_ABORT_ON_PANIC=1 lake build --wfail -KCI" + bash -o pipefail -c "env LEAN_ABORT_ON_PANIC=1 lake build --wfail -KCI" - name: upload cache # We only upload the cache if the build started (whether succeeding, failing, or cancelled) @@ -214,8 +226,13 @@ jobs: MATHLIB_CACHE_SAS: ${{ secrets.MATHLIB_CACHE_SAS }} MATHLIB_CACHE_S3_TOKEN: ${{ secrets.MATHLIB_CACHE_S3_TOKEN }} - - name: update {Mathlib, Tactic, Counterexamples, Archive}.lean - run: lake exe mk_all --check + - name: Check {Mathlib, Tactic, Counterexamples, Archive}.lean + run: | + if [ ${{ steps.mk_all.outputs.mk_all }} == "false" ] + then + echo "Please run 'lake exe mk_all' to regenerate the import all files" + exit 1 + fi - name: check for noisy stdout lines id: noisy diff --git a/.github/workflows/build_fork.yml b/.github/workflows/build_fork.yml index dc971651acfde6..f08ba63897a503 100644 --- a/.github/workflows/build_fork.yml +++ b/.github/workflows/build_fork.yml @@ -149,13 +149,25 @@ jobs: lake exe cache get Mathlib.Init lake build --no-build Mathlib.Init && lake exe cache get || echo "No cache for 'Mathlib.Init' available" + - name: update {Mathlib, Tactic, Counterexamples, Archive}.lean + id: mk_all + run: | + + if ! lake exe mk_all --check + then + echo "Not all lean files are in the import all files" + echo "mk_all=false" >> "${GITHUB_OUTPUT}" + else + echo "mk_all=true" >> "${GITHUB_OUTPUT}" + fi + - name: build mathlib id: build uses: liskin/gh-problem-matcher-wrap@v3 with: linters: gcc run: | - bash -o pipefail -c "lake exe mk_all || echo \"There are unaccounted for files, but I am not failing yet\!\"; env LEAN_ABORT_ON_PANIC=1 lake build --wfail -KCI" + bash -o pipefail -c "env LEAN_ABORT_ON_PANIC=1 lake build --wfail -KCI" - name: upload cache # We only upload the cache if the build started (whether succeeding, failing, or cancelled) @@ -211,8 +223,13 @@ jobs: MATHLIB_CACHE_SAS: ${{ secrets.MATHLIB_CACHE_SAS }} MATHLIB_CACHE_S3_TOKEN: ${{ secrets.MATHLIB_CACHE_S3_TOKEN }} - - name: update {Mathlib, Tactic, Counterexamples, Archive}.lean - run: lake exe mk_all --check + - name: Check {Mathlib, Tactic, Counterexamples, Archive}.lean + run: | + if [ ${{ steps.mk_all.outputs.mk_all }} == "false" ] + then + echo "Please run 'lake exe mk_all' to regenerate the import all files" + exit 1 + fi - name: check for noisy stdout lines id: noisy diff --git a/Mathlib/Nothing.lean b/Mathlib/Nothing.lean new file mode 100644 index 00000000000000..e95cb5d1f6aa9f --- /dev/null +++ b/Mathlib/Nothing.lean @@ -0,0 +1 @@ +-- nothing