chore: trim CI set by default #2986
Conversation
Note that the CI step only tests that the benchmarks still work, it is not a part of the
One upside is that we could now actually factor out common configuration :) ? But all the comments are gone :( ? |
Ah, great! Removed from |
That’s what I meant to say :-)
Ups. While converting I thought “I need to put comments back in”, and then thought got lost… will fix … fixed. |
github-actions
bot
added
the
toolchain-available
|
nomeata
force-pushed
the
joachim/quick-ci
branch
from
4c2d6aa
to
6fb58e2
Compare
|
As expected the PR release only has linux: I’ll rebase this on nightly-with-mathlib to see if the mathlib test job works as expected. |
leanprover-community-mathlib4-bot
added
the
builds-mathlib
|
Ok, mathlib builds. Good to go, I guess… |
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.
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.
The goal of this change is to run a trimmed-down CI on PRs by default, but allows opt-in the full CI as necessary.
Specification
The CI workflow runs in “quick” mode if it was triggered from a pull request, and that pull request does not have the
full-cilabel set.In “quick” mode the build matrix contains fewer jobs. At the moment only:
In non-quick mode everything should be as before.
Implementation notes
I created a
configurejob that combines all the previousset-jobs, I guess this is faster than firing up separate jobs.The matrix is calculated in this job; this seems to be the cleanest way to get a dynamic matrix going (experiments using
excludefailed). The downside is that the matrix is now in JSON rather than Yaml syntax. The upside is that we can (later) make it’s calculation simpler, e.g. set defaultshellvalues etc.I was not able to make it so that CI runs when the
full-cilabel is added, but don’t do anything otherwise. I think it can be done with another workflow listening tolabeledand then triggering this one, but let’s do that separately. For now, add the label and then push (or close and reopen).The checks
were dead code, we did not have these fields in the matrix anymore, so I replaced them with