From f356d8830e05e440048df0b8301766f2f599e617 Mon Sep 17 00:00:00 2001 From: Joachim Breitner Date: Thu, 30 Nov 2023 18:21:51 +0100 Subject: [PATCH] chore: CI: in quick mode, only Nix build runs the tests (#2998) Following up on #2986, stop running the test suite in ci.yml in quick mode; the test suite is run in the Nix job, and we do not need to run it twice. With a cold nix cache, when `lean` is rebuilt, not much changes, as both jobs take ~20mins. But when `lean` is unchanged, the nix build should be faster, and shaving off the (currently) 4mins in the CI.yaml run should get us to a green PR sooner. Another benefit is that we get the PR release sooner and even get it when the test suite fails, which can be useful if you want to test mathlib or other things before fixing the lean test suite. --- .github/workflows/ci.yml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 6b7c44946faa..524d9add3fa9 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -371,10 +371,10 @@ jobs: ulimit -c unlimited # coredumps # exclude nonreproducible test ctest -j4 --output-on-failure ${{ matrix.CTEST_OPTIONS }} < /dev/null - if: matrix.wasm || !matrix.cross + if: (matrix.wasm || !matrix.cross) && !needs.configure.outputs.quick - name: Check Test Binary run: ${{ matrix.binary-check }} tests/compiler/534.lean.out - if: ${{ !matrix.cross }} + if: ${{ !matrix.cross && !needs.configure.outputs.quick }} - name: Build Stage 2 run: | cd build