Skip to content

Commit

Permalink
chore: CI: in quick mode, only Nix build runs the tests (#2998)
Browse files Browse the repository at this point in the history
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.
  • Loading branch information
nomeata authored Nov 30, 2023
1 parent 5b6e4fa commit f356d88
Showing 1 changed file with 2 additions and 2 deletions.
4 changes: 2 additions & 2 deletions .github/workflows/ci.yml
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down

0 comments on commit f356d88

Please sign in to comment.