-
Notifications
You must be signed in to change notification settings - Fork 5
Add CI caching and improve CI tooling #239
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Conversation
43f5221 to
865514f
Compare
|
We're very explicitly building with a stable release, so it should be used for local development and for CI builds. The only reason we use a nightly for formatting is that many formatting config options are unstable only. You can run those locally for formatting with |
iamrecursion
left a comment
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
This is a really great start! Thanks so much for cleaning this up bigtime! A few comments:
- What is the impact to our CI runtime to use the container? I would hope that even with that new overhead it reduces the general CI runtime.
- Please make sure that there are as few mentions of the lean toolchain version or rust toolchain version as possible. If you can, I would suggest relying only on the
rust-toolchain.tomlandlean-toolchainfiles as relevant. - If that is not possible, we should be checking that they are coherent in any place that they exist on CI and before building any images.
I do apologise if I've left any silly questions. CI and particularly containers are quite far out of my wheelhouse, so please point out anywhere I've got something wrong!
Other than that, please let me know if you've got any questions, and thanks for the hard work at all of this!
|
Just a thought: an interesting test for whether this all works with good devx would be trying to update the Rust version to the latest stable release and separately the Lean version to the latest stable release. Do note that for the Lean version #234 is worth taking a look at as that claims to have the fix we need for the issue that was blocking us from versions |
|
When you want me to take a look at this again, please ping me and/or re-request review! Easiest way to get my attention! I've also fixed the branch protection rules to look for the "Build CLI" job name instead of "Build Rust" so it shouldn't be blocked on the CI portion any more, just an approving review. |
bb1ff50 to
c2dff27
Compare
|
a lot of comments I still need to address but at least now we have the image already pushed to shame i didn't realize earlier i could have just built and pushed the image from this PR, I'll close #240 now, have already rebased this branch on top of those changes. about your worries if this will still be faster after the image build step: yes, because we won't rebuild the image on every PR. and other changes about making the DAG better and hitting cache whenever possible go a long mile. we have to decide on when we want to build the image but i think we can just run manually whenever we want to change the versions. requiring to merge something first to only then be able to update the image version could be annoying. but we can always check if the toolchain versions are all the same and if not, build and push a new image. |
76ced5c to
4ad1585
Compare
iamrecursion
left a comment
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
This is really good stuff. A few more questions and comments about making this work smoothly!
1ce4f22 to
bb58f0a
Compare
bb58f0a to
1b9da5f
Compare
|
I went back and forth with how to structure the commits, removed the previous discarded attempts from history, but still not suuuper happy with how it turned out, wish the scripts could be simplified and didn't depend on different logic for CI, but there are a few footguns this avoids (i think lake will verify mathlib on ci or something like that, at least i ran into that when iterating earlier) i sugggest we squash the commits before merging. maybe something like |
iamrecursion
left a comment
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
This is fantastic! Thanks so much for all the hard work on this!
| with: | ||
| registry: ghcr.io | ||
| username: ${{ github.actor }} | ||
| password: ${{ secrets.GITHUB_TOKEN }} |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I take it we don't need the GHCR_TOKEN now?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
precisely. we needed it temporarily cuz i wasnt sure i had permissions to push images from actions in my pr before it got merged. but in hindsight it was never necessary
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Awesome. I'll remove it from the repo!
lake exe cache getlake exe cache getto avoid rebuilding mathlib, lampe and stdlib